EU Horizon 2020
Horizon 2020
HomeNewsResearch ThemesPeopleKey Prior PublicationsPublicationsWorkshop
[JKP+25] Wojciech Jamroga, Marta Kwiatkowska, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk. Probabilistic Timed ATL. In Proc. at 24th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2025). 2025. [pdf] [bib]
Downloads:  pdf pdf (636 KB)  bib bib
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.