Counterexample searches in Spot

Authors

Clément Gillard

Type

techreport

Year

2019

Number

1903

Abstract

Spot is an $\omega$-automata manipulation library who aims to help doing $\omega$-automata-theoretic approach to model checking or develop tools for $\omega$-automata transformation. As such, it provides many algorithms, with many different implementations depending of the specificities of each $\omega$-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.