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
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

Metatheory. PCTL model checking is polynomial in model size. Probability computation uses linear algebra (matrix methods). CSL requires solving differential equations. For MDPs, linear programming computes optimal probabilities. Decidable and practical for finite-state systems. Simulation-based methods for large/infinite state.

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

Limitations. State explosion with large systems. Numerical precision issues. Probability values may be hard to specify. CTMCs assume exponential distributions. Model abstraction required for scalability. Continuous state spaces need approximation. Doesn't handle all probability distributions.