## ω-automata## BackgroundA where: is a set of states, is an alphabet, is a transition function, is a set of initial states, and is a set of final states.
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 A where: is a set of states, is an alphabet, is a transition function, is the initial state, and is a set of Rabin pairs.
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 AlgorithmSafra'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: a name where is the number of states in the original automaton, a label , and, 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: the union of the labels where is a child of some node must be a proper subset of if and are in separate branches then
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: if and are disjoint, then the initial tree is a single node with name 1 and label set if is a subset of , then the initial tree is a single node with name 1, label set , and the node is marked otherwise, let be the intersection of and , which is non-empty, then the initial tree is a root with name 1 and label set with a child node with name 2, label set , and the node is marked
The algorithm itself consists of the following steps: unmark: unmark all the leaves in the tree update: update the label set of each node according to the transition function and the current input symbol create: if the label set of , , intersects , then we add a right-most child to , call it , where is the intersection of and horizontal merge: remove all states in that appear in nodes where appears anywhere to the left of kill empty: remove all nodes with empty label sets, and their descendants vertical merge: mark all nodes where the union of the label sets of where is a child of is actually the label set of , then remove all descendants of
The Rabin automaton, , is obtained as follows: the state set is the collection of Safra trees generated by iterating the algorithm in all possible ways, starting at the initial tree this implicitly generates the transition function of the Rabin pairs of are , where is a name, is the set of trees in which does not appear, and is the set of trees in which appears and is marked
## ImplementationMy 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 . ## SourceThe 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. |