Is there a best Büchi automaton for explicit model checking?
| Název česky | Existuje nejlepší Büchiho automat pro explicitní metodu ověřování modelu? |
|---|---|
| Autoři | |
| Rok publikování | 2014 |
| Druh | Článek ve sborníku |
| Konference | 2014 International SPIN Symposium on Model Checking of Software |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1145/2632362.2632377 |
| Obor | Informatika |
| Klíčová slova | linear temporal logic; Büchi automata; explicit model checking |
| Přiložené soubory | |
| Popis | Překladače LTL na Büchiho automaty jsou obvykle optimalizovány tak, aby produkovaly automaty s co nejmenším počtem stavů, či s co nejmenším počtem nedeterministických stavů. V této publikaci hledáme vlastnosti Büchiho automatů, které skutečně ovlivňují výkon nástrojů pro explicitní metodu ověřování modelu (model checking). A to pomocí manuální analýzy několika automatů a experimenty s běžnými překladače LTL na automaty a realistickými verifikačními úlohami. Výsledkem těchto experimentů je lepší porozumění charakteristik automatů, které jsou dobré pro model checker Spin. |
| Související projekty: |