2014
Is there a best Büchi automaton for explicit model checking?
BLAHOUDEK, František; Alexandre DURET-LUTZ; Mojmír KŘETÍNSKÝ and Jan STREJČEKBasic information
Original name
Is there a best Büchi automaton for explicit model checking?
Name in Czech
Existuje nejlepší Büchiho automat pro explicitní metodu ověřování modelu?
Authors
BLAHOUDEK, František (203 Czech Republic, belonging to the institution); Alexandre DURET-LUTZ (250 France); Mojmír KŘETÍNSKÝ (203 Czech Republic, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)
Edition
New York, 2014 International SPIN Symposium on Model Checking of Software, p. 68-76, 9 pp. 2014
Publisher
ACM
Other information
Language
English
Type of outcome
Proceedings paper
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
United States of America
Confidentiality degree
is not subject to a state or trade secret
Publication form
printed version "print"
RIV identification code
RIV/00216224:14330/14:00073815
Organization unit
Faculty of Informatics
ISBN
978-1-4503-2452-6
EID Scopus
2-s2.0-84942354163
Keywords in English
linear temporal logic; Büchi automata; explicit model checking
Tags
International impact, Reviewed
Changed: 11/7/2019 13:31, RNDr. Pavel Šmerk, Ph.D.
V originále
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 characteristics of automata that work well with Spin.
In Czech
Překladače LTL na Büchiho automaty jsou obvykle optimalizovány tak, aby produkovaly automaty s co nejmenším počtem stavů, či s co nejmenším počtem nedeterministických stavů. V této publikaci hledáme vlastnosti Büchiho automatů, které skutečně ovlivňují výkon nástrojů pro explicitní metodu ověřování modelu (model checking). A to pomocí manuální analýzy několika automatů a experimenty s běžnými překladače LTL na automaty a realistickými verifikačními úlohami. Výsledkem těchto experimentů je lepší porozumění charakteristik automatů, které jsou dobré pro model checker Spin.
Links
| GBP202/12/G061, research and development project |
| ||
| MUNI/A/0765/2013, interní kód MU |
| ||
| MUNI/A/0855/2013, interní kód MU |
|
