Probabilistic Timed ATL

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.

Authors

• Wojciech Jamroga Institute of Computer Science, Polish Academy of Sciences and Faculty of Mathematics and Computer Science & Institute of Advanced Studies, Nicolaus Copernicus University in Torun
• Marta Kwiatkowska Institute of Computer Science, PAS & University of Oxford
• Wojciech Penczek ICS, Polish Academy of Sciences
• Laure Petrucci LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord
• Teofil Sidoruk Institute of Computer Science, Polish Academy of Sciences

Keywords

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