PSTCTL Semantics

Context

Jamroga2026 - Towards Probabilistic Strategic Timed CTL defines PSTCTL as a branching-time logic combining coalition ability, real-time bounds, and probabilistic thresholds over paths. This annex collects the syntax and the key semantic clause so the main source and concept notes can stay readable.

Formal Statement

The paper’s syntax separates state formulas \varphi from path formulas \gamma:

$$\phi ::=p\mid \neg \phi \mid \phi \wedge \phi \mid ⟨⟨A⟩⟩\gamma ,$$ $$\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 .$$

The characteristic semantic clause is the strategic probabilistic modality:

$$M,(s,v)\models ⟨⟨A⟩⟩P_{\bowtie z}\psi$$

iff there exists a joint strategy \sigma_A for coalition A such that every outcome distribution induced by \sigma_A from concrete state (s,v) assigns probability related to z by \bowtie to the set of paths satisfying \psi.

Timed until and release are evaluated over dense time. For example,

$$M,\rho \models {\gamma }_1{U}_I{\gamma }_2$$

holds iff some r \in I satisfies M,\pi_\rho(r) \models \gamma_2 and every earlier r' < r satisfies M,\pi_\rho(r') \models \gamma_1.

Derivation / Construction

• \langle\!\langle A \rangle\!\rangle contributes the ATL-style strategic quantification over coalitions.
• U_I and R_I contribute the TCTL-style real-time bounding of temporal operators.
• P_{\bowtie z} contributes the PCTL-style threshold over path probabilities.
• The intended models are probabilistic continuous-time asynchronous multi-agent systems (PCAMAS), where agents are represented by probabilistic timed automata composed asynchronously with synchronization on shared actions.
• The feasibility study focuses on irP strategies: imperfect-information, memoryless, probabilistic policies over local actions.

Implications

• PSTCTL can express specifications that are awkward in the wiki’s current LTL-heavy cluster because it reasons about branching futures and coalition power, not only single traces.
• The logic is a natural fit for verification questions in strategic multi-agent systems where deadlines and uncertainty matter simultaneously.
• The semantics also help explain why model checking is expensive: the verifier must account for time, nondeterminism, stochasticity, and strategy choice at once.

Links

• Probabilistic Strategic Timed CTL
• Jamroga2026 - Towards Probabilistic Strategic Timed CTL
• Temporal Logic
• Formal Methods
• Strategic Reasoning