MsATL: a Tool for SAT-Based ATL Satisfiability Checking

Niewiadomski, Artur; Kacprzak, Magdalena; Kurpiewski, Damian; Knapik, Michał; Penczek, Wojciech; JAMROGA, Wojciech

Download

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

MsATL: a Tool for SAT-Based ATL Satisfiability Checking

Niewiadomski, Artur; Kacprzak, Magdalena; Kurpiewski, Damian et al.

2020 • In Proceedings of 19th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2020

Peer reviewed

Permalink
https://hdl.handle.net/10993/45853

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

msatatl20aamas[1].pdf

Author preprint (618.69 kB)

Download

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Abstract :

[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 :

Computer science

Author, co-author :

Niewiadomski, Artur

Kacprzak, Magdalena

Kurpiewski, Damian

Knapik, Michał

Penczek, Wojciech

JAMROGA, Wojciech ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > APSIA

External co-authors :

yes

Language :

English

Title :

MsATL: a Tool for SAT-Based ATL Satisfiability Checking

Publication date :

2020

Event name :

19th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2020

Event date :

9-13 May 2020

Audience :

International

Main work title :

Proceedings of 19th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2020

ISBN/EAN :

978-1-4503-7518-4

Peer reviewed :

Peer reviewed

Focus Area :

Security, Reliability and Trust

Additional URL :

http://www.ifaamas.org/Proceedings/aamas2020/pdfs/p2111.pdf

FnR Project :

FNR12685695 - Socio-technical Verification Of Information Security And Trust In Voting Systems, 2018 (01/09/2019-31/08/2022) - Peter Y. A. Ryan

Available on ORBilu :

since 24 January 2021

Statistics

Number of views

94 (17 by Unilu)

Number of downloads

62 (5 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

Bibliography

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.