Embedded Systems Group (ES)

Automata Constructions

Using this tool, you can compute for a given automaton its associated Kripke structure as well as the Rabin/Scott and Breakpoint constructions for determinization. For deterministic acceptors on finite words, you can also compute its uniquely defined minimal acceptor, and for deterministic Mealy machines, you can compute a sequential circuit for it.

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

In the generated figures, initial states are drawn with double lines and accepting states are given in a green color. For acceptors, you can omit the declaration of output symbols and the outputs in the transitions.

Note that either you describe an automaton with outputs and no accepting states, i.e., a Mealy/Moore machine, or and acceptor that has accepting states and no outputs. See the examples at the end of the page.

implement the automaton as sequential circuit using various kinds of flipflops
compute the uniquely determined minimal automaton (for a deterministic acceptor on finite words)
compute associated Kripke structure
compute Rabin/Scott subset construction
compute breakpoint construction
compute transition monoid (for checking aperiodicity, i.e., expressibility in temporal logic)

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.

The following example acceptor accepts radix-4 numbers that are multiples of 3:

inputs i0,i1,i2,i3;
outputs ;
init 0,1;
accept 0;

The following Mealy machine implements a binary serial adder:

inputs i00,i01,i10,i11;
outputs s0,s1;
init 0;
accept ;

The following Mealy machine outputs o1 whenever sequence 1011 (without overlaps) has been read:

inputs i0,i1;
outputs o0,o1;
init 0;
accept ;

The following automata accepts all words with exactly one letter b (they are all equivalent to each other and produce therefore the same minimal automaton):

inputs a,b;
outputs ;
init 0;
accept 1,2;
inputs a,b;
outputs ;
init 0;
accept 2,3,4;
inputs a,b;
outputs ;
init 0;
accept 3,4,5,6,7,8;