Büchi Automata for Model Checking: Transforming System Models and LTL Properties

1. Introduction

In the previous posts of this series, we introduced the main building blocks of system modelling: Kripke structures, labelled transition systems (LTS), and program graphs. We also explored LTL and CTL as formalisms for expressing correctness properties.

In this post, we return to the structural side of model checking—how models and formulas are prepared so that they can be compared. This requires transforming systems into a unified form (usually a Kripke structure) and translating temporal logic formulas into structures such as Büchi automata, which accept infinite executions.

The purpose of these transformations is not to complicate the model but to place all models and formulas in a compatible mathematical framework. Each transformation keeps the system’s behaviour and the meaning of the specifications intact, but rephrases them so they can interact in a precise and mechanical way.

2. Büchi Automata and Omega-Languages

Classical finite automata analyse finite sequences of symbols. However, the executions of reactive systems—like controllers, concurrent programs, and communication protocols—are in general infinite. They continuously react to inputs and never “finish”.
To capture these behaviours, we use Büchi automata, which accept infinite words.

Formally, a Büchi automaton is a tuple:

• Q – a finite set of states,
• Q₀ – a set of initial states,
• Σ – an alphabet, often sets of propositions true at a state,
• Δ – a transition relation Q × Σ × Q,
• F – a set of accepting states.

A run of the automaton is an infinite sequence of transitions, each matching the next symbol of the word.
An infinite word is accepted if the run visits states from F infinitely often.

The acceptance condition may look unusual at first, but it matches typical recurring behaviours of systems—properties like “eventually something happens” or “something holds infinitely many times”. Büchi automata are specifically designed to express these repeating patterns over infinite executions.

A set of infinite words recognised by a Büchi automaton is called an omega-language. These languages allow us to represent precisely the executions that satisfy or violate temporal specifications.

3. Any system as a Kripke structure

Even though systems can be described in multiple modelling styles—transition systems, program graphs, or other formal models—we often need a unified representation when analysing them. Most temporal logics (including LTL) interpret their formulas over Kripke structures.

Therefore, no matter how the system is initially described, our first step is typically to transform it into an equivalent Kripke structure. This transformation ensures that the system’s behaviour is preserved while providing labels on states instead of transitions or variable assignments.

3.1. LTS to Kripke structure

A labelled transition system defines what actions occur during transitions between states. In contrast, a Kripke structure describes what propositions hold in each state. To bridge this difference, we translate the action-labelled transitions into state-labelled propositions.

The main idea is:

• Each state in the LTS becomes a state in the Kripke structure.
• The initial states remain unchanged.
• Each LTS transition s --a--> t becomes a Kripke transition s → t.
• The action a is encoded as a proposition that holds in the target state t.

In this way, the Kripke structure preserves the behaviour of the LTS while fitting the requirement that all descriptive information be available in the states. This conversion is simple yet powerful—it effectively turns dynamic action information into static state descriptions.

3.2. Program Graph to Kripke structure

Program graphs contain variables, guards, and assignments. A state in a program graph consists of:

• the current control location in the graph,
• the current valuation of all variables.

To create its Kripke structure:

1. We define each Kripke state as (location, valuation).
2. We choose initial states where the location is an initial program location and all variables satisfy their initial assignments.
3. For each program-graph transition with guard φ and actions α, we add a Kripke transition between any states whose valuation satisfies φ and whose updated valuation matches α.
4. The labelling function describes the truth of atomic propositions based on variable values and location.

This procedure essentially “unfolds” the program graph’s semantics into a structure where each node contains all required information. Although it may generate a large state space, it gives us a clear, propositional model suitable for temporal logic interpretation.

4. Transformations on Kripke structures

Systems often consist of several components running at different speeds or interacting in specific ways. To model such systems accurately, we need to combine individual Kripke structures into a single structure that reflects the overall behaviour.

Two common combination operations are the synchronous and asynchronous product.
A third important transformation is interpreting the Kripke structure as a Büchi automaton.

4.1. Synchronous product

The synchronous product models systems where all components move together at each step. It is appropriate when the system is governed by a global clock or when components communicate in strictly coordinated steps.

Given structures K₁ and K₂:

• The combined state space is the Cartesian product S₁ × S₂.
• Initial states are all pairs of initial states.
• A transition exists only if both components can move simultaneously.
• The label of a pair (s₁, s₂) is the union of L₁(s₁) and L₂(s₂).

This operation may increase the state space significantly, but it gives a precise representation of tightly coordinated systems.

4.2. Asynchronous product

The asynchronous product captures systems where components act independently. Only one component moves at a time while the other(s) remain idle. This is common in distributed systems, event-driven programs, or networks where processes do not share a global notion of time.

Formally:

• States are again pairs (s₁, s₂).
• A transition exists if one component moves and the other stays the same.
• Labels combine propositions from both components.

The asynchronous product allows individual behaviours to interleave in many possible ways, representing nondeterministic interleavings of parallel execution.

4.3. Kripke structure as a Büchi automaton

To express infinite executions, a Kripke structure can be directly interpreted as a Büchi automaton. This does not change the behaviour—it simply changes the perspective from “states and transitions” to “automaton over infinite words”.

The transformation is straightforward:

• States become automaton states.
• Initial states remain the same.
• Transitions remain unchanged.
• The alphabet of the automaton is the set of proposition sets appearing as labels.
• All states are accepting (F = S), because every infinite execution is considered a valid behaviour.

This representation lets us compare system executions with omega-languages defined by Büchi automata.

5. LTL to Büchi Automata

An LTL formula expresses conditions on infinite executions, such as safety (“something bad never happens”) or liveness (“something good eventually happens”). To analyse such formulas using automata, we convert them into Büchi automata whose accepted words are exactly the infinite sequences that satisfy the formula.

The translation follows these ideas:

• The automaton states represent collections of subformulas describing what must hold at each step.
• Transitions indicate how subformulas must evolve over time according to temporal operators such as X, U, or F.
• The acceptance condition ensures that certain required events (e.g., satisfaction of an until formula) occur infinitely often when needed.

The resulting automaton provides a structural representation of the formula’s semantics over infinite words. While the construction may produce a large structure, it forms the foundation for interpreting LTL in the automata-theoretic domain.

6. Summary

In this post, we explored how different modelling and specification representations can be transformed into more uniform structures suitable for analysis. We covered:

1. Büchi automata as a way to represent infinite executions and omega-languages.
2. Transformations of LTS and program graphs into Kripke structures, ensuring all models can be interpreted under temporal logics.
3. Synchronous and asynchronous products as methods to combine multiple Kripke structures into a single model.
4. How a Kripke structure can be understood as a Büchi automaton describing all its infinite behaviours.
5. A general view of how LTL formulas can be converted into Büchi automata, preparing formulas for further analysis.

These transformations form the mathematical foundation for later stages of verification, where system behaviour and logical formulas will be compared.

7. Sources and References

• Christel Baier & Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008.
• Edmund M. Clarke, Orna Grumberg, Doron Peled, Model Checking, MIT Press, 1999.
• G. Holzmann, The SPIN Model Checker, Addison-Wesley, 2004.
• Büchi Automaton (Wikipedia)