7. Logic and model checking
A Hennessy–Milner logic whose modalities are contexts (Hennessy and Milner,
Algebraic laws for nondeterminism and concurrency, 1985; Leifer and Milner,
Deriving bisimulation congruences for reactive systems, 2000), its
constructive apartness form (Geuvers and Jacobs, Relating apartness and
bisimulation, 2021), and checkers that turn certificates from untrusted
search into theorems about the library's reaction relation. Symbols are
those of the Notation chapter. Every other result is in Logic/: the IPO
test and decidability of the logic (T1.lean, T2.lean; the IPO criterion
is folklore, Leifer and Milner 2000, Jensen and Milner 2004), the μ-calculus
(Mu.lean), up-to techniques and rules with parameters (UpTo.lean,
Param.lean), witness certificates (Lasso.lean), weak bisimilarity blind to tags
(CertBisimTagBlind.lean), certified false verdicts (TrackDual.lean), and
the countermodels and remaining lemmas behind the congruence and preservation
results stated below (Congruence.lean, CongruenceChar.lean,
TagGaps.lean, OccPreserve.lean).