Documentation Finite State Automaton Analysis

Operations FSA

The following operations can be performed on FSA models.

• Convert to DFA – converts a non-deterministic automaton (NFA) to a deterministic automaton (DFA);
• Eliminate $\epsilon$ – eliminates all $\epsilon$ transitions from an NFA;
• Make Complete – make the automaton complete, by adding transitions and a state where needed to make sure that every states has an outgoing transition for every symbol of the alphabet; non-deterministic automata (NFA) are first converted to a DFA.
• Check for Emptiness – analyze if the language defined by the automaton, interpreted as an automaton on finite words is empty or not;
• Synchronous Product – compute the synchronous product between two automata on finite words. Automata are not allowed to take transitions without synchronization on symbols that are not present in the alphabet of the other automaton;
• Complement – compute the complement of the automaton on finite words;
• Check Word Acceptance – analyze if a given word is accepted by the automaton on finite words;
• Check Determinism – check if the automaton is deterministic;
• Determine Alphabet – determine the alphabet of the automaton;
• Check Language Inclusion – check if the language of one automaton on finite words is included in the language of another automaton;
• Minimize – minimize an automaton. Tries to find a smaller automaton that accepts the same language. Note that it does not necessarily give the smallest possible automaton that accepts the same language;
• Relabel States – replace the state labels of an automaton with labels of the form S followed by a number;
• Convert to Regular Expression – converts the automaton on finite words into a regular expression that defines the same language.

Operations NBA

The following operations can be performed on FSA models that represent Büchi automata.

• Check for Emptiness NBA – analyze if the language defined by the automaton, interpreted as an automaton on infinite words is empty or not;
• Synchronous Product NBA – compute the synchronous product between two automata on infinite words. Automata are not allowed to take transitions without synchronization on symbols that are not present in the alphabet of the other automaton;
• Minimize – minimize an automaton. Tries to find a smaller automaton that accepts the same language. Note that it does not necessarily give the smallest possible automaton that accepts the same language;