Draft:Continuous Stochastic Logic

A possible syntax of CSL can be defined as follows:^[3]

Therein, ${\displaystyle a\in A}$ for some finite set ${\displaystyle A}$ of atomic propositions, ${\displaystyle \sim \in \{<,\leq ,\geq ,>\}}$ is a comparison operator, ${\displaystyle I}$ is an interval of ${\displaystyle \mathbb {R} _{\geqslant 0}}$ and ${\displaystyle \lambda }$ is a probability threshold. Let ${\displaystyle {\mathcal {P}}_{\sim \lambda }(\phi )}$ indicate that the probability of a path formula ${\displaystyle \phi }$ being satisfied from a given state satisfies bound ${\displaystyle {\sim \lambda }}$, and let ${\displaystyle {\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 ${\displaystyle K=\langle S,s^{i},{\mathcal {T}},L\rangle }$, where

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