Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-23404-5_6 | International SPIN Workshop on Model Checking of Software |
Field | DocType | Volume |
Kripke structure,Abstraction model checking,Model checking,Automaton,Atomic sentence,Theoretical computer science,Linear temporal logic,Mathematics,Büchi automaton | Conference | 9232 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.36 |
References | Authors | |
8 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frantisek Blahoudek | 1 | 48 | 4.02 |
| Alexandre Duret Lutz | 2 | 213 | 17.70 |
| Vojtech Rujbr | 3 | 1 | 0.36 |
| Jan Strejcek | 4 | 99 | 13.83 |