A twelve-week track on building precise models of systems and checking their properties: logic, transition systems, temporal logic, model checking, Petri nets, process composition, timed automata, probabilistic models and property-based testing. Every week opens on a small system introduced on its own terms, the kind a student will meet in practice: a controller that polls once a minute and tries to make the world match a desired state, a watchdog that repairs a component when a probe reads zero, a decode-and-write pipeline with a bounded buffer between two stages, a publish/subscribe broker with three delivery guarantees, a gateway that translates messages between two networks with different payload limits, a file store that must survive a crash in the middle of a write. No week depends on knowing any particular laboratory. The throughline: a model you can check beats a description you can only argue about, and a model you can break in front of you teaches more than one you can only read.
The 12-week arc
1 of 12 lectures published — each a self-contained read with a slide deck and runnable workbook. Start at the first published week and work forward.
| Wk | Theme & focus | Read |
|---|---|---|
| 01 | From informal spec to checkable property start here Verification vs validation; safety refuted by a finite trace, liveness only by a lasso; guards that make bad states unrepresentable; bounded liveness is safety. Widgets (nine): `ModelVsWorld` (guarded model against a world with an unguarded side door), `SchemaGate` (field, kind and slot selects; schema check on or off), `TraceExplorer` (room capacity 5-20 people, arrival probability 0-1, guard on or off; picture = occupancy trace with the first violating step marked; readout = first witness step), `EvidenceMeter` (sampled traces 10-1000 with a Wilson interval against the exact hit probability; break it with the rare-bug preset), `PrefixJudge` (five properties judged on a prefix of length 1-60), `LassoViewer` (reachability fixpoint on a looping schedule, break it by deleting the exit edge and watch EXIT drop out of the reachable set), `SurvivalLab` (exit probability 0-0.05 per step; break it with p = 0), `DeadlineDial` (timeout guard, deadline 50-400 steps; break it with D below the bound), `ClassifyIt` (eight requirements, safety, liveness or bounded). | read → slides · workbook |
| 02 | Logic, satisfiability and vacuous guards Propositional and predicate logic as the substrate; normal forms; satisfiability and DPLL; implication with a false premise, and why a guard that can only fire when its evidence is meaningless is true and useless. Widgets: `SatPlayground` (assign 2-8 jobs to 2-8 slots with conflict edges; picture = assignment grid plus the DPLL decision tree; readout = decisions taken vs the 2^n brute-force count; break it with n+1 jobs in n slots and watch an unsatisfiable pigeonhole blow up), `VacuityLens` (a repair rule "probe reads zero implies component dead"; toggle whether the probe runs only while the channel is quiet; readout = share of firings that carry information). | planned |
| 03 | Transition systems, reachability and the state explosion Kripke structures, interleaving of components, reachability as a least fixpoint, breadth-first search with counterexample paths; why n components of k states give up to k^n states; symmetry and abstraction, and the abstraction that is too coarse. Widgets: `StateSpaceBuilder` (components 1-6, local states 2-6, symmetry reduction on or off; picture = BFS frontier by depth; readout = reachable states vs k^n), `AbstractionToggle` (a controller status abstracted as two values or three; break it with two values and watch "running but degraded" raise a false alarm). | planned |
| 04 | Linear temporal logic Paths, lassos, the operators X, F, G, U and their duals; response and recurrence patterns; finite-prefix versus infinite-trace semantics. Scenario: a controller that retries once a minute and stops after a fixed number of failures, checked against G(desired → F converged). Widgets: `LtlTraceLab` (click states of a lasso trace to set p and q; select G p, F q, G(p → F q), p U q, G F p; picture = trace with the witness or refuting position lit; break it by truncating to a finite prefix and watch a verdict flip), `RetryCapLab` (retry cap 1-20 attempts, poll period 10-300 s, fault duration 1-180 min; readout = whether the response property holds, and why an "exhausted" state with no exit is an absorbing counterexample). | planned |
| 05 | CTL and fixpoint model checking Branching time, path quantifiers A and E, the labelling algorithm and its O(formula size × states) cost; EF, AG, AF, EG, E[p U q] as least and greatest fixpoints; formulas LTL can say and CTL cannot, and the reverse. Widgets: `CtlFixpoint` (an 8-state graph, formula select, step button; picture = states coloured per iteration until the fixpoint; readout = iterations and satisfying set; break it by adding one self-loop and watch AF fail at the initial state), `LtlVsCtl` (the F G p versus AF AG p example side by side). | planned |
| 06 | Petri nets and bounded buffers Places, transitions, markings, firing rule; boundedness, liveness, deadlock; reachability and coverability graphs; the incidence matrix and the state equation M = M0 + C·σ; place invariants. Scenario: a two-stage pipeline where decoded results wait for a single writer, bounded by a semaphore place held across both stages. Widgets: `PetriStepper` (workers 1-6, semaphore capacity 1-10, fire by click or seeded auto-run; picture = the net with tokens; formula = the state equation with the current marking substituted; readout = maximum tokens on the queue place; break it by deleting the semaphore place and watch the queue grow without bound, ω on the coverability graph), `ReachabilityGraph` (markings enumerated, dead markings highlighted). | planned |
| 07 | Coloured Petri nets and a message-translation gateway Typed tokens, arc expressions, guards; state-space exploration and its cost; symmetry by permuting identities. Scenario: a gateway that translates messages between two networks with different payload limits and must either deliver or explicitly reject every message. Widgets: `CpnGateway` (message identities 1-4, payload limit ratio, rejection path on or off, symmetry on or off; picture = the net plus the state-space size; readout = reachable markings and dead markings; break it by removing the rejection arc and find the marking where an oversized message waits forever). | planned |
| 08 | Composition, refinement and deadlock Labelled transition systems, synchronous product on shared actions, deadlock as a reachable state with no successor; trace equivalence versus bisimulation by partition refinement; refinement with invariant proof obligations as in Event-B. Widgets: `ProcessComposer` (2-6 processes around a ring of shared resources, acquisition order fixed or alternating; picture = the product graph with deadlocks in red; readout = reachable and deadlocked states; break it by making every process acquire left first), `BisimChecker` (two small machines that accept the same traces; step the partition refinement until it separates them). | planned |
| 09 | Timed automata and real-time properties Clocks, guards, invariants, resets; regions and zones for one and two clocks; bounded response ("within D seconds") and why a deadline turns liveness back into safety; UPPAAL-style queries. Scenario: a retry loop whose budget is counted in attempts, so its tolerance is really a time. Widgets: `ClockZoneLab` (poll period 10-300 s, attempt cap 1-20, repair time 1-180 min, deadline D; picture = the one-clock zone graph and a timeline; formula = tolerance = cap × period with values substituted; readout = whether "repaired implies converged within D" holds; break it by setting the timeout below the round-trip time), `RegionCounter` (clocks 1-3, largest constant 1-10; readout = number of regions, the reason zones exist). | planned |
| 10 | Probabilistic model checking Discrete-time Markov chains, reachability probability as a linear system, expected steps with rewards; PCTL-style queries; statistical model checking and its confidence interval. Scenario: message delivery over a lossy link under at-most-once, at-least-once and exactly-once handshakes. Widgets: `DtmcSolver` (loss probability 0-0.5, retries 0-5, handshake select; picture = the chain with transition probabilities; formula = x = (I − Q)^-1 b with values; readout = P(delivered) and expected transmissions), `SmcBudget` (simulated runs 10-10,000, seeded; picture = estimate with its interval against the exact value; break it with too few runs and watch the interval straddle the threshold). | planned |
| 11 | Property-based testing and runtime monitors Properties as executable specifications, generators, shrinking to a minimal counterexample; what a passing run proves and what it does not; monitors compiled from past-time temporal formulas over a live event log. Scenario: a file store that overwrites a document in place versus one that writes a temporary file and renames it, with a crash injected at a random point. Widgets: `ShrinkLab` (operation sequences of length 5-200, crash probability, seed, write strategy select; picture = the failing sequence before and after shrinking; readout = steps to first failure and shrunk length; break it by turning shrinking off), `MonitorLab` (stream a seeded event log through a monitor for "no commit without a prior open"; three-valued verdict per event). | planned |
| 12 | Capstone Model one small distributed control loop of the student's choice (a reconciler, a bounded pipeline, a broker, a gateway), state one safety and one liveness or probabilistic property, check both, and present the result through one widget of the student's own that follows the course contract. Widget: `AbstractionLedger` (a template table the student fills: what the model drops, why the property survives the drop, which counterexample would show it does not). | planned |
Capstone
Week 12: pick one small distributed control loop, build a formal model of it in the course's own Python kernel (the functions the workbooks build week by week), state one safety property and one liveness or probabilistic property worth guaranteeing, check both, and present the result through one widget of your own that meets the materials contract: named controls with units and ranges, a picture, the formula with values substituted, a readout, and a way to break the model. The written part is the abstraction ledger: what the model leaves out, why the checked property survives that, and which counterexample would show it does not.