[en] We present MsATL: the first tool for deciding the satisfiability of
Alternating-time Temporal Logic ( ATL ) with imperfect informa-
tion. MsATL combines SAT Modulo Monotonic Theories solvers
with existing ATL model checkers: MCMAS and STV. The tool can
deal with various semantics of ATL , including perfect and imper-
fect information, and can handle additional practical requirements.
MsATL can be applied for synthesis of games that conform to a
given specification, with the synthesised game often being minimal.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
Niewiadomski, Artur
Kacprzak, Magdalena
Kurpiewski, Damian
Knapik, Michał
Penczek, Wojciech
JAMROGA, Wojciech ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > APSIA
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
MsATL: a Tool for SAT-Based ATL Satisfiability Checking
Date de publication/diffusion :
2020
Nom de la manifestation :
19th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2020
Date de la manifestation :
9-13 May 2020
Manifestation à portée :
International
Titre de l'ouvrage principal :
Proceedings of 19th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2020
R. Alur, T. A. Henzinger, and O. Kupferman. 1997. Alternating-Time Temporal Logic. In Proc. of the 38th IEEE Symp. on Foundations of Computer Science (FOCS'97). IEEE Computer Society, 100-109.
R. Alur, T. A. Henzinger, and O. Kupferman. 1998. Alternating-Time Temporal Logic. LNCS 1536 (1998), 23-60.
R. Alur, T. A. Henzinger, and O. Kupferman. 2002. Alternating-Time Temporal Logic. J. ACM 49(5) (2002), 672-713.
P. C. Attie, A. Cherri, K. Dak-Al-Bab, M. Sakr, and J. Saklawi. 2015. Model and program repair via SAT solving. In 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Austin, TX, USA, September 21-23, 2015. IEEE, 148-157.
S. Bayless, N. Bayless, H.H. Hoos, and A.J. Hu. 2015. SAT Modulo Monotonic Theories. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI'15). AAAI Press, 3702-3709.
F. Belardinelli. 2014. Reasoning about Knowledge and Strategies: Epistemic Strategy Logic. In Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014. 27-33.
N. Bulling and W. Jamroga. 2011. Alternating Epistemic Mu-Calculus. In Proceedings of IJCAI-11. 109-114.
N. Bulling and W. Jamroga. 2014. Comparing Variants of Strategic Ability: How Uncertainty and Memory Influence General Properties of Games. Journal of Autonomous Agents and Multi-Agent Systems 28, 3 (2014), 474-518.
E.M. Clarke and E.A. Emerson. 1981. Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In Proceedings of Logics of Programs Workshop (Lecture Notes in Computer Science), Vol. 131. 52-71.
A. David. 2015. Deciding ATL* Satisfiability by Tableaux. In International Conference on Automated Deduction. Springer, 214-228.
E. De Angelis, A. Pettorossi, and M. Proietti. 2012. Synthesizing Concurrent Programs Using Answer Set Programming. Fundam. Inform. 120, 3-4 (2012), 205-229.
C. Dima, B. Maubert, and S. Pinchinat. 2015. Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus. In Proceedings of MFCS (Lecture Notes in Computer Science), Vol. 9234. Springer, 179-191. https://doi.org/10.1007/ 978-3-662-48057-1_14
C. Dima and F.L. Tiplea. 2011. Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable. CoRR abs/1102.4225 (2011).
N. Eén and N. Sörensson. 2003. An Extensible SAT-solver. In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers (Lecture Notes in Computer Science), Vol. 2919. Springer, 502-518.
D. Gopinath, M.Z. Malik, and S. Khurshid. 2011. Specification-Based Program Repair Using SAT. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings (Lecture Notes in Computer Science), Vol. 6605. Springer, 173-188.
V. Goranko and G. Van Drimmelen. 2006. Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science 353, 1-3 (2006), 93-117.
V. Goranko and D. Shkatov. 2009. Tableau-based decision procedures for logics of strategic ability in multiagent systems. ACM Trans. Comput. Log. 11, 1 (2009), 3:1-3:51.
W. Jamroga and J. Dix. 2006. Model Checking ATLir is Indeed ∆2P -complete. In Proceedings of EUMAS'06 (CEUR Workshop Proceedings), Vol. 223. CEUR-WS.org.
W. Jamroga, M. Knapik, D. Kurpiewski, and Ł. Mikulski. 2019. Approximate verification of strategic abilities under imperfect information. Artif. Intell. 277 (2019).
W. Jamroga, W. Penczek, P. Dembiński, and A. Mazurkiewicz. 2018. Towards Partial Order Reductions for Strategic Ability. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS'18). 156-165.
M. Kacprzak, A. Niewiadomski, and W. Penczek. 2020. SAT-Based ATL Satisfiability Checking. (2020). arXiv:cs.LO/2002.03117
M. Kacprzak and W. Penczek. 2004. A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic. Synthese 142, 2 (2004), 203-227.
G. Katz and D. Peled. 2017. Synthesizing, correcting and improving code, using model checking-based genetic programming. STTT 19, 4 (2017), 449-464.
T. Klenze, S. Bayless, and A.J. Hu. 2016. Fast, Flexible, and Minimal CTL Synthesis via SMT. In Computer Aided Verification, S. Chaudhuri and A. Farzan (Eds.). Springer International Publishing, 136-156.
J. R. Koza. 1993. Genetic programming - on the programming of computers by means of natural selection. MIT Press.
K. Krawiec, I. Bladek, J. Swan, and J. H. Drake. 2018. Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden. ijcai.org, 5304-5308.
D. Kurpiewski, W. Jamroga, and M. Knapik. 2019. STV: Model Checking for Strategies under Imperfect Information. In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS'19, Montreal, QC, Canada, May 13-17, 2019. 2372-2374.
D. Kurpiewski, M. Knapik, and W. Jamroga. 2019. On Domination and Control in Strategic Ability. In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS'19, Montreal, QC, Canada, May 13-17, 2019. 197-205.
A. Lomuscio, W. Penczek, and H. Qu. 2010. Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems. Fundam. Inform. 101, 1-2 (2010), 71-90.
A. Lomuscio, H. Qu, and F. Raimondi. 2017. MCMAS: an open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer 19, 1 (2017), 9-30.
A. Lomuscio and F. Raimondi. 2006. Model checking knowledge, strategies, and games in multi-agent systems. In 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan, May 8-12, 2006. 161-168.
S. Schewe. 2008. ATL* Satisfiability Is 2EXPTIME-Complete. In Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations. 373-385.
P. Y. Schobbens. 2004. Alternating-Time Logic with Imperfect Recall. Electronic Notes in Theoretical Computer Science 85, 2 (2004), 82-93.
G. van Drimmelen. 2003. Satisfiability in alternating-time temporal logic. In 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. IEEE, 208-217.
D. Walther, C. Lutz, F. Wolter, and M. Wooldridge. 2006. ATL satisfiability is indeed EXPTIME-complete. Journal of Logic and Computation 16, 6 (2006), 765-787.
