Stochastic Logic

Origin. Probabilistic model checking emerged 1990s. PCTL (Hansson & Jonsson, 1994) adds probability to CTL. CSL (Aziz et al., 1996) extends to continuous-time. Developed for analyzing randomized algorithms and stochastic systems. PRISM tool (2002) made practical verification possible.

Models. Temporal properties with probability bounds. Systems with randomness: probabilistic choices, stochastic timing. PCTL: "with probability ≥ 0.99, eventually reach goal." CSL: "probability of reaching error within 10 time units < 0.01." Quantitative verification: not just yes/no but probability values.

Formalism.

Discrete-time Markov chains (DTMCs): M = (S, P, L) where P: S × S → [0,1] is transition probability.

PCTL syntax: State formulas: φ ::= true | a | ¬φ | φ ∧ ψ | P∼p[ψ] Path formulas: ψ ::= Xφ | φ U φ | φ U≤k φ

P≥p[ψ] — "probability of ψ-paths is ≥ p"

PCTL semantics: s ⊨ P∼p[ψ] iff Prob(s, ψ) ∼ p where Prob(s, ψ) = probability measure of paths from s satisfying ψ.

Examples:

P≥0.99[F goal] — reach goal with prob ≥ 0.99
P≤0.01[F≤100 error] — error within 100 steps has prob ≤ 0.01
P=?[G safe] — compute probability of always safe

CSL (Continuous Stochastic Logic): For continuous-time Markov chains (CTMCs). Adds time bounds: P≥p[φ U[t₁,t₂] ψ] Steady-state: S∼p[φ] — in steady state, φ holds with prob ∼ p.

Markov Decision Processes: Nondeterminism + probability. Pmax, Pmin — optimize over adversary choices.

Symbols.

Symbol	Unicode	Name	Meaning
P∼p	—	Probability bound	Prob ∼ p
∼	U+223C	Tilde operator	Placeholder for one of ≥, >, ≤, <
X	—	Next	Next state
U	—	Until	Until
U≤k	—	Bounded until	Within k steps
F	—	Finally	Eventually
G	—	Globally	Always
S∼p	—	Steady-state	Long-run probability
Pmax, Pmin	—	Extremal	Optimal probability
P=?	—	Quantitative query	Compute the probability rather than test it
M	—	Model	The chain, M = (S, P, L)
S	—	State space	The states of the chain
P	—	Transition function	P : S × S → [0,1]
L	—	Labelling	Atomic propositions true at a state
s	—	State	A particular state of the chain
Prob	—	Path measure	Measure of the paths satisfying a path formula
φ	U+03C6	Greek small phi	Schematic state formula
ψ	U+03C8	Greek small psi	Schematic path formula
→	U+2192	Rightwards arrow	Function arrow, as in P : S × S → [0,1]
a	—	Atomic proposition	A label drawn from L
::=	—	Production	Grammar rule for the syntax
⊨	U+22A8	True / Double turnstile	Satisfaction of a formula at a state
¬	U+00AC	Not sign	Negation
∧	U+2227	Logical and	Conjunction
×	U+00D7	Multiplication sign	Cartesian product in S × S
≥	U+2265	Greater-than or equal to	Lower probability bound
≤	U+2264	Less-than or equal to	Upper probability bound
[t₁,t₂]	—	Time interval	Bound on the CSL until operator
\|	—	Vertical line	Alternation in the grammar

Metatheory. Over a finite DTMC, PCTL model checking is polynomial in the number of states and linear in the formula: unbounded until reduces to a linear equation system once the states of probability 0 and 1 are found by graph search, step-bounded until to k matrix-vector products. The qualitative fragment, where the only bounds are P>0 and P=1, depends on the transition graph alone and not on the numerical probabilities, so it is decided by reachability. For MDPs the semantics quantifies over schedulers; maximum reachability is a linear program and its decision problem is P-complete (Papadimitriou and Tsitsiklis 1987), with memoryless deterministic schedulers optimal for unbounded reachability but not for bounded or multi-objective properties. Expressiveness is calibrated exactly by bisimulation: Aziz et al. (1995) proved two states of a finite chain probabilistically bisimilar iff they satisfy the same PCTL formulas, and Baier, Katoen, Hermanns and Wolf (2005) proved the same for CSL on CTMCs. Moving to linear time costs formula complexity rather than model complexity: Courcoubetis and Yannakakis (1995) showed LTL model checking of a Markov chain polynomial in the chain, exponential in the formula and PSPACE-complete overall, while for MDPs it is 2EXPTIME-complete.

Applies to. Randomized algorithm verification. Network protocol analysis. Biological systems modeling. Reliability engineering. Security (probabilistic anonymity). Performance evaluation. Cyber-physical systems.

Limitations. PCTL is branching-time and inherits the gap between CTL and LTL: probabilistic fairness and ω-regular path conditions lie outside it, and PCTL* closes the gap only by moving formula complexity from linear to exponential for chains and doubly exponential for MDPs. Quantitative operators range over the whole reachable state space, so state explosion belongs to the semantics rather than to an implementation: a symbolic encoding compresses the representation, not the number of equations. Nondeterminism and probability do not compose freely — the meaning of P∼p over an MDP depends on which schedulers are admitted, and that class must be stipulated; under partial observation the qualitative problem becomes undecidable (Baier, Bertrand and Größer 2008), as does the value-1 problem for probabilistic automata (Gimbert and Oualhadj 2010). In continuous time the bounded-until probability is transcendental and computed only to a stated error, so a threshold test is answered soundly only when p is bounded away from the true value; and CTMCs presuppose exponential residence times, general distributions requiring semi-Markov models that lose the memorylessness making transient analysis a matrix exponential.