Article

Parallel Model Checking for Temporal Epistemic Logic

Authors:

Marta Kwiatkowska,

Alessio Lomuscio,

Hongyang QuAuthors Info & Claims

Proceedings of the 2010 conference on ECAI 2010: 19th European Conference on Artificial Intelligence

Pages 543 - 548

Published: 04 August 2010 Publication History

Abstract

We investigate the problem of the verification of multi-agent systems by means of parallel algorithms. We present algorithms for CTLK, a logic combining branching time temporal logic with epistemic modalities. We report on an implementation of these algorithms and present the experimental results obtained. The results point to a significant speed-up in the verification step.

References

[1]

R. E. Bryant, 'Graph-based algorithms for boolean function manipulation', IEEE Transactions on Computers, 35(8), 677-691, (1986).

Digital Library

[2]

D. Chaum, 'The dining cryptographers problem: Unconditional sender and recipient untraceability', Journal of Cryptology, 1(1), 65-75, (1988).

Digital Library

[3]

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

Digital Library

[4]

M. Cohen, M. Dam, A. Lomuscio, and H. Qu, 'A symmetry reduction technique for model checking temporal-epistemic logic', in the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 721-726, (2009).

Digital Library

[5]

M. Cohen, M. Dam, A. Lomuscio, and F. Russo, 'Abstraction in model checking multi-agent systems', in 8th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2009), pp. 945-952. IFAAMAS, (2009).

Digital Library

[6]

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

Digital Library

[7]

P. Gammie and R. van der Meyden, 'MCK: Model checking the logic of knowledge', in Proceedings of 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of LNCS, pp. 479-483. Springer, (2004).

[8]

O. Grumberg, T. Heyman, and A. Schuster, 'Distributed symbolic model checking for µ-calculus', Formal Methods in System Design, 26(2), 197-219, (2005).

Digital Library

[9]

A. Lomuscio, H. Qu, and F. Raimondi, 'MCMAS: A model checker for the verification of multi-agent systems.', in Proceedings of CAV 2009, LNCS 5643, pp. 682-688. Springer, (2009).

Digital Library

[10]

A. Lomuscio, H. Qu, and M. Solanki, 'Towards verifying compliance in agent-based web service compositions', in Proceedings of The Seventh International Joint Conference on Autonomous Agents and Multi-agent systems (AAMAS-08). IFAAMAS, (2008).

Digital Library

[11]

A. Lomuscio and F. Raimondi, 'MCMAS: A model checker for multi-agent systems.', in Proceedings of TACAS 2006, volume 3920, pp. 450- 454. Springer, (2006).

Digital Library

[12]

R. M. Needham and M. D. Schroeder, 'Using encryption for authentication in large networks of computers', Communications of the ACM, 21(12), 993-999, (1978).

Digital Library

[13]

R. Parikh and R. Ramanujam, 'Distributed processes and the logic of knowledge', in Logic of Programs, volume 193 of Lecture Notes in Computer Science, pp. 256-268. Springer, (1985).

Digital Library

[14]

W. Penczek and A. Lomuscio, 'Verifying epistemic properties of multi-agent systems via bounded model checking', Fundamenta Informaticae, 55(2), 167-185, (2003).

Digital Library

[15]

F. Raimondi and A. Lomuscio, 'Automatic verification of multi-agent systems by model checking via OBDDs', Journal of Applied Logic, 5(2), 235-251, (2005).

[16]

D. Sahoo, J. Jain, S. K. Iyer, and D. L. Dill, 'A new reachability algorithm for symmetric multi-processor architecture', in the 3th International Symposium on Automated Technology for Verification and Analysis (ATVA 2005), LNCS 3707, pp. 26-38. Springer, (2005).

Digital Library

[17]

F. Somenzi. CUDD: CU decision diagram package - release 2.4.2. http://vlsi.colorado.edu/~fabio/CUDD/ cuddIntro.html, 2009.

