Fachbereich Informatik

Embedded Systems Group (ES)

Algorithms for ω-Automata

Using this tool, you can apply several algorithms to a given ω-automaton. The ω-automaton can either be given in a symbolic representation as shown with the example below or in an explicit representation (see examples below). Allowed acceptance conditions are G,F,FG and GF.

The tool can convert symbolic to explicit representations and vice versa, can trim the given automaton, i.e., restrict it to states which are reachable and have infinite outgoing paths (reactive states). Clearly, the tool also draws the state transition diagram for both explicit and symbolic representations. In the generated figures, initial states are drawn with double lines and accepting states are given in a green color.

The next set of operations is the change of acceptance conditions from G to any other one and from F and FG to F,FG,GF (it is in general not possible to reduce GF to others). The tool can also determinize these automata (except for GF acceptance), and it also simply applies the subset and breakpoint construction (make sure that this makes sense for you since the generated automaton may not be equivalen to the given one).

The tool can also check the emptiness of the automaton and can compute a word with an accepting run in case the language of the automaton is not empty.

In addition to the associated Kripke structure of the automaton, the tool can also compute the transition monoid of the automaton and checks whether it is aperiodic. If so, the automaton can be described in temporal logic, otherwise, this is impossible.

automaton:
select computations:
convert symbolic to explicit automaton or vice versa
restrict the automaton to reachable reactive states
show state transition diagram
change acceptance condition
determinize (except for GF)
apply subset construction
apply breakpoint construction
check emptiness
compute associated Kripke structure
compute transition monoid (for checking aperiodicity, i.e., expressibility in temporal logic)
compute the uniquely determined minimal automaton (for a deterministic acceptor on finite words)
implement the automaton as sequential circuit using various kinds of flipflops

Please note that the automaton is given in an explicit form, i.e., the automaton given above has two inputs a1 and 2 and two possible outputs b1 and b2 (it is not a boolean encoding). So, in any state the automaton may read either the input a1 or a2 and can then react by transitions with corresponding outputs and a target state. If a transition is taken, there must be one of the two outputs b1 or b2.

An explicit representation of the example automaton above is as follows: 

inputs a,b,c,d;
init 0;
trans
    (0,a,0); (0,a,2); (0,c,0);
    (1,a,0); (1,a,1); (1,a,2); (1,a,3);
    (1,b,0); (1,b,1); (1,b,2); (1,b,3);
    (1,c,0); (1,c,1); 
    (2,a,0); (2,a,2);
    (2,c,0); (2,c,2);
    (3,a,0); (3,a,1); (3,a,2); (3,a,3);
    (3,b,0); (3,b,1); (3,b,2); (3,b,3);
    (3,c,0); (3,c,1); (3,c,2); (3,c,3);
    (3,d,0); (3,d,1); (3,d,2); (3,d,3);
accept 2,3;
acpTy FG;