Identifikační kód | RIV/00216224:14330/15:00080986 |
Název v anglickém jazyce | On Refinement of Büchi Automata for Explicit Model Checking |
Druh | D - Článek ve sborníku |
Jazyk | eng - angličtina |
Obor - skupina | I - Informatika |
Obor | IN - Informatika |
Rok uplatnění | 2015 |
Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
Počet výskytů výsledku | 2 |
Počet tvůrců celkem | 4 |
Počet domácích tvůrců | 3 |
Výčet všech uvedených jednotlivých tvůrců | František Blahoudek (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 1425234) Alexandre Duret-Lutz (státní příslušnost: FR - Francouzská republika) Vojtěch Rujbr (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6148999) Jan Strejček (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3978915) |
Popis výsledku v anglickém jazyce | 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. |
Klíčová slova oddělená středníkem | linear temporal logic; Büchi automata; explicit model checking; specification refinement |
Stránka www, na které se nachází výsledek | - |
DOI výsledku | 10.1007/978-3-319-23404-5_6 |