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

From LRDE

(Created page with "{{CSIReport | authors = Clément Gillard | title = Counterexample searches in Spot | year = 2019 | number = 1903 | abstract = Spot is an <math>\omega</math>-automata manipulat...")
 
 
Line 4: Line 4:
 
| year = 2019
 
| year = 2019
 
| number = 1903
 
| number = 1903
| abstract = Spot is an <math>\omega</math>-automata manipulation library who aims to help doing <math>\omega</math>-automata-theoretic approach to model checking or develop tools for <math>\omega</math>-automata transformation. As such, it provides many algorithms, with many different implementations depending of the specificities of each <math>\omega</math>-automaton. Of those algorithms, emptiness check algorithms and counterexample search algorithms are often used, with various goals, and since their results are linkedthey are often used together. However, some implementations of emptiness check algorithms lack a similar counterexample search implementation which is able to work in the same way on the same automata. We introduce two implementations of counterexample computation, which complete two already existing implementations of emptiness check algorithms by walking in their footsteps and reusing some of the data they gathered to efficiently compute counterexamples.
+
| abstract = Spot is an <math>\omega</math>-automata manipulation library who aims to help doing <math>\omega</math>-automata-theoretic approach to model checking or develop tools for <math>\omega</math>-automata transformation. As such, it provides many algorithms, with many different implementations depending of the specificities of each <math>\omega</math>-automaton. Of those algorithms, emptiness check algorithms and counterexample search algorithms are often used, with various goals, and since their results are linked, they are often used together. However, some implementations of emptiness check algorithms lack a similar counterexample search implementation which is able to work in the same way on the same automata. We introduce two implementations of counterexample computation, which complete two already existing implementations of emptiness check algorithms by walking in their footsteps and reusing some of the data they gathered to efficiently compute counterexamples.
 
| type = techreport
 
| type = techreport
 
| id = gillard.19.seminar
 
| id = gillard.19.seminar

Latest revision as of 17:07, 29 January 2019

Abstract

Spot is an -automata manipulation library who aims to help doing -automata-theoretic approach to model checking or develop tools for -automata transformation. As such, it provides many algorithms, with many different implementations depending of the specificities of each -automaton. Of those algorithms, emptiness check algorithms and counterexample search algorithms are often used, with various goals, and since their results are linked, they are often used together. However, some implementations of emptiness check algorithms lack a similar counterexample search implementation which is able to work in the same way on the same automata. We introduce two implementations of counterexample computation, which complete two already existing implementations of emptiness check algorithms by walking in their footsteps and reusing some of the data they gathered to efficiently compute counterexamples.