Adrian Trejo Nuñez [email protected]
To build, modify src/Makefile so that BOOSTDIR and BOOSTLIB are set to the paths of the Boost root directory and Boost compiled libraries, respectively.
Safra's Determinization Algorithm
A Büchi automaton is a non-deterministic automaton M = <Q, S, t, I, F> where Q is a set of states, S is an alphabet, t: Q * S -> Q is a transition function and I and F are the sets initial and final states respectively.
M accepts an infinite word x in S^ω if there is a run r of M on x that starts in I and 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, a subset of S^ω, is recognizable if there is some Büchi automaton that accepts L.
A Rabin automaton is a deterministic automaton M = <Q, S, t, q_0, P> where Q, S, and t are defined as before but q_0 is a single initial state and P is a subset of pow(Q) * pow(Q).
M accepts an infinite word x in S^ω if there is a run r of M on x that starts at q_0 and such that for some (L, R) in P, Inf(r) intersect L is empty and Inf(r) intersect R is not empty. The pairs (L, R) are called Rabin pairs: L is the negative condition and R is the positive condition.
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, ..., 2n} where n is the number of states in the original automaton,
(2) a label l(v) which is a subset of the state set 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) is disjoint from l(v)
We'll use these Safra trees to represent the states of the deterministic automaton, so now we need to compute the transition function d:
d(T, a) = T', where T,T' are Safra trees and a is a symbol in S
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
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^ω 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 automaton 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.