Probabilistic Timed ATL

JAMROGA, Wojciech; Penczek, Wojciech; Kwiatkowska, Marta; Petrucci, Laure; Sidoruk, Teofil

doi:10.5555/3709347.3743625

Download

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

Probabilistic Timed ATL

JAMROGA, Wojciech; Penczek, Wojciech; Kwiatkowska, Marta et al.

2026 • In Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems

Peer reviewed

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

DOI
10.5555/3709347.3743625

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

jamroga25PTATL.pdf

Publisher postprint (651.24 kB)

Download

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

multi-agent systems; probabilistic model checking; strategic ability; continuous time

Abstract :

[en] We consider strategic reasoning for multi-agent systems modelled as networks of continuous-time probabilistic timed automata (TA) with asynchronous execution (PCAMAS) in the setting of imperfect information. We define PTATL, a probabilistic extension of the alternating-time timed temporal logic TATL, which is interpreted over PCAMAS. Focusing on memoryless strategies of agents with imperfect information, both probabilistic (irP) and deterministic (irp), we establish theoretical results regarding the computational complexity of model checking for the proposed logic: between PSPACE and EXPTIME for PTATL irp , and in 2EXPTIME for PTATL irP. We demonstrate the practical feasibility of verification for PTATL irp formulas through a novel proof-of-concept combination of state-of-the-art tools IMITATOR and PRISM on a scalable benchmark, with encouraging results.

Disciplines :

Computer science

Author, co-author :

JAMROGA, Wojciech ; University of Luxembourg

Penczek, Wojciech

Kwiatkowska, Marta

Petrucci, Laure

Sidoruk, Teofil

External co-authors :

yes

Language :

English

Title :

Probabilistic Timed ATL

Publication date :

2026

Event name :

The 24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS'25.

Event date :

2025

Main work title :

Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems

Publisher :

Association for Computing Machinery (ACM)

Peer reviewed :

Peer reviewed

FnR Project :

FNR17232062 - SpaceVote - Probabilistic Verification Of Complex Heterogeneous Systems: From Ballots To Ballistics, 2022 (01/03/2023-28/02/2026) - Peter Y. A. Ryan

Funding text :

This work was supported by: CNRS IRP “Le Trójkąt”, NCBR Poland &FNRLuxembourgunderthePolLux/FNR-COREprojectSpaceVote (POLLUX-XI/14/SpaceVote/2023 and C22/IS/17232062/SpaceVote), the ANR-22-CE48-0012 project BISOUS, the PHC Polonium project MoCcA (BPN/BFR/2023/1/00045). Marta Kwiatkowska contributed while on sabbatical and acknowledges funding from the ERC under the EU’s Horizon 2020 research and innovation programme (FUN2MODEL, grant agreement No. 834115). For the purpose of open access, and in fulfilment of the obligations arising from the grant agreement, the authors have applied CC BY 4.0 license to any Author Accepted Manuscript version arising from this submission.

Available on ORBilu :

since 12 January 2026

Statistics

Number of views

11 (0 by Unilu)

Number of downloads

4 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

