Is there a best Büchi automaton for explicit model checking?
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Is there a best Büchi automaton for explicit model checking?
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
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
Others
Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
2014 International SPIN Symposium on Model Checking of Software
ISBN
9781450324526
ISSN
—
e-ISSN
—
Number of pages
76
Pages from-to
68
Publisher name
ACM
Place of publication
New York
Event location
San Jose, CA, USA
Event date
Jan 1, 2014
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—