Formal verification is a technique used to guarantee that software behaves correctly. In formal verification, the behavior of a system is modeled mathematically, and the specifications it must satisfy are expressed as logical formulas.

Rather than simply listing states, the goals are to:

• Represent specifications as mathematical models
• Mechanically determine whether those specifications are always satisfied or violated
• Guarantee safety, including cases that are easy to miss with testing

Automata theory is used as a tool to achieve these goals.

In this field, many technical terms such as DFA, NFA, NBA, and LTL appear one after another and can be confusing. Abstract concepts like “state transitions,” “nondeterminism,” and “infinite executions” did not make much sense to me at first. However, my understanding improved by visualizing these ideas using a train route map as an analogy.

By using the familiar image of a route map, I believe it becomes easier to develop an intuitive understanding of how formal verification works.

Intended Audience

• People who have just started learning automata theory or formal verification at university
• People who feel “I kind of understand it, but it doesn’t really click” in classes on model checking or LTL
• Engineers who are interested in system verification

Two Axes for Classifying Automata

When trying to understand automata, there are actually only two viewpoints you need to keep in mind.

1. Whether the behavior is deterministic or nondeterministic
2. Whether the execution is finite or infinite

By combining these two axes, automata can theoretically be classified into four types. Abbreviations such as DFA, NFA, DBA, and NBA represent the differences in these combinations.

Deterministic × Finite DFA (Deterministic Finite Automaton) 1.

Nondeterministic × Finite NFA (Nondeterministic Finite Automaton) 1.

Deterministic × Infinite DBA (Deterministic Büchi Automaton) 1.

Nondeterministic × Infinite NBA (Nondeterministic Büchi Automaton)

What determinism and nondeterminism mean, and what infinite execution refers to, will be explained later with concrete examples. In addition, DBA, which handles deterministic infinite executions, will be omitted in this explanation from the perspective of expressiveness and practical usefulness.

With that said, let us start by looking at the simplest and most intuitive case: DFA (deterministic, finite execution).

Start with the Simplest DFA: A Single-Line Route

What Is a DFA (Deterministic Finite Automaton)?

A DFA (Deterministic Finite Automaton) is the simplest type of automaton. In terms of a route map, it corresponds to a single-line route.

For example, consider the following route.

This route has the following characteristics.

• Stations (states): Start, G0, Goal
• Tracks (transitions): connections from each station to the next
• Ticket (input): the action “take the Green Line”

The important point is that when you are at a given station, there is always exactly one next station you can move to. If you take the Green Line from the Start station, you will always arrive at station G1. There are no other choices.

Mathematical Definition

Formally, a DFA is defined as the following tuple.

A = (Q, q₀, Σ, δ, F)

• Q: a set of states (the set of stations)
• q₀: the initial state (the starting station)
• Σ: a set of input symbols (types of routes)
• δ: the transition function (which station you can go to from which station)
• F: a set of accepting states (destination stations)

This mathematical definition can be visualized as a state transition diagram. In practice and in introductory textbooks, this diagram itself is often referred to as “the automaton.” Strictly speaking, an automaton is a single definition that combines the set of states, transitions, initial state, and acceptance condition. If there are multiple such definitions, they are called automata (the plural form).

Extension to NFA: A Multi-Track Route

What Is an NFA (Nondeterministic Finite Automaton)?

An NFA is an extension of a DFA. The “D” in DFA stands for “Deterministic,” which changes to “Nondeterministic” in an NFA. In other words, there can be multiple possible next states. In terms of a route map, this corresponds to a multi-track route.

For example, consider a case where there are multiple ways to go from the Start station to the Goal station.

In this route network, starting from the same Start station, the path can branch into multiple routes under the same condition. From G1, you can go directly to Goal via the Green Line, or you can go via B1 on the Blue Line. From B1 as well, there are multiple choices: going through G1 or going directly to Goal.

This is what “nondeterminism” means. Which route is taken is not determined at that moment. However, the key idea of an NFA is that it is acceptable as long as there exists at least one route that reaches the goal.

Extension to NBA: Circular Lines and Infinite Time

What Is an NBA (Nondeterministic Büchi Automaton)?

An NBA is a further extension of an NFA. In terms of a route map, it corresponds to a network that includes circular lines.

For example, consider the following circular route, the Circle Line.

The key feature of this route is that you can keep going around it indefinitely. The train can continue running forever.

An NBA deals with exactly this kind of infinite behavior. Programs and systems often “run forever once they are started.” To reason about such infinite executions, NBA is required.

Clearing Up a Common Misunderstanding: Time Is Infinite, States Are Finite

There is a very important point here.

What is infinite is the execution time; the number of states is finite.

The fictional Circle Line has only 8 stations (a finite number), but you can loop around it indefinitely (infinite time). In the same way, an NBA represents infinite behavior using a finite number of states.

As mentioned at the beginning, let us restate the key points for understanding automata.

1. Whether the behavior is deterministic or nondeterministic
2. Whether the execution is finite or infinite

When I first started learning automata, I mixed up points 1 and 2. As a result, I mistakenly thought that if the number of executions is infinite, then the behavior—that is, the outcomes of actions—must also have infinitely many patterns.

In reality, even if there are multiple possible transitions, the number of states themselves remains finite once those transitions are properly grouped.

