Is there a best Büchi automaton for explicit model checking?
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00073815" target="_blank" >RIV/00216224:14330/14:00073815 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1145/2632362.2632377" target="_blank" >http://dx.doi.org/10.1145/2632362.2632377</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/2632362.2632377" target="_blank" >10.1145/2632362.2632377</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Is there a best Büchi automaton for explicit model checking?
Popis výsledku v původní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.
Název v anglickém jazyce
Is there a best Büchi automaton for explicit model checking?
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2014
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
2014 International SPIN Symposium on Model Checking of Software
ISBN
9781450324526
ISSN
—
e-ISSN
—
Počet stran výsledku
76
Strana od-do
68
Název nakladatele
ACM
Místo vydání
New York
Místo konání akce
San Jose, CA, USA
Datum konání akce
1. 1. 2014
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—