Unbounded Model Checking for ATL

• Autorzy: Kański Michał , Niewiadomski Artur , Kacprzak Magdalena , Penczek Wojciech , Nabiałek Wojciech

Identyfikatory

DOI

10.34739/si.2021.25.01

• Języki publikacji: EN

Abstrakty

EN

In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.

Słowa kluczowe

EN

ATL; temporal logics; model checking; SAT; SMT; QBF

• Wydawca: Wydawnictwo Uniwersytetu Przyrodniczo-Humanistycznego w Siedlcach
• Czasopismo: Studia Informatica : systems and information technology
• Rocznik: 2021
• Tom: Vol. 1-2(25)
• Strony: 5--22
• Opis fizyczny: Bibliogr. 36 poz., tab., rys.

Twórcy

autor

Kański Michał

• Siedlce University of Natural Sciences and Humanities, Faculty of Exact and Natural Sciences, Institute of Computer Science, ul. 3 Maja 54, 08-110 Siedlce, Poland

autor

Niewiadomski Artur

• Siedlce University of Natural Sciences and Humanities, Faculty of Exact and Natural Sciences, Institute of Computer Science, ul. 3 Maja 54, 08-110 Siedlce, Poland

autor

Kacprzak Magdalena

• Białystok University of Technology, Faculty of Computer Science, ul. Wiejska 45A, 15-351, Białystok , Poland

autor

Penczek Wojciech

• Institute of Computer Science, Polish Academy of Sciences, ul. Jana Kazimierza 5, 01-248, Warsaw, Poland

autor

Nabiałek Wojciech

• Siedlce University of Natural Sciences and Humanities, Faculty of Exact and Natural Sciences, Institute of Computer Science, ul. 3 Maja 54, 08-110 Siedlce, Poland

Bibliografia

• 1. Alur R., Courcoubetis C.; Dill D.: Model-checking for real-time systems. In: [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE, 1990. p. 414-425.
• 2. Alur R., Henzinger T. A., and Kupferman O.: Alternating-time temporal logic. In Proc. of the 38th IEEE Symp. on Foundations of Computer Science (FOCS’97), pages 100-109. IEEE Computer Society, 1997.
• 3. Alur R., Henzinger T. A., and Kupferman O.: Alternating-time temporal logic. LNCS, 1536:23-60, 1998.
• 4. Alur R., Henzinger T. A., and Kupferman O.: Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002.
• 5. Baier C. and Katoen J.: Principles of model checking. MIT Press, 2008.
• 6. Biere A., Cimatti A., Clarke E., and Zhu Y.: Symbolic model checking without BDDs. In International conference on tools and algorithms for the construction and analysis of systems, pages 193-207. Springer, 1999.
• 7. Biere A., Cimatti A., Clarke E., Strichman O., and Zhu Y.: Bounded model checking. 2003.
• 8. Browne M. C., Clarke E. M., Dill D. L., and Mishra B.: Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12):1035-1044, 1986.
• 9. Bryant R.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, 1986.
• 10. Cimatti A., Clarke E., Giunchiglia F., and Roveri M.: NuSMV: a new symbolic model verifier. In International conference on computer aided verification, pages 495-499. Springer, 1999.
• 11. Clarke E., Biere A., Raimi R., and Zhu Y.: Bounded model checking using satisfiability solving. Formal methods in system design, 19(1):7-34,2001.
• 12. Clarke E., and Emerson E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, pages 52-71, 1981.
• 13. Clarke Jr E. M., Grumberg O., Kroening D., Peled D., and Veith H.: Model checking. MIT press, 2018.
• 14. Davis M., Logemann G., and Loveland D.: A machine program for theorem-proving. Communications of the ACM, 5():394-397, 1962.
• 15. De Moura L. and Bjørner N.: Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems pages 337-340. Springer, 2008.
• 16. Doijade M. M. and Kulkarni D. B.: Overview of sequential and parallel sat solvers. In International Conference of Information Communication adn Embedded Systems (ICICES2014), pages 1-4, 2014.
• 17. Jamroga W., Penczek W., Dembiński P., and Mazurkiewicz A.: Towards partial order reductions for strategic ability. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgents Systems, AAMAS’18, pages 156-165, 2018.
• 18. Jamroga W., Penczek W., Sidoruk T., Dembiński P., and Mazurkiewicz A.: Towards partial order reductions for strategic ability. Journal of Artificial Intelligence Research, 68:817-850, 2020.
• 19. Kacprzak M., Nabiałek W., Niewiadomski A., Penczek W., Półrola A., Szreter M., Woźna B., and Zbrzezny A.: Verics 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae, 85(1-4):313-328, 2008.
• 20. Kacprzak M., Niewiadomski A., and Penczek W.: SAT-based ATL satisfiability checking. In D. Calvanese, E. Erdem, and M. Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, pages 539-549, 2020.
• 21. Kacprzak M., and Penczek W.: Unbounded model checking for Alternating-Time Temporal Logic. In Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagents Systems, AAMAS 2004, pages 646-653, 2004.
• 22. Kacprzak M., and Penczek W.: Fully symolic unbounded model checking for alternating-time temporal logic. Auton. Agents Multi Agent Syst., 11(1):69-89,2005.
• 23. Knapik M., Niewiadomski A., Penczek W., Półrola A., Szreter M., and Zbrzezny A.: Parametric model checking with VerICS. In Transactions on Petri nets and other models of concurrency IV, pages 98-120. Springer, 2010.
• 24. Laroussine F., Markey N., and Oreiby G.: Model-checking timed ATL for durational concurrent games structures. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 245-259. Springer, 2006.
• 25. Lions J.-L., Luebeck L., Fauquembergue J.-L., Kahn G., Kubbat W., Levedag S., Mazzini L., Merle D., and O’Halloran C.: Ariane 5 flight 501 failure report by the inquiry board, 1996.
• 26. Lomuscio A., Qu H., and Raimondi F.: Mcmas: A model checker for the verification of multi-agent systems. In International conference on computer aided verification, pages 682-688. Springer, 2009.
• 27. Lomuscio A., Qu H., and Raimondi F.: MCMAS: an open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer, 19(1):9-30, 2017.
• 28. Lomuscio A., and Raimondi F.: MCMAS: a model checker for multi-agent systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 450-454. Springer, 2006.
• 29. McMillan K. L., Symbolic model checking. Kluwer, 1993.
• 30. McMillan K. L., Applying SAT methods in unbounded symbolic model checking. In International Conference on Computer Aided Verification, pages 250-264. Springer, 2002.
• 31. Pilecki J., Bednarczyk M. A., and Jamroga W.: SMC: synthesis of uniform strategies and verification of strategic ability for multi-agent systems. Journal of Logic and Computation, 27(7):1871-1895, 2017
• 32. Van der Hoek W. and Wooldridge W.: Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia logica, 75(1):125-157, 2003.
• 33. Vardi M. Y.: Automata-theoretic model checking revisited. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 137-150. Springer, 2007.
• 34. Vizel Y., Weissenbacher G., and Malik S.: Boolean satisfiability solvers and their applications in model checking. Proceedings of the IEEE, 103(11):2021-2035, 2015.
• 35. Wang J., Wang M., Zheng K., and Huang X.: Model checking nrf24101-based internet of things systems. In 9th International Conference of Information Technology in Medicine and Education (ITME), pages 867-871, 2018.
• 36. Zhang X. and van Breugel F.: Model checking randomized allgorithms with Java PathFinder. In Seventh International Conference on the Quantitative Evaluation of Systems, pages 157-158, 2010.