In model checking, the system and its corresponding LTL specification are often translated into automata-based models. One of the most popular approach to LTL model checking is an automata-theoretic algorithm called tableau construction. This method take advantage of the fact that both system and its specification can be represented in the same notion, which in here is the Bu^¨chi automata model. In this article, we will breifly discuss the properties of Bu^¨chi automata, the most widely used automata model in model checking literature. This article assumes you have some basic knowlege on axiomatic set theory and automata theory.

1Basic definitions and properties

Let us first do a quick recap on your undergraduate theory of computation course. If you have some knowledge on automata theory, you may know that a regular finite automaton, which takes fintie words as input, can be formally defined by a 5-tuple.

Definition 1. (Finite automata) A finite automata is a 5-tuple such that

Now we can define the notion of a run on a automaton :

Definition 2. (Run) Let be a word (string, sequence) in the language (the Kleen closure of the alphabet ) of finite length . A run of over is a mapping such that the following properties holds:

A run is called accepting if it ends with a state in .

We define the language to be the set of all words accepted by the automaton and is said to be a Regular Langauge. A regular langauge can be described by a regular expression, such as . This article will not elaborate on the meaning of them, as regular expression is almost ubiquitous in day-to-day programming.

Bu^¨chi automata can be defined by the same 5-tuple that defines finite automata. In fact, the only difference between Bu^¨chi automata and finite automata is that Bu^¨chi automata can take words of infinite length as input. Since computers have finite amount of memory and many computer programs only run for finite amount of time, one may argue that finite length input and finite length runs are sufficient to describe the behavior of a system. However, infinite sets (and their cardinalities) can be think of the limit of finite sets when they are bounded but their boundaries are unkown. Furthermore, reactive systems such as traffic light control systems are not expected to terminate. In these scenarios, we must introduce Bu^¨chi automata.

Definition 3. (Bu^¨chi automata) A Bu^¨chi automaton is a finite automaton whose input word can be infinitely long. That is, , same as the cardinality of the set of all natural numbers.

Unlike finite automata who take words in , Bu^¨chi automata take words in , which is the language of finite and infinitely long strings whose characters are in , as input. For a Bu^¨chi automaton , the langauge consists of all the words accepted by and is called an -regular language. To properly define what it means for a Bu^¨chi automaton to accept a word, we must first prove a preliminary lemma.

Lemma 4. Let be a Bu^¨chi automaton, be an infinite run on . There exists a non-empty set of states in called such that it appears infinitly many times in the right-hand side of the mapping .

Proof. By the infinite pigeonhole principle, since is infinite and is finite, there must be at least one state in such that it appears infinitely many times in the right-hand side of .

With the notion of , we can now define the concept of acception formally:

Definition 5. (Acceptance) A run is said to be accepted by a Bu^¨chi automaton if and only if .

Note that this definition is very similar to how we define fairness in LTL, in fact the fairness condition in LTL is called generalized Bu^¨chi acceptance condition.

An important difference between regular finite automata and Bu^¨chi automata is that non-deterministic Bu^¨chi automata are strictly more expressive than deterministic ones.

Remark 6. (Difference between deterministic and non-deterministic Bu^¨chi automata) For deterministic Bu^¨chi automata, the transition relation is actually a partial function , that is, given a state and a character in alphabet, there is at most one next state. Non-deterministic Bu^¨chi automata do not have this limitation.

Lemma 7. Let be a deterministic Bu^¨chi automaton. Then there is an infinite set of prefixes of on which reaches an accepting state.

Proof. For deterministic Bu^¨chi automata, one input word can have exactly one run starting from its initial state. Thus this proposition can be proved directly from the definition of acception.

Theorem 8. Non-deterministic Bu^¨chi automata is strictly more expressive than its deterministic counterpart.

Proof. Consider the language whose and consists of finite number of 's but infinite number of 's . We will prove that no deterministic Bu^¨chi automaton can accept this language.

Suppose there exists such automaton such that equals . By the definition of , for any finite word , we have in . Now we can construct an infinite sequence of words such that , , where is the smallest natural number such that is in . Following this definition, we can construct a function that maps a natural number to a word . Let infinite word be any infinite word accepted by such that all words in are its prefixes. By lemma 7, this word is accepted by . However, for any finite number , there is always a prefix of having many of 's. Therefore contains infinitely many 's, contradicting the definition of .

However, there exists a non-deterministic Bu^¨chi automaton that accepts this language, see figure 1.

Figure 1. The non-deterministic Bu¨chi automaton for words with infinitely many 's but finitely many 's

Bring me back to sea level...