Towards Probabilistic Strategic Timed CTL

TL;DR

The paper addresses the need to reason about probabilistic strategic properties in continuous-time asynchronous multi-agent systems. It proposes PSTCTL, a probabilistic branching-time logic that extends STCTL with a probabilistic path operator and a strategic modality suitable for imperfect-information strategies, interpreted over PCAMAS. The authors formalize the syntax and semantics, including irP memoryless strategies and continuous-time intervals, and demonstrate practical model checking through a parametric encoding and PRISM-based experiments, notably a Train-Gate-Controller benchmark. While the approach verifies probabilistic strategic properties with irP strategies, it also uncovers scalability limitations that motivate future work on efficiency, abstractions, and a deeper analysis of expressive power and complexity. Overall, the work lays groundwork for probabilistic strategic verification in real-time multi-agent systems and informs subsequent tool development and theoretical study.

Abstract

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.

Figures (1)

• Figure 1: Probabilistic choice in the PRISM model for $n=4$.