Rajeev Alur, Costas Courcoubetis, and David L. Dill. 1993. Model-Checking in Dense Real-Time. Inf. Comput. 104, 1 (1993), 2-34.
Rajeev Alur and David L. Dill. 1990. Automata for Modeling Real-Time Systems. In Proceedings of ICALP'90 (Lecture Notes in Computer Science, Vol. 443). Springer, 322-335.
Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. 1997. Alternating-Time Temporal Logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS). IEEE Computer Society Press, 100-109.
Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. 2002. Alternating-Time Temporal Logic. J. ACM 49 (2002), 672-713.
Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, and Sasha Rubin. 2019. Probabilistic Strategy Logic. In Proceedings of IJCAI 2019. ijcai.org, 32-38.
Étienne André. 2021. IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability. In Proceedings of CAV 2021 (Lecture Notes in Computer Science, Vol. 12759). Springer, 552-565.
Jaime Arias, Carlos E. Budde, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk, and Mariëlle Stoelinga. 2020. Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. In Proceedings of ICFEM 2020. Springer, 3-19.
Jaime Arias, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci, and Teofil Sidoruk. 2023. Strategic (Timed) Computation Tree Logic. In Proceedings of AAMAS'23. ACM, 382-390.
Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press.
Francesco Belardinelli, Wojciech Jamroga, Damian Kurpiewski, Vadim Malvone, and Aniello Murano. 2019. Strategy Logic with Simple Goals: Tractable Reasoning about Strategies. In Proceedings of IJCAI'19. ijcai.org, 88-94.
Francesco Belardinelli, Wojciech Jamroga, Munyque Mittelmann, and Aniello Murano. 2023. Strategic Abilities of Forgetful Agents in Stochastic Environments. In Proceedings KR 2023. 726-731.
Francesco Belardinelli, Wojciech Jamroga, Munyque Mittelmann, and Aniello Murano. 2024. Verification of Stochastic Multi-Agent Systems with Forgetful Strategies. In Proceedings of AAMAS 2024. ACM, 160-169.
Raphaël Berthon, Nathanaël Fijalkow, Emmanuel Filiot, Shibashis Guha, Bastien Maubert, Aniello Murano, Laureline Pinault, Sophie Pinchinat, Sasha Rubin, and Olivier Serre. 2020. Alternating Tree Automata with Qualitative Semantics. ACM Trans. Comput. Logic 22, 1, Article 7 (2020), 24 pages.
Thomas Brihaye, Arnaud Da Costa Lopes, François Laroussinie, and Nicolas Markey. 2009. ATL with Strategy Contexts and Bounded Memory. In Proceedings of LFCS (Lecture Notes in Computer Science, Vol. 5407). Springer, 92-106.
Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. 2007. Strategy Logic. In Proceedings of CONCUR 2007. 59-73.
Taolue Chen, Vojtech Forejt, Marta Kwiatkowska, David Parker, and Aistis Simaitis. 2013. Automatic Verification of Competitive Stochastic Systems. Formal Methods in System Design 43, 1 (2013), 61-92.
Taolue Chen and Jian Lu. 2007. Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm. In Proceedings of FSKD 2007. 35-39.
Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, and Helmut Veith. 2018. Model Checking, 2nd Edition. MIT Press.
Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. 1995. Reasoning about Knowledge. MIT Press.
Dimitar P. Guelev and Catalin Dima. 2012. Epistemic ATL with Perfect Recall, Past and Strategy Contexts. In Proceedings of CLIMA-XIII (Lecture Notes in Computer Science, Vol. 7486). Springer, 77-93. https://doi.org/10.1007/978-3-642-32897-8_7
Hans Hansson and Bengt Jonsson. 1994. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing 6, 5 (1994), 512-535.
Karel Horák and Branislav Bošanskỳ. 2019. Solving Partially Observable Stochastic Games with Public Observations. In Proceedings of AAAI'19, Vol. 33. AAAI Press, 2029-2036.
Karel Horák, Branislav Bošanskỳ, Vojtěch Kovařík, and Christopher Kiekintveld. 2023. Solving Zero-sum One-sided Partially Observable Stochastic Games. Artificial Intelligence 316 (2023), 103838.
Xiaowei Huang, Kaile Su, and Chenyi Zhang. 2012. Probabilistic Alternating-Time Temporal Logic of Incomplete Information and Synchronous Perfect Recall. In Proceedings of AAAI'12. 765-771.
Xiaowei Huang and Ron van der Meyden. 2014. Symbolic Model Checking Epistemic Strategy Logic. In Proceedings of AAAI'14. 1426-1432.
Wojciech Jamroga and Nils Bulling. 2011. Comparing Variants of Strategic Ability. In Proc. of IJCAI 2011. IJCAI/AAAI, 252-257.
Wojciech Jamroga, Beata Konikowska, and Wojciech Penczek. 2016. Multi-Valued Verification of Strategic Ability. In Proceedings of AAMAS 2016. 1180-1189.
Wojtek Jamroga, Lukasz Masko, Lukasz Mikulski, Witold Pazderski, Wojciech Penczek, Teofil Sidoruk, and Damian Kurpiewski. 2022. Verification of Multi-Agent Properties in Electronic Voting: A Case Study. In Proceedings of AiML 2022. College Publications, 531-556.
Wojciech Jamroga, Wojciech Penczek, and Teofil Sidoruk. 2021. Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them. In Proceedings of KR 2021. 368-378.
Wojciech Jamroga, Wojciech Penczek, Teofil Sidoruk, Piotr Dembinski, and Antoni W. Mazurkiewicz. 2020. Towards Partial Order Reductions for Strategic Ability. JAIR 68 (2020), 817-850.
Magdalena Kacprzak and Wojciech Penczek. 2004. Unbounded Model Checking for Alternating-Time Temporal Logic. In Proceedings of AAMAS 2004. IEEE Computer Society, 646-653.
Magdalena Kacprzak and Wojciech Penczek. 2005. Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic. Autonomous Agents and Multi-Agent Systems 11, 1 (2005), 69-89.
John G. Kemeny, J. Laurie Snell, and Anthony W. Knapp. 1976. Denumerable Markov Chains. Springer, Chapter Stochastic Processes, 40-57.
Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV'11) (LNCS, Vol. 6806). Springer, 585-591.
Marta Kwiatkowska, Gethin Norman, and David Parker. 2019. Verification and Control of Turn-Based Probabilistic Real-Time Games. Lecture Notes in Computer Science 11760, 379-396.
Marta Kwiatkowska, Gethin Norman, David Parker, and Gabriel Santos. 2019. Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games. In Proceedings of FM 2019 (Lecture Notes in Computer Science, Vol. 11800). Springer, 298-315.
Marta Kwiatkowska, Gethin Norman, David Parker, and Gabriel Santos. 2021. Automatic Verification of Concurrent Stochastic Systems. Formal Methods in System Design 58, 1 (2021), 188-250.
François Laroussinie and Nicolas Markey. 2015. Augmenting ATL with Strategy Contexts. Information and Computation 245 (2015), 98-123.
François Laroussinie, Nicolas Markey, and Ghassan Oreiby. 2006. Model-Checking Timed ATL for Durational Concurrent Game Structures. In Proceedings of FORMATS'06 (Lecture Notes in Computer Science, Vol. 4202). Springer, 245-259.
Alessio Lomuscio, Wojciech Penczek, and Hongyang Qu. 2010. Partial Order Reductions for Model Checking Temporal-Epistemic Logics over Interleaved Multi-Agent Systems. Fundam. Informaticae 101, 1-2 (2010), 71-90.
A. Lomuscio, H. Qu, and F. Raimondi. 2015. MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems. International Journal on Software Tools for Technology Transfer 24 (2015), 84-90. Available online.
Gethin Norman, David Parker, and Jeremy Sproston. 2013. Model Checking for Probabilistic Timed Automata. Formal Methods in System Design 43, 2 (2013), 164-190.
Wojciech Penczek and Agata Pólrola. 2006. Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. Studies in Computational Intelligence, Vol. 20. Springer.
Lutz Priese. 1983. Automata and Concurrency. Theoretical Computer Science 25, 3 (1983), 221-265.
Pierre-Yves Schobbens. 2004. Alternating-Time Logic with Imperfect Recall. In Proceedings of LCMAS'03, Vol. 85(2). 1-12.
Moshe Y. Vardi. 1985. Automatic Verification of Probabilistic Concurrent Finite-State Programs. In Proceedings of FOCS'85. IEEE Computer Society, 327-338.
Rui Yan, Gabriel Santos, Gethin Norman, David Parker, and Marta Kwiatkowska. 2024. Partially Observable Stochastic Games with Neural Perception Mechanisms. In Proceedings of FM'24. Springer, 363-380.