atrejo
home
automata

ω-automata

Background

A Büchi automaton is a non-deterministic automaton

M = langle Q, Sigma, tau, I, Frangle

where:

  • Q is a set of states,

  • Sigma is an alphabet,

  • tau: Q times Sigma rightarrow Q is a transition function,

  • I subseteq Q is a set of initial states, and

  • F subseteq Q is a set of final states.

M accepts an infinite word x in Sigma^omega if there is a run r of M on x that starts in I such that Inf(r), the set of recurrent states of r, intersects F. The collection of all such words x is the language accepted by M.

A language L subseteq Sigma^omega is recognizable if there is some Büchi automaton that accepts L.

A Rabin automaton is a deterministic automaton

M = langle Q, Sigma, tau, q_0, Prangle

where:

  • Q is a set of states,

  • Sigma is an alphabet,

  • tau: Q times Sigma rightarrow Q is a transition function,

  • q_0 is the initial state, and

  • P = {(L_1, R_1), dots, (L_n, R_n)} subseteq pow(Q) times pow(Q) is a set of Rabin pairs.

M accepts an infinite word x in Sigma^omega if there is a run r of M on x that starts at q_0 such that exists (L, R) in P where Inf(r) cap L = emptyset and Inf(r) cap R ne emptyset. L and R form the negative and positive conditions, respectively.

Safra's Determinization Algorithm

Safra's algorithm converts a non-deterministic Büchi automaton into a deterministic Rabin automaton. The reason for this conversion is that the class of deterministic Büchi automata accepts a smaller set of languages than the class of non-deterministic Büchi automata, but we'd still like the automaton to be deterministic.

The computation of the equivalent Rabin automaton requires the use of special ordered trees, called Safra trees.

A node in a Safra tree has three pieces of information:

  1. a name v in {1, 2, dots, 2n} where n is the number of states in the original automaton,

  2. a label l(v) subseteq Q, and,

  3. a mark, which is a single bit.

The root always has name 1 and only leaves of the tree can be marked.

The Safra conditions are:

  1. the union of the labels l(u) where u is a child of some node v must be a proper subset of l(v)

  2. if u and v are in separate branches then l(u) cap l(v) = emptyset

We'll use these Safra trees to represent the states of the deterministic automaton, so now we need to compute the transition function

d(T, a) = T'

where T,T' are Safra trees and a is a symbol in Sigma.

The initial tree is computed as follows:

  1. if I and F are disjoint, then the initial tree is a single node with name 1 and label set I

  2. if I is a subset of F, then the initial tree is a single node with name 1, label set I, and the node is marked

  3. otherwise, let L be the intersection of I and F, which is non-empty, then the initial tree is a root with name 1 and label set I with a child node with name 2, label set L, and the node is marked

The algorithm itself consists of the following steps:

  1. unmark: unmark all the leaves in the tree

  2. update: update the label set of each node according to the transition function and the current input symbol a

  3. create: if the label set of u, l(u), intersects F, then we add a right-most child to u, call it v, where l(v) is the intersection of l(u) and F

  4. horizontal merge: remove all states in l(u) that appear in nodes v where v appears anywhere to the left of u

  5. kill empty: remove all nodes with empty label sets, and their descendants

  6. vertical merge: mark all nodes u where the union of the label sets of v where v is a child of u is actually the label set of u, then remove all descendants of u

The Rabin automaton, A, is obtained as follows:

  1. the state set is the collection of Safra trees generated by iterating the algorithm in all possible ways, starting at the initial tree

  2. this implicitly generates the transition function of A

  3. the Rabin pairs of A are (L, R), where v is a name, L is the set of trees in which v does not appear, and R is the set of trees in which v appears and is marked

Implementation

My implementation begins by reading an input file with a description of a Büchi automaton. It translates the initial and final state sets into bitsets and converts the transition into a hash map. The initialization creates the initial tree according to the specification above, then it starts iterating the algorithm on the initial tree for each symbol in the alphabet.

Whenever a new tree is found, I store it in a hash table and store the transition in a hash map. The new tree is also pushed onto a queue of remaining trees. The computation ends when there are no new trees generated.

After the algorithm is finished, I convert the set of Safra trees and transitions into a directed graph, represented as an adjacency list. I also go through and generate the Rabin pairs.

I support testing of input of the form uv^omega where u is an initial transient segment and v is repeated infinitely often. Using the graph representation of the automaton, I simulate the automaton on u. Once u is exhausted, I simulate the automaton on v, however, since v is repeated infinitely often, I record the states visited along the way and stop when I find a cycle.

The automator accepts the input if there is a Rabin pair (L, R) such that the cycle C is disjoint from L and is not disjoint from R.

Source

The source code is available here. The current version is 5.0 (2012/08/05).

You'll have to modify src/Makefile so that it points to the Boost libraries and compiled binaries on your system. If you know how to use GNU Autotools with Boost and want to help me out, I'd really appreciate it.