In other words, what we are doing here is not “turning infinity into finiteness.” More precisely,

we are making infinite-time behavior decidable using an automaton with a finite number of states.

Looking at a Concrete Example with a Traffic Light System

Let us now walk through everything discussed so far using a single concrete example.

System: Traffic Lights at an Intersection

A traffic light has three states.

• 🔴 Red
• 🟡 Yellow
• 🟢 Green

The state transitions are as follows.

[Green] --time passes--> [Yellow] --time passes--> [Red] --time passes--> [Green] --> ...

This forms a cycle and repeats infinitely.

Representation as a DFA

If we represent this traffic light as a DFA, the state at each moment is deterministically defined. If the current state is “Green,” the next state is always “Yellow.”

Representation as an NBA

Because the traffic light continues operating forever, it is natural to represent it as an NBA. The infinite loop “Green → Yellow → Red → Green → ...” can be expressed using just three states.

LTL Is a Language for Writing “Rules of Change”

What Is LTL (Linear Temporal Logic)?

So far, we have described how a system behaves. The next step is to check whether the system is behaving correctly.

For this purpose, LTL (Linear Temporal Logic) is used.

LTL is a logic for writing specifications about time. Using the route map analogy, it describes “operating rules”; for traffic lights, it describes “rules about how colors change,” written using symbols.

A Simple Explanation of LTL Operators

LTL uses the following operators to write specifications precisely. This avoids ambiguities that can arise in natural language.

• □ = G (Globally): always
• ◇ = F (Finally): eventually
• 〇 = X (neXt): at the next moment
• U (Until): until

Note that Globally and Finally are not primitive operators. They are derived from U and negation ¬.

• G p ≡ ¬F ¬p
• F p ≡ true U p

By combining these operators, complex temporal properties can be expressed. Let us now look at concrete examples using the traffic light system.

Specification 1: “After red, it must always become green”

For a traffic light, this means: “Once red is on, green must turn on afterward.”

In LTL: G(Red → X Green) (green at the next moment)

Specification 2: “Green and red must not be on at the same time”

For a traffic light, this means: “There must be no state where red and green are on simultaneously.”

In LTL: G ¬(Green ∧ Red) (always not (green and red))

Specification 3: “Green appears infinitely often”

For a traffic light, this means: “No matter how much time passes, green should keep appearing repeatedly.”

In LTL: GF Green (always, eventually green)

From LTL to NBA

Why Is the Conversion Necessary?

LTL is a language that is easy for humans to write specifications in. However, for a computer to check them, a more mechanically manageable form is required.

That form is the NBA.

LTL Can Be Converted into an NBA

In fact, it has been mathematically proven that any specification written in LTL can always be converted into a corresponding NBA. This follows from the property that LTL belongs to the class of ω-regular languages. ω-regular languages are an extension of regular languages that can handle infinite-length strings (infinite sequences of symbols), but we will omit the details here.

For example, the specification “green appears infinitely often,” written as GF Green, can be converted into the following NBA.

This NBA checks at S1, starting from Start, whether the current symbol is “Green” or “not Green.” If it is Green, the automaton transitions to S2, accepts the occurrence of Green, and then transitions back to S1 in the next step. If it is not Green, it loops back to S1. As a result, this NBA accepts exactly those runs that pass through Green infinitely often.

Checking the System Against the Specification

So how do we actually check whether a system satisfies a given specification?

Overall Flow

Represent the actual system as a state transition diagram

Represent the traffic light system as an NBA: “Green → Yellow → Red → Green → ...” 1.

Write the specification in LTL

Write “green appears infinitely often” as GF Green 1.

Convert the specification into an NBA

Mechanically generate an NBA corresponding to GF Green 1.

Take the product of the two NBAs

Combine the NBA of the actual system with the NBA of the specification 1.

Check whether there exists a path that satisfies the condition

Search for an accepting infinite path in the product automaton

In terms of the traffic light example:

• The actual behavior of the traffic light: Green → Yellow → Red → Green → ... (the system)
• A “checking pattern” that represents the operational rule (the specification NBA)

By overlaying these two, we check whether there exists a behavior that does not violate the rule.

If a violating path is found, that path represents a “bug.” Formal verification tools (model checkers) present such a path as a counterexample.

Practical Value: Why Formal Verification Matters

• Bug detection

• It enables exhaustive exploration of complex timing-dependent and rare-case bugs that are difficult to find with conventional testing.

• Safety guarantees

• In systems that affect human lives, such as aircraft or medical devices, it is necessary to mathematically prove the absence of bugs. Formal verification provides a powerful means to do so.

• Clarification of specifications

• The process of writing specifications in LTL helps clarify what the system is truly required to guarantee.

Summary

By using the route map analogy, the specialized terminology of automata theory becomes more intuitive. Although formal verification may appear difficult at first, its essence is simply to describe “how a system behaves” and “which rules it must satisfy” in mathematical terms, and then check them mechanically. Understanding that automata serve as the tools for this purpose makes the subject feel much more approachable.

References

• BASICS OF AUTOMATA THEORY FOR DUMMIES BY A DUMMY
• Automata-Based Representation of Linear-Time Properties and Linear Temporal Logic (LTL)