Draft:Continuous Stochastic Logic

Continuous Stochastic Logic (CSL) is a formalism for expressing properties of continuous time Markov chains (CTMCs). It enhances the classical temporal logic frameworks by incorporating quantitative aspects of systems that exhibit continuous-time stochastic behavior. CSL is used primarily in Probabilistic Model Checking (PMC), where it enables automatic verification of properties over CTMCs.

CSL Syntax

A possible syntax of CSL can be defined as follows:

${\displaystyle \Phi$ ::=a\mid \neg \Phi \mid \Phi \land \Phi \mid {\mathcal {P}}_{\sim \lambda }(\phi )\mid {\mathcal {S}}_{\sim \lambda }(\phi )}

${\displaystyle \phi$ ::={\texttt {X}}\Phi \mid \Phi {\mathcal {U}}^{I}\Phi }

Therein, $a\in A$ for some finite set $A$ of atomic propositions, $\sim \in \{<,\leq ,\geq ,>\}$ is a comparison operator, $I$ is an interval of $\mathbb {R} _{\geqslant 0}$ and $\lambda$ is a probability threshold. Let ${\mathcal {P}}_{\sim \lambda }(\phi )$ indicate that the probability of a path formula $\phi$ being satisfied from a given state satisfies bound ${\sim \lambda }$, and let ${\mathcal {S}}_{\sim \lambda }(\phi )$ indicate the steady-state probability of the same.

Formulas of CSL are interpreted over continuous-time Markov chains. An interpretation structure is a quadruple $K=\langle S,s^{i},{\mathcal {T}},L\rangle$, where

• $S$ is a finite set of states,
• $s^{i}\in S$ is an initial state,
• ${\mathcal {T}}$ is a transition probability function based on specified reaction rates, ${\mathcal {T}}:S\times S\to [0,1]$, such that for all $s\in S$ we have $\sum _{s'\in S}{\mathcal {T}}(s,s')=1$, and
• $L$ is a labeling function, $L:S\to 2^{A}$, assigning atomic propositions to states.