Cited By

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
Cimatti AGario MTonetta SJonker CMarsella SThangarajah JTuyls K(2016)A Lazy Approach to Temporal Epistemic Logic Model CheckingProceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems10.5555/2936924.2937101(1218-1226)Online publication date: 9-May-2016
https://dl.acm.org/doi/10.5555/2936924.2937101
Qu HVeres S(2016)Verification of logical consistency in robotic reasoningRobotics and Autonomous Systems10.1016/j.robot.2016.06.00583:C(44-56)Online publication date: 1-Sep-2016
https://dl.acm.org/doi/10.1016/j.robot.2016.06.005
Show More Cited By

Index Terms

Parallel Model Checking for Temporal Epistemic Logic
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic

Recommendations

Symbolic model checking for temporal-epistemic logic
Logic Programs, Norms and Action

We survey some of the recent work in verification via symbolic model checking of temporal-epistemic logic. Specifically, we discuss OBDD-based and SAT-based approaches for epistemic logic built on discrete and real-time branching time temporal logic. ...
Interval vs. Point Temporal Logic Model Checking: An Expressiveness Comparison

In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modeled by means of (...
A Lazy Approach to Temporal Epistemic Logic Model Checking
AAMAS '16: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems

Temporal Epistemic Logic is used to reason about the evolution of knowledge over time. A notable example is the temporal epistemic logic KL₁, which is used to model what a reasoner can infer about the state of a dynamic system by using available ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Proceedings of the 2010 conference on ECAI 2010: 19th European Conference on Artificial Intelligence

August 2010

1141 pages

ISBN:9781607506058

Editors:
Helder Coelho
Faculty of Science, University of Lisbon, Portugal
,
Rudi Studer
Karlsruhe Institute of Technology, Germany
,
Michael Wooldridge
Department of Computer Science, University of Liverpool, United Kingdom

Publisher

IOS Press

Netherlands

Publication History

Published: 04 August 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Cimatti AGario MTonetta SJonker CMarsella SThangarajah JTuyls K(2016)A Lazy Approach to Temporal Epistemic Logic Model CheckingProceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems10.5555/2936924.2937101(1218-1226)Online publication date: 9-May-2016
https://dl.acm.org/doi/10.5555/2936924.2937101
Qu HVeres S(2016)Verification of logical consistency in robotic reasoningRobotics and Autonomous Systems10.1016/j.robot.2016.06.00583:C(44-56)Online publication date: 1-Sep-2016
https://dl.acm.org/doi/10.1016/j.robot.2016.06.005
Lomuscio APaquet HWeiss GYolum PBordini RElkind E(2015)Verification of Multi-Agent Systems via SDD-based Model CheckingProceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems10.5555/2772879.2773399(1713-1714)Online publication date: 4-May-2015
https://dl.acm.org/doi/10.5555/2772879.2773399
Phan QMalacaria PPǎsǎreanu C(2015)Concurrent Bounded Model CheckingACM SIGSOFT Software Engineering Notes10.1145/2693208.269324040:1(1-5)Online publication date: 6-Feb-2015
https://dl.acm.org/doi/10.1145/2693208.2693240
Herd BMiles SMcburney PLuck M(2015)$$ \texttt {MC} ^ \texttt {2} \texttt {MABS} $$MC2MABSRevised Selected Papers of the International Workshop on Multi-Agent Based Simulation XVI - Volume 956810.1007/978-3-319-31447-1_3(37-54)Online publication date: 5-May-2015
https://dl.acm.org/doi/10.1007/978-3-319-31447-1_3
Herd BMiles SMcburney PLuck M(2015)Quantitative Analysis of Multiagent Systems Through Statistical Model CheckingRevised, Selected, and Invited Papers of the Third International Workshop on Engineering Multi-Agent Systems - Volume 931810.1007/978-3-319-26184-3_7(109-130)Online publication date: 5-May-2015
https://dl.acm.org/doi/10.1007/978-3-319-26184-3_7
Lomuscio APenczek W(2012)Symbolic model checking for temporal-epistemic logicLogic Programs, Norms and Action10.5555/2340883.2340896(172-195)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.5555/2340883.2340896
Garanina N(2011)Exponential acceleration of model checking for perfect recall systemsProceedings of the 8th international conference on Perspectives of System Informatics10.1007/978-3-642-29709-0_12(111-124)Online publication date: 27-Jun-2011
https://dl.acm.org/doi/10.1007/978-3-642-29709-0_12

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents