Neural Model Checking

Abhinandan Pal

Why Model Checking?

Humans make mistakes—and so do the AI tools the mordern work-force increasingly rely on. Some slip-ups are trivial (a banner in the wrong place), while others can halt a service, sink a company, or even endanger lives. Traditional testing helps, but history shows that many disasters slipped through “good enough” test suites.

Today, a single defect can ripple worldwide because we all run the same frameworks, libraries, and cloud services. For safety-critical domains—avionics, medical devices, rail signalling, power grids, robotics, and more—we need proof-level confidence, not just “we ran a lot of tests.”

Model checking delivers that confidence. By exhaustively exploring every possible behaviour of a design, it uncovers corner-case failures that testing almost always misses. The result: stronger guarantees, fewer surprises, and safer systems at global scale.

The Model Checking Problem#

Model checking boils down to one yes-or-no question: “Does my system M always behave according to property P?”

• M—the program, circuit, or protocol you wrote
• P—a logical checklist of everything it should do and must never do

Two Kinds of Promises#

Any linear-time property can be decomposed into a safety part plus a liveness part, and Linear Temporal Logic (LTL) is a convenient language for expressing both.

Mini Example — Example 1#

A system with two 1-bit outputs:

1. q — should go high once the job is done
   Liveness: eventually (q == 1)

2. p — an error flag that must never go high
   Safety: always (p == 0)

Model checking explores every possible run of the gadget; if any run violates either promise, it returns a concrete counter-example trace.

Linear Temporal Logic (LTL): Defining Behaviour Through Time

LTL extends propositional logic with time. Instead of a single snapshot, a satisfying assignment of an LTL formula is an infinite trace—one assignment of every variable for every time-step:

(q0 =0, p𝑛 =0) → (q1 = 0, p1 = 0) → (q2 = 1, p2 = 0) → ... → (q𝑛 =0, p𝑛 =0) → ...

This trace is an satisfying assignment to Example 1 if the error flag p is never 1 and, eventually, the “done” signal q becomes 1.

Note: a system satisfies an LTL property ig all its infinite traces satisfy the propoperty.

Four Building-Block Operators (+ two composites)#

Two handy composites:

• G F φ (recurrence) → φ occurs infinitely often.
• F G φ (persistence) → after some point, φ is permanently true.

All of these combine freely with Boolean logic (∧ ∨ ¬ →) and comparisons (= < > ≤ ≥).

A Small Example in Practice#

FG ¬rst   →   (GF (disp = 0) ∧ GF (disp = 1))

Plain English: Once the reset line (rst) stops firing forever, the controller must still bring up display 0 and display 1 infinitely often.

• FG ¬rst — reset is eventually off and stays off.
• GF (disp = 0) and GF (disp = 1) — each display reappears without end.
• The conjunction ensures neither display starves the other.

With LTL, we can specify such “always and eventually” behaviours, so a model checker can prove—or refute—that our system follows them.

Model Checking through Emptiness Checking#

1. Reactive System Model#

A reactive program runs forever. We describe it by

• Finite Number of Variables X_M
• Initial states Init_M
• Update relation Update_M(s, s′) that tells which next states s′ are legal after s.

2. Example 2#

for (int i = 0; ; i++) ;   // 16-bit signed, so it wraps

The program has exactly one infinite trace:

(i = 0) → (i = 1) → (i = 2) → … → (i = 32 767) → (i = -32 768) → … → (i = 0) → …`

3. System and Properties as Sets of Traces#

In a richer system, there may be many legal infinite traces—collect them in the set L_M. Consider the property

F (i = 5)          // “eventually i equals 5”

Every trace that ever visits a state with i = 5 belongs to the (huge) set L_P of traces satisfying the property. Model checking therefore asks a single question:

Is L_M ⊆ L_P? (Are all possible executions of the system also executions that eventually hit i = 5?)

If the answer is “yes,” the program meets the specification; if not, a counter-example trace lies in L_M ∖ L_P.

4. From “All Traces Satisfy P” to “No Trace Satisfies ¬P”#

Let L_¬P be the set of all infinite traces that violate the property P (i.e., traces that satisfy ¬P).

A program meets its spec exactly when no program trace is also a violating trace:

 L<sub>M</sub> ∩ L<sub>¬P</sub> = ∅

In words: there is no execution of M for which ¬P holds.

5. Büchi Automata: An Automata for Infinite Traces#

• A Büchi automaton (BA) recognises sets of infinite traces.
• A run is accepting if it visit “accepting” states infinitely often.

6. Product Automaton = Intersection of Traces#

Taking the synchronous product of the two automata yields

This new BA accepts exactly the traces in the intersection \(L_M \cap L_{\lnot P}\).

• If \(A_{M‖\lnot P}\) has no accepting run ⇒ the intersection is empty ⇒ every trace of M satisfies P.
• If it does have an accepting run, that run is a concrete counter-example.

Constructing the full product can blow up exponentially.
Modern techniques—symbolic model checking, SAT/SMT solving, and neural methods—reason about the emptiness of \(A_{M‖\lnot P}\) without enumerating all its states. This keeps the verification problem tractable even for large, real-world systems.

Emptiness checking using Invariants and Ranking Functions#

1. Which Transitions actually reachable?#

Instead of constructing the full product automaton A_(M‖¬P), we keep only:

• Init_(M‖¬P) – the set of initial states of the product.
• Update_(M‖¬P)(s, s′) – a relation that lists all legal next states s′ for any state s.

Important: Update_(M‖¬P) can provide next states for current states that cannot be reached from Init_(M‖¬P). Such state papers would disappear if we built the explicit product.

Which mean we must determine which states are reachable, using reachability invariant:

• I(s) = true  ⇔ s is reachable from Init_(M‖¬P)
• I(s) = false ⇔ s is unreachable “dead state” in the product

To enforce this,

1. Base case: I(s) is true for every initial state.
2. Step case: whenever I(s) and Update(s, s′) both hold, then ϕ(s′) must hold. In other words, if the current state is reachable so it the next.

Such a predicate is called an invariant because its truth value stays unchanged along every reachable path.

2. Accepting states can’t repeat forever#

Consider a non-negative integer function R(s) ∈ {0,1,2,…} for the reachable states, called the ranking function.

If a step in the trace goes through an accepting state, the rank strictly decreases. (Think of it as a counter that ticks down whenever an accepting state is observed in an infinite trace)

Because you cannot count down forever without hitting 0, such a function does not exists if there is a trace that visits accepting states infinitely many times.

Therefore if such a function exists the automaton has no accepting run. Conversly, if an accepting infinite trace exists, we cant compute such a function.

For the reachable states, the product automaton is empty iff no run can hit accepting states infinitely often.

3. The takeaway#

If you can supply:

• an Invariant marking all and only reachable states, and
• a Rank that drops whenever you pass an accepting state,

then you have proved the product automaton is empty, which means every trace of M satisfies P—all without ever listing the full state space.

We can additionally fold the invariant and ranking function into one function V:

• V(s) > k → state s is unreachable (invariant is false).
• V(s) ≤ k → state s is reachable; the value V(s) now plays the role of the ranking function.

Because we only need ranks for reachable states, this single function tells us both “is it reachable?” and “what is the rank?” in one shot.