Notebooks
Browser-based interactive notebooks for the Verification and Validation Techniques course at UniUD — automata, infinite words, Büchi complementation, temporal logic, and model checking, grouped by chapter.
Each notebook keeps one construction or algorithm in the foreground and lets you drive it on concrete inputs. They follow the chapters of the lecture notes; work through a chapter's notebooks alongside its Proof Labs and Mind Map.
Chapter 1 · Finite-State Automata
NB 1
Intro to Finite-State Automata
Alphabets, words, languages, and DFAs — a hands-on first contact
NB 2
NFA Reachable States
Step through the blackboard NFA and trace its active state sets
NB 3
Subset Construction
Convert any NFA to an equivalent DFA, subset by subset
Chapter 2 · Regular Languages & Decision Problems
NB 4
ε-Closure & ε-Removal
Compute ε-closures and compile ε-transitions away
NB 5
Product Automaton
Build the intersection of two DFAs by the product construction
NB 6
Reachability Fixpoint
Reachable states via a fixpoint, and the decision problems it settles
NB 7
Kleene State Elimination
Turn a DFA into a regular expression by eliminating states
NB 8
Regex to Automaton (Kleene)
Generate NFAs from a regex and trace the Rᵏᵢⱼ paths
Chapter 3 · Automata over Infinite Words
NB 11
Infinite Words & In(α)
ω-words, segments, and the infinity set of positions
NB 12
Büchi Automaton Runner
Trace u·vω and test acceptance via In(ρ) ∩ F ≠ ∅
NB 13
Vectorial Closure
Which ω-words have infinitely many prefixes in a language W
NB 14
Büchi Emptiness (Lasso)
Decide emptiness by hunting for a reachable accepting cycle
NB 15
Parity Between a's
A deterministic Büchi automaton whose states encode a parity invariant
NB 16
The DBA vs NBA Gap
Why "finitely many saves" needs nondeterminism — no DBA can do it
NB 17
ω-Regular Expressions
The ⋃ Uᵢ·Vᵢω normal form and its Büchi automata
NB 18
Büchi Union & Intersection
Trivial union vs the two-phase product for intersection
NB 19
Ultimately-Periodic Witnesses
Read a u·vω witness off a lasso; the fingerprint of non-emptiness
Chapter 4 · Complementation of ω-Regular Languages
NB 20
Congruence & Saturation
Finite-index congruences (parity) and what saturation means
NB 21
The Congruence ≈𝒜
The state×state profile a word attaches to a Büchi automaton
NB 22
Merging Positions
When two positions merge, and why merging can never be broken
NB 23
Ramsey Decomposition
A non-periodic ω-word as prefix + one idempotent block class
NB 24
Saturation → Complement
Assemble the complement automaton from disjoint class products
Temporal Logic & Model Checking · Part II preview
Chapter 7 · Reactive Systems, SMV & Model Checking
NB 10
The Arbiter Kripke Structure
Click through the buggy/fixed arbiter and watch AG(request → AX busy) hold or break
NB 25
SMV Step Simulator
Flip-flop, modulo-4 counter, and the five-digit mechanical counter, one next() at a time
NB 26
Producer–Consumer Fairness Sandbox
Schedule producer/consumer steps yourself and watch an unfair run take shape