More Web Proxy on the site http://driver.im/

article

Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking

Authors:

Wojciech Penczek,

Alessio LomuscioAuthors Info & Claims

Fundamenta Informaticae, Volume 55, Issue 2

Pages 167 - 185

Published: 01 April 2003 Publication History

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 coordination in multi-agent systems.

References

[1]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS'99, volume 1579 of LNCS, pages 193-207. Springer-Verlag, 1999.

Digital Library

[2]

M. E. Bratman. Intentions, Plans, and Practical Reason. Harvard University Press: Cambridge, MA, 1987.

[3]

E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7-34, 2001.

Digital Library

[4]

E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.

Digital Library

[5]

E. A. Emerson. Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter Temporal and Modal Logic, pages 995-1067. Elsevier, 1990.

[6]

E. A. Emerson and E. M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241-266, 1982.

[7]

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.

Digital Library

[8]

R. Fagin, J. Y. Halpern, and M. Y. Vardi. What can machines know? On the properties of knowledge in distributed systems. Journal of the ACM, 39(2):328-376, Apr. 1992.

Digital Library

[9]

J. Halpern, R. Meyden, and M. Y. Vardi. Complete axiomatisations for reasoning about knowledge and time. SIAM Journal on Computing, 2003. To Appear.

[10]

J. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3):549-587, 1990. A preliminary version appeared in Proc. 3rd ACM Symposium on Principles of Distributed Computing, 1984.

Digital Library

[11]

