Counterexample searches in Spot

From LRDE

Revision as of 15:29, 14 January 2019 by Bot (talk | contribs) (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...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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 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.