Difference between revisions of "Publications/gillard.18.seminar"

From LRDE

(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 ...")
 
 
Line 4: Line 4:
 
| year = 2018
 
| year = 2018
 
| number = 1805
 
| number = 1805
| 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 <math>\omega</math>-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.
+
| 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 <math>\omega</math>-automata without building their productcircumventing 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 check, allowing us to use this new method in algorithms that require the counterexample.
 
| type = techreport
 
| type = techreport
 
| id = gillard.18.seminar
 
| id = gillard.18.seminar

Latest revision as of 16:16, 6 June 2018

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 productcircumventing 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 check, allowing us to use this new method in algorithms that require the counterexample.