A process algebraic framework for multi-agent dynamic epistemic systems

TL;DR

This paper introduces a unified process algebraic framework combining labeled transition systems and epistemic models to analyze multi-agent dynamic systems, with a practical specification language and a modal logic for verification.

Contribution

It presents a novel process algebraic language for modeling multi-agent systems with knowledge dynamics and a modal logic for their analysis.

Findings

Framework unifies modeling and verification of multi-agent systems

Specification language simplifies practical modeling

Modal logic enables comprehensive reasoning about knowledge and time

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.