BLAHOUDEK, František, Alexandre DURET-LUTZ, Vojtěch RUJBR a Jan STREJČEK. On Refinement of Büchi Automata for Explicit Model Checking. In Fischer, Bernd and Geldenhuys, Jaco. 2015 International SPIN Symposium on Model Checking of Software. Heidelberg, New York, Dordrecht, London: Springer International Publishing, 2015, s. 66-83. ISBN 978-3-319-23403-8. Dostupné z: https://dx.doi.org/10.1007/978-3-319-23404-5_6.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název On Refinement of Büchi Automata for Explicit Model Checking
Název česky O zpřesňování 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), Vojtěch RUJBR (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí).
Vydání Heidelberg, New York, Dordrecht, London, 2015 International SPIN Symposium on Model Checking of Software, od s. 66-83, 18 s. 2015.
Nakladatel Springer International Publishing
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Švýcarsko
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/15:00080986
Organizační jednotka Fakulta informatiky
ISBN 978-3-319-23403-8
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-23404-5_6
UT WoS 000363788300006
Klíčová slova anglicky linear temporal logic; Büchi automata; explicit model checking; specification refinement
Štítky best, Büchi automata, firank_B, formela-conference, LTL, Model checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 20:47.
Anotace
In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.
Anotace česky
Při používání explicitní metody ověřování modelu jsou systémy typicky popsány implicitně a úsporně. Z tohoto implicitního popisu však lze snadno vyčíst užitečné informace, například že některé atomické propozice nemohou platit naráz. Tato publikace ukazuje několik způsobů, jak pomocí takovéto informace zlepšit Büchiho automat vytvořený na základě požadované specifikace zadané formulí ligiky LTL. Výsledkem jsou často menší automaty s kratšími návěštími hran, které jsou nejen jednoduší pro porozumění, ale především které zrychlují proces ověřování modelu.
Návaznosti
GBP202/12/G061, projekt VaVNázev: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
MUNI/A/1159/2014, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1206/2014, interní kód MUNá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
VytisknoutZobrazeno: 25. 4. 2024 07:19