W. van der Hoek and M. Wooldridge. Model checking knowledge and time. In Proc. of the 9th Int. SPIN Workshop (SPIN'02), volume 2318 of LNCS, pages 95-111. Springer-Verlag, 2002.

Digital Library

[12]

W. van der Hoek and M. Wooldridge. Tractable multiagent planning for epistemic goals. In Proc. of the 1st Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'02), July 2002. to appear.

Digital Library

[13]

R. van der Meyden and H. Shilov. Model checking knowledge and time in systems with perfect knowledge. In Proceedings of Proc. of FST&TCS, volume 1738 of Lecture Notes in Computer Science, pages 432-445, Hyderabad, India, 1999.

Digital Library

[14]

ISO/IEC 9074(E), Estelle - a formal description technique based on an extended state-transition model. International Standards Organization, 1997.

[15]

B. van Linder, W. van der Hoek, and J.-J. Meyer. Seeing is believing, and so are hearing and jumping. Journal of Logic, Language, and Information, 6(1):33-61, 1997.

[16]

A. Lomuscio, T. ¿asica, and W. Penczek. Bounded model checking for interpreted systems: preliminary experimental results. In M. Hinchey, editor, Proceedings of FAABS II, volume 2699 of LNCS. Springer Verlag, 2003.

[17]

A. Lomuscio, R. Meyden, and M. Ryan. Knowledge in multi-agent systems: Initial configurations and broadcast. ACM Transactions of Computational Logic, 1(2), 2000.

Digital Library

[18]

A. Lomuscio, F. Raimondi, and M. Sergot. Towards model checking interpreted systems. In Proceedings of Mochart -- First International Workshop on Model Checking and Artificial Intelligence, 2002.

[19]

A. Lomuscio and M. Sergot. Deontic interpreted systems. Studia Logica, 75, 2003.

[20]

M.-P. H. M. Wooldridge, M. Fisher and S. Parsons. Model checking multiagent systems with mable. In Proceedings of the First International Conference on Autonomous Agents and Multiagent Systems (AAMAS- 02), Bologna, Italy, July 2002.

Digital Library

[21]

Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems, volume 1. Springer-Verlag, Berlin/New York, 1992.

Digital Library

[22]

R. V. Meyden and K. Wong. Complete axiomatizations for reasoning about knowledge and branching time. Studia Logica, 75, 2003.

[23]

J.-J. C. Meyer and R. J. Wieringa. Deontic logic: A concise overview. In Deontic Logic in Computer Science, Wiley Professional Computing Series, chapter 1, pages 3-16. John Wiley and Sons, Chichester, UK, 1993.

[24]

M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference (DAC01), pages 530-535, June 2001.

[25]

W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. In T. Sandholm, editor, Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-agent systems (AAMAS-03), 2003.

[26]

W. Penczek, B. Wozna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, 2002.

Digital Library

[27]

A. S. Rao and M. P. Georgeff. Decision procedures for BDI logics. Journal of Logic and Computation, 8(3):293-343, June 1998.

[28]

M. Wooldridge. Computationally grounded theories of agency. In E. Durfee, editor, Proceedings of ICMAS, International Conference of Multi-Agent Systems. IEEE Press, 2000.

Digital Library

Cited By

Kouvaros PElkind E(2023)Towards formal verification of neuro-symbolic multi-agent systemsProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/800(7014-7019)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/800
Bozzelli LMaubert BMurano A(2023)On the Complexity of Model Checking Knowledge and TimeACM Transactions on Computational Logic10.1145/363721225:1(1-42)Online publication date: 13-Dec-2023
https://dl.acm.org/doi/10.1145/3637212
B TRamesh YKalyanasundaram SRao MHong JLanperne MPark JCerny TShahriar H(2023)Traffic Intersections as Agents: A model checking approach for analysing communicating agentsProceedings of the 38th ACM/SIGAPP Symposium on Applied Computing10.1145/3555776.3577720(109-118)Online publication date: 27-Mar-2023
https://dl.acm.org/doi/10.1145/3555776.3577720
Show More Cited By

Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking

Recommendations

Verifying epistemic properties of multi-agent systems via bounded model checking
AAMAS '03: Proceedings of the second international joint conference on Autonomous agents and multiagent systems

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 ...
Verification of multi-agent systems via bounded model checking
AI'06: Proceedings of the 19th Australian joint conference on Artificial Intelligence: advances in Artificial Intelligence

We present a bounded model checking (BMC) approach to the verification of temporal epistemic properties of multi-agent systems. We extend the temporal logic CTL^* by incorporating epistemic modalities and obtain a temporal epistemic logic that we call ...
Verifying epistemic properties of multi-agent systems via bounded model checking
Concurrency specification and programming

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Fundamenta Informaticae

Fundamenta Informaticae Volume 55, Issue 2

Concurrency Specification and Programming (CS&P'2002), Part 2

April 2003

138 pages

ISSN:0169-2968

Issue’s Table of Contents

Publisher

IOS Press

Netherlands

Publication History

Published: 01 April 2003

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

57
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kouvaros PElkind E(2023)Towards formal verification of neuro-symbolic multi-agent systemsProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/800(7014-7019)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/800
Bozzelli LMaubert BMurano A(2023)On the Complexity of Model Checking Knowledge and TimeACM Transactions on Computational Logic10.1145/363721225:1(1-42)Online publication date: 13-Dec-2023
https://dl.acm.org/doi/10.1145/3637212
B TRamesh YKalyanasundaram SRao MHong JLanperne MPark JCerny TShahriar H(2023)Traffic Intersections as Agents: A model checking approach for analysing communicating agentsProceedings of the 38th ACM/SIGAPP Symposium on Applied Computing10.1145/3555776.3577720(109-118)Online publication date: 27-Mar-2023
https://dl.acm.org/doi/10.1145/3555776.3577720
Drawel NBentahar JLaarej ARjoub G(2022)Formal verification of group and propagated trust in multi-agent systemsAutonomous Agents and Multi-Agent Systems10.1007/s10458-021-09542-636:1Online publication date: 1-Apr-2022
https://dl.acm.org/doi/10.1007/s10458-021-09542-6
Lomuscio ABogomolov SFisher MKress-Gazit HSoudjani SZuliani P(2021)Towards verifying neural autonomous systemsProceedings of the 1st International Workshop on Verification of Autonomous & Robotic Systems10.1145/3459086.3459627(1-2)Online publication date: 18-May-2021
https://dl.acm.org/doi/10.1145/3459086.3459627
Akintunde MBotoeva EKouvaros PLomuscio A(2021)Formal verification of neural agents in non-deterministic environmentsAutonomous Agents and Multi-Agent Systems10.1007/s10458-021-09529-336:1Online publication date: 9-Nov-2021
https://dl.acm.org/doi/10.1007/s10458-021-09529-3
Barrière AMaubert BMurano ARubin SElkind EVeloso MAgmon NTaylor M(2019)Reasoning about Changes of Observational Power in Logics of Knowledge and TimeProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3331792(971-979)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3331792
Kong JLomuscio AAndre EKoenig SDastani MSukthankar G(2018)Model Checking Multi-Agent Systems against LDLK Specifications on Finite TracesProceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3237383.3237414(166-174)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.5555/3237383.3237414
Kong JLomuscio A(2017)Model checking multi-agent systems against LDLK specificationsProceedings of the 26th International Joint Conference on Artificial Intelligence10.5555/3171642.3171804(1138-1144)Online publication date: 19-Aug-2017
https://dl.acm.org/doi/10.5555/3171642.3171804
Kong JLomuscio ALarson KWinikoff MDas SDurfee E(2017)Symbolic Model Checking Multi-Agent Systems against CTL*K SpecificationsProceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems10.5555/3091125.3091147(114-122)Online publication date: 8-May-2017
https://dl.acm.org/doi/10.5555/3091125.3091147
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents