Namespace mata::nfa::algorithms

namespace algorithms

Concrete NFA implementations of algorithms, such as complement, inclusion, or universality checking.

Functions

Nfa minimize_brzozowski(const Nfa &aut)

Brzozowski minimization of automata (revert -> determinize -> revert -> determinize).

Parameters:

aut – [in] Automaton to be minimized.

Returns:

Minimized automaton.

Nfa minimize_hopcroft(const Nfa &dfa_trimmed)

Hopcroft minimization of automata.

Based on the algorithm from the paper: “Efficient Minimization of DFAs With Partial Transition Functions” by Antti Valmari and Petri Lehtinen. The algorithm works in O(a*n*log(n)) time and O(m+n+a) space, where: n is the number of states, a is the size of the alphabet, and m is the number of transitions. [https://dl.acm.org/doi/10.1016/j.ipl.2011.12.004]

Parameters:

dfa_trimmed – [in] Deterministic automaton without useless states. Perform trimming before calling this function.

Returns:

Minimized deterministic automaton.

Nfa complement_classical(const Nfa &aut, const mata::utils::OrdVector<Symbol> &symbols)

Complement implemented by determization, adding sink state and making automaton complete.

Then it adds final states which were non final in the original automaton.

Parameters:

  • aut – [in] Automaton to be complemented.

  • symbols – [in] Symbols needed to make the automaton complete.

  • minimize_during_determinization – [in] Whether the determinized automaton is computed by (brzozowski) minimization.

Returns:

Complemented automaton.

Nfa complement_brzozowski(const Nfa &aut, const mata::utils::OrdVector<Symbol> &symbols)

Complement implemented by determization using Brzozowski minimization, adding a sink state and making the automaton complete.

Then it swaps final and non-final states.

Parameters:

  • aut – [in] Automaton to be complemented.

  • symbols – [in] Symbols needed to make the automaton complete.

Returns:

Complemented automaton.

bool is_included_naive(const Nfa &smaller, const Nfa &bigger, const Alphabet *alphabet = nullptr, Run *cex = nullptr)

Inclusion implemented by complementation of bigger automaton, intersecting it with smaller and then it checks emptiness of intersection.

Parameters:

  • smaller – [in] Automaton which language should be included in the bigger one.

  • bigger – [in] Automaton which language should include the smaller one.

  • alphabet – [in] Alphabet of both automata (it is computed automatically, but it is more efficient to set it if you have it).

  • cex – [out] A potential counterexample word which breaks inclusion

Returns:

True if smaller language is included, i.e., if the final intersection of smaller complement of bigger is empty.

bool is_included_antichains(const Nfa &smaller, const Nfa &bigger, const Alphabet *alphabet = nullptr, Run *cex = nullptr)

Inclusion implemented by antichain algorithms.

Parameters:

  • smaller – [in] Automaton which language should be included in the bigger one

  • bigger – [in] Automaton which language should include the smaller one

  • alphabet – [in] Alphabet of both automata (not needed for antichain algorithm)

  • cex – [out] A potential counterexample word which breaks inclusion

Returns:

True if smaller language is included, i.e., if the final intersection of smaller complement of bigger is empty.

bool is_universal_naive(const Nfa &aut, const Alphabet &alphabet, Run *cex)

Universality check implemented by checking emptiness of complemented automaton.

Parameters:

  • aut – [in] Automaton which universality is checked

  • alphabet – [in] Alphabet of the automaton

  • cex – [out] Counterexample word which eventually breaks the universality

Returns:

True if the complemented automaton has non empty language, i.e., the original one is not universal

bool is_universal_antichains(const Nfa &aut, const Alphabet &alphabet, Run *cex)

Universality checking based on subset construction with antichain.

Parameters:

  • aut – [in] Automaton which universality is checked

  • alphabet – [in] Alphabet of the automaton

  • cex – [out] Counterexample word which eventually breaks the universality

Returns:

True if the automaton is universal, otherwise false.

Simlib::Util::BinaryRelation compute_relation(const Nfa &aut, const ParameterMap &params = {{"relation", "simulation"}, {"direction", "forward"}})
Nfa product(const Nfa &lhs, const Nfa &rhs, const std::function<bool(State, State)> &&final_condition, const Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr)

Compute product of two NFAs, final condition is to be specified, with a possibility of using multiple epsilons.

Parameters:

  • lhs – [in] First NFA to compute intersection for.

  • rhs – [in] Second NFA to compute intersection for.

  • first_epsilons – [in] The smallest epsilon.

  • final_condition – [in] The predicate that tells whether a pair of states is final (conjunction for intersection).

  • prod_map – [out] Can be used to get the mapping of the pairs of the original states to product states. Mostly useless, it is only filled in and returned if !=nullptr, but the algorithm internally uses another data structures, because this one is too slow.

Returns:

NFA as a product of NFAs lhs and rhs with ε-transitions preserved.

Nfa concatenate_eps(const Nfa &lhs, const Nfa &rhs, const Symbol &epsilon, bool use_epsilon = false, StateRenaming *lhs_state_renaming = nullptr, StateRenaming *rhs_state_renaming = nullptr)

Concatenate two NFAs.

Supports epsilon symbols when use_epsilon is set to true.

Parameters:

  • lhs – [in] First automaton to concatenate.

  • rhs – [in] Second automaton to concatenate.

  • epsilon – [in] Epsilon to be used for concatenation (provided use_epsilon is true)

  • use_epsilon – [in] Whether to concatenate over epsilon symbol.

  • lhs_state_renaming – [out] Map mapping lhs states to result states.

  • rhs_state_renaming – [out] Map mapping rhs states to result states.

Returns:

Concatenated automaton.

Nfa reduce_simulation(const Nfa &nfa, StateRenaming &state_renaming)

Reduce NFA using (forward) simulation.

Parameters:

  • nfa – [in] NFA to reduce

  • state_renaming – [out] Map mapping original states to the reduced states.

Nfa reduce_residual(const Nfa &nfa, StateRenaming &state_renaming, const std::string &type, const std::string &direction)

Reduce NFA using residual construction.

Parameters:

  • nfa – [in] NFA to reduce.

  • state_renaming – [out] Map mapping original states to the reduced states.

  • type – [in] Type of the residual construction (values: “after”, “with”).

  • direction – [in] Direction of the residual construction (values: “forward”, “backward”).

Nfa reduce_residual_with(const Nfa &nfa)

Reduce NFA using residual construction.

The residual construction of the residual automaton and the removal of the covering states is done during the last determinization.

Similar performance to reduce_residual_after(). The output is almost the same except the transitions: transitions may slightly differ, but the number of states is the same for both algorithm types.

Nfa reduce_residual_after(const Nfa &nfa)

Reduce NFA using residual construction.

The residual construction of the residual automaton and the removal of the covering states is done after the final determinization.

Similar performance to reduce_residual_with(). The output is almost the same except the transitions: transitions may slightly differ, but the number of states is the same for both algorithm types.