Two-automaton accepting run search in Spot

From LRDE

Revision as of 10:15, 1 June 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Clément Gillard | title = Two-automaton accepting run search in Spot | year = 2018 | number = 1805 | abstract = In a previous paper we introduced the ...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

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.