Towards Probabilistic Strategic Timed CTL

We define PSTCTL, a probabilistic variant of Strategic Timed CTL (STCTL), interpreted over stochastic multi-agent systems with continuous time and asynchronous execution semantics. STCTL extends TCTL with strategic operators in the style of ATL. Moreover, we demonstrate the feasibility of verification with irP-strategies.

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

• model checking
• probabilistic systems
• strategic ability
• real time