Verifying epistemic properties of multi-agent systems via bounded model checking
- 14 July 2003
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. 55 (2) , 209-216
- https://doi.org/10.1145/860575.860609
Abstract
We present a framework for verifying temporal and epistemic properties of multi-agent systems by means of bounded model checking. We use interpreted systems as underlying semantics. We give details of the proposed technique, and show how it can be applied to the "attacking generals problem", a typical example of oordination in multi-agent systems.Keywords
This publication has 14 references indexed in Scilit:
- Complete Axiomatizations for Reasoning about Knowledge and TimeSIAM Journal on Computing, 2004
- Tractable multiagent planning for epistemic goalsPublished by Association for Computing Machinery (ACM) ,2002
- Model checking multi-agent systems with MABLEPublished by Association for Computing Machinery (ACM) ,2002
- ChaffPublished by Association for Computing Machinery (ACM) ,2001
- Knowledge in multiagent systemsACM Transactions on Computational Logic, 2000
- Model Checking Knowledge and Time in Systems with Perfect RecallPublished by Springer Nature ,1999
- Decision procedures for BDI logicsJournal of Logic and Computation, 1998
- What can machines know?Journal of the ACM, 1992
- Knowledge and common knowledge in a distributed environmentJournal of the ACM, 1990
- Using branching time temporal logic to synthesize synchronization skeletonsScience of Computer Programming, 1982