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