# 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 |
+ | | 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 18:07, 29 January 2019

- Authors
- Clément Gillard
- Type
- techreport
- Year
- 2019
- Number
- 1903

## Abstract

Spot is an **Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \omega}**
-automata manipulation library who aims to help doing **Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \omega}**
-automata-theoretic approach to model checking or develop tools for **Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \omega}**
-automata transformation. As such, it provides many algorithms, with many different implementations depending of the specificities of each