Scholarlink

<p>We present a formal framework encompassing concurrency theoretic and modal logic based approaches to the modeling and verification of dynamic multi-agent systems. We develop a model of computation merging classical labeled transition systems and multi-agent Kripke frames. Based on this model, which we call a Kripke labeled transition system, we provide a modal logic and a process algebra for the specification and analysis of interacting multi-agent systems. Our logic is obtained by combining proof systems for Hennessy-Milner Logic and the normal epistemic logic <InlineEquation ID="IEq1"> <EquationSource Format="TEX">\(\textsf{S5}_n\)</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="sans-serif">S</mi> <msub> <mn mathvariant="sans-serif">5</mn> <mi>n</mi> </msub> </mrow> </math></EquationSource> </InlineEquation> and is sound and complete with respect to its intended models. Further, we show that this logic is decidable and induces a behavioral equivalence combining classical notions of bisimulation. We prove that our process algebra is adequate for specifying the behavior of Kripke labeled transition systems and we show its effectiveness and usability through real-world examples.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Bridging concurrency theory and epistemic models: a formal framework for dynamic multi-agent systems

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年3月11日

查看全文
  • Alessandro Aldini,
  • Ludovico Fusco

摘要

We present a formal framework encompassing concurrency theoretic and modal logic based approaches to the modeling and verification of dynamic multi-agent systems. We develop a model of computation merging classical labeled transition systems and multi-agent Kripke frames. Based on this model, which we call a Kripke labeled transition system, we provide a modal logic and a process algebra for the specification and analysis of interacting multi-agent systems. Our logic is obtained by combining proof systems for Hennessy-Milner Logic and the normal epistemic logic \(\textsf{S5}_n\) S 5 n and is sound and complete with respect to its intended models. Further, we show that this logic is decidable and induces a behavioral equivalence combining classical notions of bisimulation. We prove that our process algebra is adequate for specifying the behavior of Kripke labeled transition systems and we show its effectiveness and usability through real-world examples.