On Refinement of Büchi Automata for Explicit Model Checking

Varování

Publikace nespadá pod Ústav výpočetní techniky, 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:	Centrum excelence - Institut teoretické informatiky Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV. Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity