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

Abstract 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$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>S</mml:mi> <mml:msub> <mml:mn>5</mml:mn> <mml:mi>n</mml:mi> </mml:msub> </mml:mrow> </mml:math> 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.