Two-automaton accepting run search in Spot
- Clément Gillard
In a previous paper we introduced the two-automaton emptiness check in the Spot library, that would check for the emptiness of the intersection of the languages of two -automata without building their product, circumventing a limitation in Spot on the number of acceptance sets of the automata. This operation, when the intersection is actually not empty, is usually followed by an accepting run search on the product that would return an example of such a word that is in the languages of both automata. We introduce a new method that computes an accepting run from the data gathered during the two-automaton emptiness checkallowing us to use this new method in algorithms that require the counterexample.