Is there a best Büchi automaton for explicit model checking?

BLAHOUDEK, František, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Is there a best Büchi automaton for explicit model checking?. Online. In Neha Rungta and Oksana Tkachuk. 2014 International SPIN Symposium on Model Checking of Software. New York: ACM, 2014. s. 68-76. ISBN 978-1-4503-2452-6. Dostupné z: https://dx.doi.org/10.1145/2632362.2632377. [citováno 2024-04-24]

Základní údaje

• Originální název: Is there a best Büchi automaton for explicit model checking?
• Název česky: Existuje nejlepší Büchiho automat pro explicitní metodu ověřování modelu?
• Autoři: BLAHOUDEK, František (203 Česká republika, domácí), Alexandre DURET-LUTZ (250 Francie), Mojmír KŘETÍNSKÝ (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)
• Vydání: New York, 2014 International SPIN Symposium on Model Checking of Software, od s. 68-76, 9 s. 2014.
• Nakladatel: ACM

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Spojené státy
• Utajení: není předmětem státního či obchodního tajemství
• Forma vydání: tištěná verze "print"
• Kód RIV: RIV/00216224:14330/14:00073815
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-1-4503-2452-6
• Doi: http://dx.doi.org/10.1145/2632362.2632377
• Klíčová slova anglicky: linear temporal logic; Büchi automata; explicit model checking
• Štítky: Büchi automata, firank_B, formela-conference, LTL, Model checking
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

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.

Anotace česky

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.

Návaznosti

• GBP202/12/G061, projekt VaV: Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

• MUNI/A/0765/2013, interní kód MU: Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

• MUNI/A/0855/2013, interní kód MU: Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty