Name
Abstract | ||
|---|---|---|
LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2632362.2632377 | SPIN |
Keywords | Field | DocType |
explicit model checking,algorithms,mathematical logic,verification,software/program verification,linear temporal logic,theory,büchi automata,buchi automata | Quantum finite automata,Automata theory,Model checking,Automaton,Linear temporal logic,Theoretical computer science,Timed automaton,Mathematics,Büchi automaton,ω-automaton | Conference |
Citations | PageRank | References |
3 | 0.43 | 19 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frantisek Blahoudek | 1 | 48 | 4.02 |
| Alexandre Duret Lutz | 2 | 213 | 17.70 |
| Mojmír Kretínský | 3 | 88 | 7.11 |
| Jan Strejcek | 4 | 99 | 13.83 |