A process algebraic framework for multi-agent dynamic epistemic systems
Alessandro Aldini
TL;DR
The paper addresses the challenge of modeling multi-agent dynamic systems that combine temporal behavior with knowledge reasoning. It introduces Kripke labeled transition systems (KLTS) by attaching a per-state Kripke model to each LTS state and develops KT logic to express temporal-epistemic properties, along with a process-algebraic language for agent-oriented specifications. A Cluedo-inspired case study demonstrates the framework's expressiveness for knowledge transfer and private/public communications, and the authors discuss bisimulation, image-finiteness, and decidability implications. The work outlines future directions, including belief modalities, imperfect information, and probabilistic/time extensions to broaden practical applicability.
Abstract
This paper combines the classical model of labeled transition systems with the epistemic model for reasoning about knowledge. The result is a unifying framework for modeling and analyzing multi-agent, knowledge-based, dynamic systems. On the modeling side, we propose a process algebraic, agent-oriented specification language that makes such a framework easy to use for practical purposes. On the verification side, we define a modal logic encompassing temporal and epistemic operators.