On Refinement of Büchi Automata for Explicit Model Checking

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky O zpřesňování Büchiho automatů pro explicitní metodu ověřování modelu.
Autoři

BLAHOUDEK František DURET-LUTZ Alexandre RUJBR Vojtěch STREJČEK Jan

Rok publikování 2015
Druh Článek ve sborníku
Konference 2015 International SPIN Symposium on Model Checking of Software
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-319-23404-5_6
Obor Informatika
Klíčová slova linear temporal logic; Büchi automata; explicit model checking; specification refinement
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.