| Identifikační kód | RIV/00216224:14330/14:00073815 |
|---|
| Název v anglickém jazyce | Is there a best Büchi automaton for explicit model checking? |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2014 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 2 |
|---|
| Počet tvůrců celkem | 4 |
|---|
| Počet domácích tvůrců | 3 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | František Blahoudek (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 1425234)
Alexandre Duret-Lutz (státní příslušnost: FR - Francouzská republika)
Mojmír Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5598095)
Jan Strejček (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3978915) |
|---|
| Popis výsledku v anglickém jazyce | LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristicsof automata that work well with Spin. |
|---|
| Klíčová slova oddělená středníkem | linear temporal logic; Büchi automata; explicit model checking |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1145/2632362.2632377 |
|---|