Probabilistic Timed ATL

Wojciech Jamroga (Institute of Computer Science, Polish Academy of Sciences & SnT, University of Luxembourg), Marta Kwiatkowska (Institute of Computer Science, PAS & Department of Computer Science, University of Oxford), Wojciech Penczek (Institute of Computer Science, Polish Academy of Sciences), Laure Petrucci (LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord), Teofil Sidoruk (Institute of Computer Science, Polish Academy of Sciences)

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 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.