This chapter answers the question the previous one left open: after modelling a system with probabilities and rates, how do we verify properties of it? Deck 08, "Stochastic analysis and prediction: from model checking to simulation", builds the answer on logics. The formal framework first:
"A logic defines a notion of 'validity' of a sentence in a 'model'. It can be used as a philosophical concept, or in science/engineering: in science/engineering it is used to state what does it mean that (and sometimes compute whether) a system (model) enjoys a certain property."
Several logics exist, "each focusing on certain classes of properties and certain system 'observables'". A logic has two ingredients: syntax — a set of admissible formulas F = {ϕ0, ϕ1, ...}, typically defined by a grammar — and semantics — a pair ⟨M, ⊨⟩ where M is a set of models and ⊨ ⊆ M × F is the satisfaction relation (also called validity). The notation M ⊨ ϕ reads: property ϕ is valid for system M (or: M is a model for ϕ).
The deck assigns logics three roles — a classification that will structure any exam discussion:
The starting point is propositional logic, whose grammar is ϕ ::= p | T | F | ¬ϕ | ϕ∧ϕ | ϕ∨ϕ | ϕ→ϕ, where p is any propositional symbol that can be judged true or false — "variable v is 0", "place p has 1 token", and so on. The semantics is the usual truth tables: M is a function associating proposition symbols to validity states. But propositional logic is static: "in standard logic, like propositional logic, propositions hold or not, and this does not depend on any concept of system evolution — the system is static". The models of this course evolve, so the logics must talk about evolution — that is the step of the next section.
Static logics are not enough for evolving systems: "we need logics in which the model is based on a rewrite system, and can express whether something happens in the next state, in all states, in some state, and so on."
LTL (Linear Temporal Logic) "adds modal operators G, F, U (globally, eventually, until)" and "defines validity over a single path; whole systems are considered by verifying validity over all paths". Model checking "explores by brute force, handling finite-state systems (with cycles)": "as a loop is encountered, MC stops searching and smartly derives the right conclusion", and "the key difficulty of MC is that formulas can nastily be 'recursive'".
The move of the lecture: "From linear time to branching time: LTL flattens a system (graph) into a set of linear paths; CTL (Computational Tree Logic) considers the branching structure of time." Where LTL sees one timeline per path, CTL sees the tree of all futures from a state — and its quantifiers alternate with the temporal operators. The syntax distinguishes state formulas ϕ from path formulas ψ:
ϕ ::= p | T | F | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ → ϕ | Aψ | Eψ
ψ ::= Xϕ | Gϕ | Fϕ | ϕUϕAψ (or ∀ψ) — "in all paths" (from here);Eψ (or ∃ψ) — "for at least one path" (from here);X — next; G — globally (always); F — eventually; U — until;The expressiveness intuition is given on a system with just two paths, s0 → s1 → s2 and s0 → s3 → s4 → s5:
AG ϕ — ϕ should hold from s0, s1, s2, s3, s4, s5 (every state of every path);EG ϕ — ϕ should hold from s0, s1, s2 or from s0, s3, s4, s5 (one whole path);AX ϕ — ϕ should hold from s1, s3 (all immediate successors);EX ϕ — ϕ should hold from s1 or s3 (some immediate successor);AF ϕ — ϕ should hold from (s0 or s1 or s2) and (s0 or s3 or s4 or s5) (every path eventually hits it);EF ϕ — ϕ should hold from s0 or s1 or s2 or s3 or s4 or s5 (some path hits it).With the crucial caveat: "'ϕ should hold from s' really means that ϕ can be itself modal, and should check its validity from all/some paths starting from s, recursively."
A/E with X/G/F/U. The two-path example fixes the reading of each of the eight combinations — the vocabulary used in section 3 for the channel.The semantics of CTL is recursive, defined by s ⊨ ϕ. The deck gives the (semi-)formal clauses for the A fragment:
s ⊭ F
s ⊨ p iff predicate p holds in state s alone
s ⊨ ϕ → ϕ′ iff s ⊨ ϕ implies s ⊨ ϕ′
s ⊨ AX ϕ iff s → s′ ⇒ s′ ⊨ ϕ
s ⊨ AG ϕ iff s ⊨ ϕ ∧ ∀s′ s.t. s → s′, s′ ⊨ AG ϕ
s ⊨ AF ϕ iff s ⊨ ϕ ∨ ∀s′ s.t. s → s′, s′ ⊨ AF ϕ
s ⊨ A[ϕUϕ′] iff s ⊨ ϕ′ ∨ (s ⊨ ϕ ∧ ∀s′ s.t. s → s′, s′ ⊨ A[ϕUϕ′])Note the self-reference: AG, AF and A[ϕUϕ′] are defined in terms of themselves at the successors — that is the "nastily recursive" difficulty of the previous section, and the reason model checkers must compute these as fixpoints (and why cycles are handled "smartly": on a loop, the search stops and derives the conclusion).
The deck then shows that most of the language is syntactic sugar: AX ϕ ≡ ¬EX ¬ϕ, AG ϕ ≡ ¬EF ¬ϕ, EG ϕ ≡ ¬AF ¬ϕ, AF ϕ ≡ A[TUϕ], and ¬ϕ ≡ ϕ → F, ϕ ∨ ϕ′ ≡ ¬ϕ → ϕ′, ϕ ∧ ϕ′ ≡ ¬(¬ϕ ∨ ¬ϕ′). Hence "E, G, F, ∧, ∨, ¬ are just syntactic sugar — could stick to syntax: ϕ ::= p | F | ϕ→ϕ | Aψ, ψ ::= Xϕ | ϕUϕ".
The chapter-9 graph — states s0..s3, predicates try, fail, succ as simple queries on states — yields the four canonical formulas of the lecture:
⊭ AF succ success is never guaranteed
⊨ EF succ success is possible
⊨ AG (fail → EF succ) failure does not prevent future success
⊨ AG EF succ success is possible at any pointRead them against the graph: AF succ fails because the loop s1 → s1 (or the absorbing s3 → s3, if succ does not hold there) admits a path that never reaches success; EF succ holds because a path to success exists; AG (fail → EF succ) holds because every state in which failure holds can still reach success; and AG EF succ holds because every reachable state can reach success — which requires succ to hold at the absorbing s3 as well (otherwise EF succ would be false there, and AG would fail).
AG EF succ is the subtle one: because s3 is absorbing, the formula holds only if succ holds at s3 — the recursive, fixpoint nature of the semantics is not optional.Each CTL formula is a recursive query: AG ϕ is "ϕ everywhere reachable", EF ϕ is "ϕ reachable", AF ϕ is "ϕ inevitable on every path", EG ϕ is "ϕ can be kept forever". The widget above computes exactly those queries on the channel graph. This is also the bridge to verification: a model checker is just a very efficient engine for these recursive queries — the topic of section 5 and section 6.
The second example of the lecture is the Readers & Writers Petri Net of chapter 9, section 7, with predicates over the number of tokens in the places p1..p7. The six formulas of the deck are a complete vocabulary of safety and liveness:
Reachability from the initial state: ⊨ AF (p2 > 0)
Safety: ⊨ AG ¬(p6 > 0 ∧ p7 > 0)
Inevitable reachability from any state: ⊨ AG AF (p6 > 0 ∨ p7 > 0)
Requests are not necessarily granted: ⊨ ¬AG (p3 > 0 → AF (p6 > 0))
Requests may be granted: ⊨ AG (p3 > 0 → EF (p6 > 0))
However: ⊨ AG ((p3 + p4 > 0) → AF (p6 + p7 > 0))Read each one as a design requirement. AF (p2 > 0) — a request eventually appears. AG ¬(p6 > 0 ∧ p7 > 0) — the safety property: never both reading and writing (this is the inhibitor-arc property of the net, now expressed as a formula, exactly the VERIFIER lab task of chapter 9, section 10). AG AF (p6 > 0 ∨ p7 > 0) — from any state, some reader or writer is eventually active (no deadlock). The pair on requests is the subtle one: AG (p3 > 0 → AF (p6 > 0)) would claim that every reader request is eventually granted, which the model does not guarantee (a writer can keep winning the race) — hence ⊨ ¬AG(...); but AG (p3 > 0 → EF (p6 > 0)) — a reader request may be granted — does hold, as does the combined liveness AG ((p3 + p4 > 0) → AF (p6 + p7 > 0)) — a pending request of either kind eventually leads to some active read or write. This distinction between "may" (EF) and "eventually" (AF) is exactly the distinction between possibility and liveness that CTL is built to draw.
Be able to translate a natural-language requirement into CTL and back. The pattern: safety = AG ¬(bad); reachability = EF (good); liveness/inevitability = AF (good) or AG AF (good); conditioned properties use → inside. And be able to explain why the readers/writers net satisfies "may be granted" but not "eventually granted": the CTMC rates of chapter 10, section 7 decide the probabilities, but the structure of the net decides possibility — which is exactly the gap PCTL closes in the next section.
CTL asks "is there a path?"; with probabilities in the model, the question becomes "what is the probability of the paths?". The deck frames it as the model-checking problem for DTMCs:
"After you described the DTMC, you may want to know: what is the probability that a certain state is eventually reached? that a certain state is reached within N steps? that if a state s1 is reached, then also s2 is reached within N steps?"
"Model checking: if the number of states is finite, by brute force we can find an answer in spite of cycles, since the path probability is simply computed as the product of single transitions, and smart MC algorithms easily intercept and manage those cycles. A suitable logic is of course to be identified."
The logic is PCTL (Probabilistic Computation Tree Logic): "It uses as model a DTMC (a RS with also probabilities on transitions). Instead of modal operators A and E (meaning 'all' or 'at least one' path) have a P_J operator, where J is an interval into [0, 1] (e.g. J = [0, 0.5], also written '≤ 0.5')."
P≤0.5 ψmeans that the probability of ψ is ≤ 0.5, i.e.: take all (finite, infinite) paths where ψ is true · sum the probabilities of such paths · check if the result is in J.
PCTL also adds a bounded until operator U≤n which limits the number of steps within which something should happen — "consequently, G≤n, F≤n are derived". The syntax and semantics:
ϕ ::= p | ϕ → ϕ | F | P_J(ψ) (.. | true | ¬ϕ | ϕ ∧ ϕ | ...)
ψ ::= Xϕ | ϕUϕ′ | ϕU≤n ϕ′ (.. | ϕU≥n ϕ′ | F≤n ϕ | ...)
J ::= [p, q] | ]p, q[ | ]p, q] | [p, q[ (.. | ≤ p | < p | ≥ p | > p)
s ⊨ P_J(ψ) iff Pr{π ∈ Path(s) | π ⊨ ψ} ∈ J
π ⊨ Xϕ iff π[1..] ⊨ ϕ
π ⊨ ϕUϕ′ iff ∃j, π[j..] ⊨ ϕ′ ∧ ∀i, i < j, π[i..] ⊨ ϕ
π ⊨ ϕU≤n ϕ′ iff ∃j, j ≤ n, π[j..] ⊨ ϕ′ ∧ ∀i, i < j, π[i..] ⊨ ϕThe derived operators come with an important caveat: P_J(¬(ϕUϕ′)) is not a PCTL formula — "hence you can say that Fϕ ≡ trueUϕ, but cannot say that Gϕ ≡ ¬F¬ϕ!" However, the probability of the negation can still be expressed: P_J(¬ϕ) ≈ P_J̄(ϕ), where J̄ = [0, 1] \ J — e.g. P≥p(¬ϕ) ≈ P<p(ϕ). The usable equivalences are:
P_J(Fϕ) ≡ P_J(trueUϕ)
P_J(F≤n ϕ) ≡ P_J(trueU≤n ϕ)
P_J(Gϕ) ≡ P_J(F¬ϕ)
P_J(G≤n ϕ) ≡ P_J(F≤n ¬ϕ)The deck's example is a message-sending system with failure and waiting — the DTMC of the next section — and its queries mix probability thresholds, time bounds and nesting:
P≥0.99999 (tU≤10 s3) — with probability ≥ 0.99999, while trying, success within 10 steps
P≥0.99999 (F≤10 s3) — same, expressed as bounded eventually
P≤0.00001 (G≤10 ¬s3) — the dual: failure to succeed within 10 steps is nearly impossible
P≥0.99 [F (s2 → P≥0.9 [F≤5 s3])] — nested: with prob ≥ 0.99, eventually, if a retry happens,
then with prob ≥ 0.9 success follows within 5 stepsP_J operator replaces A/E by summing the probabilities of the satisfying paths; the bounded until limits the horizon; and the derived operators come with the caveat that G cannot be defined by negation inside P_J. The message-sending queries of the deck are all answered "yes" — and the widget verifies the numbers.The lecture now introduces the tool that does "all this": PRISM (http://www.prismmodelchecker.org). The deck's assessment is a study in what a research tool should be: "It is one of the most known probabilistic analysis [tools]... and a reference example of how a research tool needs to be." Its characteristics:
P=? [..] queries);The message-sending model, as a PRISM dtmc module: one integer variable s in [0..3], probabilistic transitions on s=1 (0.01 stay, 0.01 retry, 0.98 succeed), s=2 goes back to s=0 (waiting), s=3 is absorbing. The properties tab then answers the queries — including the numerical one, which matches the widget of section 5 exactly:
P>0.9999 [ (true) U<=10 (s=3) ] → Yes
P=? [ (true) U<=10 (s=3) ] → 0.999998968..Experiments make the parameter explicit: "declare a property parametric in a parameter (typically the time-bound); declare the values this property can get; an experiment is an iteration of various model-checking instances" — e.g. P=? [(true) U<=k (s=3)] with k ∈ [0, 10.0] step 0.1, producing a chart of probability versus time bound. (Note the deck writes k as a real here; the bounded-until index of PCTL is a step count, and PRISM treats the bound accordingly.)
P>0.9999 → Yes) and numerical (P=? → 0.999998968) queries, and experiments sweep a parameter to chart probability against the bound. The same language handles the 12 166-state readers/writers CTMC.The DTMC of the message-sending example. The syntax is plain: one module, one variable, guarded probabilistic transitions. Queries in the properties tab:
P>0.9999 [ (true) U<=10 (s=3) ] → Yes
P=? [ (true) U<=10 (s=3) ] → 0.999998968..dtmc
module msg
s : [0..3] init 0;
[] s=0 -> 1 : (s'=1);
[] s=1 -> 0.01 : (s'=1) +
0.01 : (s'=2) +
0.98 : (s'=3);
[] s=2 -> 1 : (s'=0);
[] s=3 -> 1 : (s'=3);
endmoduleState 1 is "trying": with probability 0.98 the message is delivered, with 0.01 it waits (returns to 0) and with 0.01 it retries. State 3 is absorbing — success.
The same system as a ctmc: the probabilities become rates (0.1, 0.1, 10 — the "10" dominating the delivery), and the queries use continuous time bounds:
P=? [ (true) U<=1 (s=3) ] → 0.5877
S=? [ !s=3 ] → 0ctmc
module msg
s : [0..3] init 0;
[] s=0 -> 1 : (s'=1);
[] s=1 -> 0.1 : (s'=1) +
0.1 : (s'=2) +
10 : (s'=3);
[] s=2 -> 100 : (s'=0);
[] s=3 -> 1 : (s'=3);
endmoduleThe queries of section 7: P≥0.5 (tU≤1.0 s3) holds (0.5877 ≥ 0.5), and the steady-state probability of not being in success is 0 — in the long run, success is reached almost surely.
The stochastic Readers & Writers Petri Net of chapter 10, section 7 as a PRISM ctmc — "a model of 12'166 states" for N = 20 readers/writers. Each place becomes a bounded counter; each transition a guarded, rated command:
ctmc
const int N = 20;
module RW
p1 : [0..N] init N;
p2 : [0..N] init 0;
p3 : [0..N] init 0;
p4 : [0..N] init 0;
p5 : [0..N] init 1;
p6 : [0..N] init 0;
p7 : [0..N] init 0;
[t1] p1>0 & p2<N -> 1 : (p1'=p1-1)&(p2'=p2+1);
[t2] p2>0 & p3<N -> 200000 : (p2'=p2-1) & (p3'=p3+1);
[t3] p2>0 & p4<N -> 100000 : (p2'=p2-1) & (p4'=p4+1);
[t4] p3>0 & p5>0 & p6<N -> 100000 : (p3'=p3-1) & (p6'=p6+1);
[t5] p4>0 & p5>0 & p6=0 & p7<N -> 100000 : (p4'=p4-1) & (p5'=p5-1) & (p7'=p7+1);
[t6] p6>0 & p1<N -> p6*1 : (p6'=p6-1) & (p1'=p1+1);
[t7] p7>0 & p5<N & p1<N -> 0.5 : (p7'=p7-1) & (p1'=p1+1) & (p5'=p5+1);
endmodule
// example experiment: P=? [(true) U<=k (p6>0)]Note how the inhibitor arcs of the Petri Net become guards (p5>0 on t4, p6=0 on t5) and how the marking-dependent rate m(T) of chapter 10 becomes the expression p6*1 on t6.
PRISM's module language plays the role of the DSLs of chapter 9, section 8: numeric variables and guarded transitions are enough to model Petri Nets, hence chemical-like systems, and modules compose by synchronisation. The "no colours" remark is the deck's way of saying the meta-model stops where the ARTIST lab extension of chapter 9 (coloured tokens) would begin.
For CTMCs, the logic is CSL (Continuous Stochastic Logic). The model is "a RS structure with also rates on the accessibility relation" — "a small extension to standard transition systems: ⟨A, →⟩ where → ⊆ A × ℝ⁺₀ × A, edges labelled with rates; sanity condition: there is at most one arc from a to b". Semantics: "transition time follows a negative exponential distribution probability, with average time 1/r; memoryless property holds" — the CTMC of chapter 10, section 5.
CSL adds two operators on top of the PCTL machinery:
U^I which limits the time at which something should happen — I is a continuous time interval;S_J(ϕ) called the steady-state operator: "computes the probability that in the long run ϕ holds".ϕ ::= p | ϕ → ϕ | F | P_J(ψ) | S_J(ϕ) ψ ::= Xϕ | ϕUϕ′ | ϕU^I ϕ′
s ⊨ P_J(ψ) iff Pr{π ∈ Path(s) | π ⊨ ψ} ∈ J
s ⊨ S_J(ϕ) iff lim_{t→+∞} Pr{π ∈ Path(s) | π@t ⊨ ϕ} ∈ J
π ⊨ Xϕ iff π[1..] ⊨ ϕ
π ⊨ ϕUϕ′ iff ∃j ∈ ℕ, π[j..] ⊨ ϕ′ ∧ ∀i < j, π[i..] ⊨ ϕ
π ⊨ ϕU^I ϕ′ iff ∃τ ∈ ℝ⁺₀, τ < t, π⟨τ..⟩ ⊨ ϕ′ ∧ ∀τ′ < τ, π⟨τ′..⟩ ⊨ ϕ (with t ∈ I)The steady-state clause reads: the probability of being in a ϕ state at time t, as t goes to infinity, belongs to J. The example query of the lecture, on the CTMC version of the message model:
P≥0.5 (tU≤1.0 s3) — with probability ≥ 0.5, while trying, success within 1.0 time unit → holds
S≤0.1 (¬s3) — in the long run, the probability of not being in success is ≤ 0.1 → holdsPRISM computes the numerical answers: P=? [(true) U<=1 (s=3)] → 0.5877 and S=? [!s=3] → 0 — in the long run the probability of being outside success is zero, because the chain is eventually absorbed in s=3 with probability 1. The P≥0.5 query holds because 0.5877 ≥ 0.5; the S≤0.1 query holds because 0 ≤ 0.1.
U^I bounds the time (continuous interval), and the steady-state operator S_J asks about the long-run probability. The deck's two queries on the message CTMC both hold, with PRISM's numerical answers 0.5877 and 0.The lab deck states it as a rule: "the transition from TS to DTMC and then to CTMC should be followed at the logic level: this is LTL/CTL, then PCTL, and then CSL". One meta-meta-model, one logic: CTL quantifies paths of a transition system, PCTL measures paths of a DTMC, CSL measures timed paths of a CTMC and adds steady state. When a new analysis need appears in chapter 12, the same ladder is used to decide which tool applies.
The lecture compresses the whole toolbox into a stairway: three ways to analyse a stochastic system, ordered by how much of the state space they explore and how exact their answer is:
The approximate case is the interesting engineering one, and PRISM's approach is given precisely: use CSL to identify the run we are interested in, by formula ϕ; seek to compute the probability p that ϕ holds; let ε be the approximation of the result p (e.g. 0.01); let δ be the confidence of the result p (e.g. 0.001); then P[|r_sim − r_real| ≤ ε] ≥ (1 − δ). "ε and δ dictate N, or vice-versa, depending on the internal algorithm used: e.g. N = ln(2/δ)/(2ε²) (19'000 for ε, δ above)." The two parameters are the trade-off knobs: tightening the error or the confidence multiplies the number of runs.
PRISM's other mechanisms round out the picture: it assigns a numerical reward to each state/transition; you "can perform a simulation and chart rewards and/or variables"; "you can try to modelcheck to know what happens probabilistically"; and you can even perform bounded model checking — it does not explore the whole state space, performs a (possibly large) set of simulations, and "computes the confidence about the result and its accuracy — e.g. you have the 90% of probability that this result has 1% of accuracy". PRISM provides various simulation methods — CI, API, APMC (check the documentation).
N = ln(2/δ)/(2ε²) relates the two parameters; the exact constant depends on the algorithm's bound (the deck quotes ≈19 000 runs for ε = 0.01, δ = 0.001).The last part of the lecture shows the whole stairway implemented in the course's own toolkit: CTMCExperiment turns the simulation traces of chapter 10, section 6 into statistical experiments. A property is just a predicate over traces — an opaque type for readability:
object CTMCExperiment:
import CTMCSimulation.*
opaque type Property[A] = Trace[A] => Boolean
given rnd: Random = new Random
extension [S](self: CTMC[S])
// globally is simply achieved by equivalence: not G x = F not x
def eventually[A](filt: A => Boolean): Property[A] =
trace => trace exists (e => filt(e.state))
// takes a property and makes it time bounded by the magics of streams
def bounded[A](timeBound: Double)(prop: Property[A]): Property[A] =
trace => prop(trace takeWhile (_.time <= timeBound))
// a PRISM-like experiment, giving a statistical result (in [0,1])
def experiment(runs: Int, prop: Property[S], s0: S, timeBound: Double): Double =
(0 until runs).count: _ =>
bounded(timeBound)(prop)(self.newSimulationTrace(s0, rnd))
.toDouble / runsRead the three lines as the stairway in miniature: eventually is a property of a single trace (simulation reading); bounded truncates the trace at a time bound "by the magics of streams" — takeWhile on a LazyList (the laziness of chapter 10 pays off: the bound stops the simulation without overrunning); experiment counts, over runs fresh traces, how many satisfy the bounded property, and divides — this is approximate model checking, "a PRISM-like experiment, giving a statistical result (in [0,1])". The deck notes the eventually naming: "globally is simply achieved by equivalence: not G x = F not x" — the derived-operator caveat of section 5 in code.
The experiment on the stochastic channel sweeps the time bound from 0.1 to 10.0 in steps of 0.1, runs 26 000 simulations per bound, and charts the probability of having reached DONE against the bound:
object StochasticChannelExperiment extends App with de.sciss.chart.module.Charting:
import u08.modelling.CTMCExperiment.*
import u08.examples.StochasticChannel.*
val data =
for
t <- 0.1 to 10.0 by 0.1
p = stocChannel.experiment(
runs = 26000,
prop = stocChannel.eventually(_ == DONE),
s0 = IDLE,
timeBound = t.toDouble)
yield (t, p)
Time.timed:
println:
data.mkString("\n")
given ChartTheme = ChartTheme.Default
val chart = de.sciss.chart.api.XYLineChart(data)
chart.show("Probability")The resulting chart rises quickly and saturates near 1: within a few seconds the channel has almost surely completed — matching the theoretical expectation of about 1.5 seconds from chapter 10, section 7. This is exactly the PRISM P=? [(true) U<=k (s=3)] experiment of section 6, performed with the course's own tools; the 08-Lab task PRISM-VS-SCALA asks you to compare the two pipelines on the same model.
Simulation (newSimulationTrace), approximate model checking (experiment) and exact model checking (PRISM) answer the same question — "with what probability, within what time?" — at three points of the stairway. The Scala toolkit covers the first two and can emulate the third statistically; PRISM covers the second and third exactly. Chapter 12 extends the simulation side to kinetic Monte Carlo and to Alchemist for large-scale systems.
The lab deck (08-Lab) closes the analysis story: logics capture properties and their verification; "the transition from TS to DTMC and then to CTMC should be followed at the logic level: LTL/CTL, then PCTL, then CSL"; and the verification methods are model checking (exact), approximate model checking (with ε, δ) and simulation (a few runs, for complex systems). The tools: "need performance, hence, ad-hoc tools — PRISM (symbolic model checker), will see Alchemist as a general simulator."
u08 of https://github.com/mviroli/asmd-public-models). Get acquainted with all parts: utils (MSet "and also others"), modelling (CTMC, CTMCSimulation, CTMCExperiment as meta-meta-model; SPN and DAP as meta-model), examples (StochasticChannel, StochasticMutualExclusion, DAPGossip), and test. Check that all tests pass — "specifically checking CTMCExperiment".https://www.prismmodelchecker.org/). Play with the provided code, possibly directly on CTMCs; try to reproduce the runs shown in slides 26–29 (the DTMC and CTMC message models and queries); recall the progress: edit model, create property with parameters, run simulation, or experiment, or experiment with simulation.| Task | What it asks |
|---|---|
| PRISM | Make the stochastic Readers & Writers Petri Net of the lesson work in PRISM: perform experiments to investigate the probability that something good happens within a bound. Play with the PRISM configuration to inspect the steady-state probabilities of reading and writing ("may need to play with options, also choose 'linear equations method'"). |
| PRISM-VS-SCALA | Write Scala support for performing additional experiments and comparisons — e.g. G formulas and steady-state computations — and compare the numbers with PRISM on the same models. This is the empirical counterpart of section 9's claim that the Scala experiment is a PRISM-like approximate model checker. |
| LLM-STOCHASTIC-ANALYSIS | PRISM is rather well known, and perhaps LLMs know it. Can LLMs understand the meaning of a stochastic property? Can they solve (very) simple model checking? Can they preview what a simulation can produce? Compare with the LLM tasks of chapter 4 and chapter 9. |
The arc of this chapter is the arc of verification: requirements as formulas (specification), formulas checked against models (verification), and probabilities/rates as the quantitative extension. A strong presentation takes one model — the channel or the readers/writers net — and walks it through all four rungs: CTL properties (what is possible), PCTL/CSL properties (with what probability, within what time), PRISM (exact numbers), and the Scala experiment (approximate numbers with ε, δ). That is the complete answer to the "how do I verify?" question left open at the end of chapter 10.
The three roles: formalise requirements (specification), check if a design complies with requirements (verification), and check at runtime if a system behaviour complies with requirements (runtime verification). The two ingredients: syntax — a set of admissible formulas F = {ϕ0, ϕ1, ...} defined by a grammar — and semantics — a pair ⟨M, ⊨⟩ with M a set of models and ⊨ ⊆ M × F the satisfaction (validity) relation.
Its grammar is ϕ ::= p | T | F | ¬ϕ | ϕ∧ϕ | ϕ∨ϕ | ϕ→ϕ, where p is a propositional symbol judged true or false; the semantics is the usual truth tables. It is not enough because propositions hold or not independently of any concept of system evolution — "the system is static" — while the models of the course are rewrite systems.
LTL adds the modal operators G (globally), F (eventually), U (until) and defines validity over a single path; whole systems are considered by verifying validity over all paths. CTL (Computation Tree Logic) considers the branching structure of time: quantifiers A (all paths) and E (at least one path) alternate with X, G, F, U, giving 8 possibilities. LTL flattens a system into linear paths; CTL keeps the tree.
ϕ ::= p | T | F | ¬ϕ | ϕ∧ϕ | ϕ∨ϕ | ϕ→ϕ | Aψ | Eψ; ψ ::= Xϕ | Gϕ | Fϕ | ϕUϕ. On the system with paths s0→s1→s2 and s0→s3→s4→s5: AG ϕ holds from s0..s5; EG ϕ from (s0,s1,s2) or (s0,s3,s4,s5); AX ϕ from s1,s3; EX ϕ from s1 or s3; AF ϕ from both path-closures; EF ϕ from any state. "ϕ should hold from s" means ϕ can itself be modal, checked recursively from s.
s ⊨ AX ϕ iff s → s′ ⇒ s′ ⊨ ϕ. s ⊨ AG ϕ iff s ⊨ ϕ ∧ ∀s′ with s → s′: s′ ⊨ AG ϕ. s ⊨ AF ϕ iff s ⊨ ϕ ∨ ∀s′ with s → s′: s′ ⊨ AF ϕ. s ⊨ A[ϕUϕ′] iff s ⊨ ϕ′ ∨ (s ⊨ ϕ ∧ ∀s′ with s → s′: s′ ⊨ A[ϕUϕ′]). The self-reference is why model checking computes fixpoints and why cycles are handled "smartly".
E, G, F, ∧, ∨, ¬ are syntactic sugar: AX ϕ ≡ ¬EX ¬ϕ, AG ϕ ≡ ¬EF ¬ϕ, EG ϕ ≡ ¬AF ¬ϕ, AF ϕ ≡ A[TUϕ], ¬ϕ ≡ ϕ→F, ϕ∨ϕ′ ≡ ¬ϕ→ϕ′, ϕ∧ϕ′ ≡ ¬(¬ϕ∨¬ϕ′). The minimal syntax is ϕ ::= p | F | ϕ→ϕ | Aψ with ψ ::= Xϕ | ϕUϕ.
⊭ AF succ (success is never guaranteed), ⊨ EF succ (success is possible), ⊨ AG (fail → EF succ) (failure does not prevent future success), ⊨ AG EF succ (success is possible at any point). AF succ fails because a path such as s0→s1→s1→... avoids success forever; AG EF succ holds only if succ holds at the absorbing state s3 as well.
Reachability: ⊨ AF (p2 > 0). Safety: ⊨ AG ¬(p6 > 0 ∧ p7 > 0). Inevitable reachability: ⊨ AG AF (p6 > 0 ∨ p7 > 0). Requests not necessarily granted: ⊨ ¬AG (p3 > 0 → AF (p6 > 0)). Requests may be granted: ⊨ AG (p3 > 0 → EF (p6 > 0)). However: ⊨ AG ((p3+p4 > 0) → AF (p6+p7 > 0)).
Questions: the probability that a state is eventually reached, reached within N steps, or that s1 implies s2 within N steps. Brute force works on finite state spaces in spite of cycles because the path probability is simply the product of the single transition probabilities, and smart MC algorithms intercept and manage the cycles. A suitable logic — PCTL — is then identified.
s ⊨ P_J(ψ) iff Pr{π ∈ Path(s) | π ⊨ ψ} ∈ J: take all paths where ψ holds, sum their probabilities, check the interval J (e.g. ≤ 0.5). π ⊨ ϕU≤n ϕ′ iff ∃j ≤ n with π[j..] ⊨ ϕ′ and ∀i < j, π[i..] ⊨ ϕ. Derived: P_J(F≤n ϕ) ≡ P_J(trueU≤n ϕ) and P_J(G≤n ϕ) ≡ P_J(F≤n ¬ϕ).
P_J(¬(ϕUϕ′)) is not a PCTL formula, so F ϕ ≡ trueUϕ is fine but G ϕ ≡ ¬F ¬ϕ is not. The probability of the negation is still expressible: P_J(¬ϕ) ≈ P_J̄(ϕ) where J̄ = [0, 1] \ J — e.g. P≥p(¬ϕ) ≈ P<p(ϕ).
PRISM (prismmodelchecker.org) is one of the most known probabilistic analysis tools and a reference example of how a research tool should be: state transitions by numeric variables and probabilistic transitions (enough for Petri Nets, "no colours"), interacting modules, PCTL verification with numerical results, and CTMC support. The dtmc module msg has s : [0..3]; from s=1: 0.01 to s=1, 0.01 to s=2, 0.98 to s=3; queries P>0.9999 [(true) U<=10 (s=3)] → Yes and P=? [(true) U<=10 (s=3)] → 0.999998968..
CSL uses a CTMC as model and adds the bounded until U^I with a continuous time interval I, plus the steady-state operator S_J(ϕ): s ⊨ S_J(ϕ) iff lim_{t→+∞} Pr{π ∈ Path(s) | π@t ⊨ ϕ} ∈ J — the probability that in the long run ϕ holds. Example: P≥0.5 (tU≤1.0 s3) and S≤0.1 (¬s3) both hold on the message CTMC; PRISM computes P=? [(true) U<=1 (s=3)] → 0.5877 and S=? [!s=3] → 0.
Simulation: analysing one run (Gillespie or alike), the solution when the system is extremely complex. Model checking: analysing all runs (CSL as logic), exact but practical only for simple systems. Approximate model checking: analysing many runs statistically, each giving a yes/no result, with approximation ε and confidence δ: P[|r_sim − r_real| ≤ ε] ≥ (1 − δ); N = ln(2/δ)/(2ε²) relates runs to the two bounds.
Property[A] is an opaque type = Trace[A] => Boolean. eventually(filt) checks that some trace event satisfies the filter (not G x = F not x). bounded(timeBound)(prop) truncates the trace with takeWhile (_.time <= timeBound) — "the magics of streams". experiment(runs, prop, s0, timeBound) counts how many of runs fresh traces satisfy the bounded property and divides by runs: a PRISM-like statistical result in [0,1].
It sweeps the time bound t from 0.1 to 10.0 by 0.1; for each bound it runs experiment(runs = 26000, prop = eventually(_ == DONE), s0 = IDLE, timeBound = t) and yields (t, p); the XY line chart shows the probability of having completed rising quickly and saturating near 1 — matching the ≈ 1.5 s expected completion time of chapter 10. This mirrors PRISM's P=? [(true) U<=k (s=3)] experiment.