2015
On Refinement of Büchi Automata for Explicit Model Checking
BLAHOUDEK, František, Alexandre DURET-LUTZ, Vojtěch RUJBR a Jan STREJČEKZá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
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
UT WoS
000363788300006
Klíčová slova anglicky
linear temporal logic; Büchi automata; explicit model checking; specification refinement
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 13. 5. 2020 20:47, RNDr. Pavel Šmerk, Ph.D.
V originále
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.
Č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 VaV |
| ||
MUNI/A/1159/2014, interní kód MU |
| ||
MUNI/A/1206/2014, interní kód MU |
|