Informace o publikaci
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 | |
| Rok publikování | 2015 |
| Druh | Článek ve sborníku |
| Konference | 2015 International SPIN Symposium on Model Checking of Software |
| Fakulta / Pracoviště MU | |
| 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: |