Probabilistic Strategic Timed CTL

Definition

PSTCTL is a branching-time temporal logic that combines ATL-style coalition modalities, TCTL-style real-time bounds, and PCTL-style probability thresholds. In the formulation summarized by the current source note, state and path formulas are built from

$$\phi ::=p\mid \neg \phi \mid \phi \wedge \phi \mid ⟨⟨A⟩⟩\gamma ,$$

and

$$\gamma ::=\phi \mid \neg \gamma \mid \gamma \wedge \gamma \mid P_{\bowtie z}\gamma U_I\gamma \mid P_{\bowtie z}\gamma R_I\gamma .$$

Intuitively, \langle\!\langle A \rangle\!\rangle P_{\bowtie z} F_I \psi says that coalition A has a strategy ensuring that \psi is reached within interval I with probability meeting threshold z.

Why It Matters

This logic is useful when one needs all of the following at once: explicit coalition ability, timed requirements, and uncertainty. That combination is common in verification problems for multi-agent coordination, partially observed control, and safety specifications that cannot be stated as purely deterministic trace properties.

Formalism / Key Objects

• Coalitions A equipped with strategies.
• Probability thresholds P_{\bowtie z} over path sets.
• Real-time intervals I \subseteq \mathbb{R}_{\ge 0} constraining temporal operators.
• Timed until and release operators, with F_I and G_I as derived forms.
• Interpretation over probabilistic continuous-time asynchronous multi-agent systems (PCAMAS).
• A practically important strategy class is irP: imperfect-information, memoryless, probabilistic strategies that map local states to action distributions.
• The heavier syntax-and-semantics details are collected in PSTCTL Semantics.

Connections

• Extends the wiki’s existing Linear Temporal Logic material from linear-time trace constraints to Branching-Time Temporal Logic under strategic uncertainty.
• Sits naturally in Formal Methods because it is a model-checking-oriented specification language rather than only a conceptual vocabulary item.
• Connects to Strategic Reasoning because truth is defined by what coalitions can enforce.
• Relevant to Temporal Logic when the specification needs both explicit deadlines and stochastic guarantees.
• The accompanying artifact PSTCTL Semantics records the core formulas without overloading this concept note.

Common Confusions

• PSTCTL is not just LTL with probabilities added; it is branching-time and explicitly quantifies over coalition strategies.
• The probability threshold constrains the measure of satisfying paths under a strategy, not merely the frequency of states in one trace.
• The current feasibility results focus on irP strategies; they do not by themselves settle the full expressivity or scalability story.

Key Sources

• Jamroga2026 - Towards Probabilistic Strategic Timed CTL