engleski

Verifying Epistemic Properties of Multi-agent Systems via Action-based Temporal Logic

This paper investigates the problem of multi-agent system (MAS) specification and verification, with the emphasis on their epistemic properties. Epistemic transition system (ETS) is introduced to present an agent as the smallest unit in a multi-agent system. Being composed of a set of well defined ETSs, MAS builds an epistemic synchronous product (ESP) describing the formal model for a multi-agent system. A special extension of Action computation tree logic with unless operator (ACTLW) for epistemic reasoning (ACTLW-ER) is then used for model checking epistemic properties of MAS. Epistemic operators of ACTLW-ER are implemented by symbolic model checking algorithms using binary decision diagrams.

Action Computation Tree Logic with Unless Operator; Epistemic Reasoning; Multi-agent Systems

nije evidentirano