www.prismmodelchecker.org
[JKP+25] Wojciech Jamroga, Marta Kwiatkowska, Wojciech Penczek, Laure Petrucci and Teofil Sidoruk. Probabilistic Timed ATL. In Proc. 24th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'25). To appear. May 2025. [pdf] [bib] [Proposes a probabilistic extension of alternating-time timed temporal logic, with an implementation building on PRISM and IMITATOR.]
Downloads:  pdf pdf (636 KB)  bib bib
Links: [Google] [Google Scholar]
Abstract. 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 PTATLirp, and in 2EXPTIME for PTATLirP. We demonstrate the practical feasibility of verification for PTATLirp formulas through a novel proof of-concept combination of state-of-the-art tools IMITATOR and PRISM on a scalable benchmark, with encouraging results.

Publications