A Büchi automaton is a non-deterministic automaton
accepts an infinite word if there is a run of on that starts in such that , the set of recurrent states of , intersects . The collection of all such words is the language accepted by .
A language is recognizable if there is some Büchi automaton that accepts .
A Rabin automaton is a deterministic automaton
accepts an infinite word if there is a run of on that starts at such that where and . and 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:
The root always has name 1 and only leaves of the tree can be marked.
The Safra conditions are:
We'll use these Safra trees to represent the states of the deterministic automaton, so now we need to compute the transition function
where are Safra trees and is a symbol in .
The initial tree is computed as follows:
The algorithm itself consists of the following steps:
The Rabin automaton, , is obtained as follows:
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 where is an initial transient segment and is repeated infinitely often. Using the graph representation of the automaton, I simulate the automaton on . Once is exhausted, I simulate the automaton on , however, since 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 such that the cycle is disjoint from and is not disjoint from .
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.