On Refinement of Büchi Automata for Explicit Model Checking
| Authors | |
|---|---|
| Year of publication | 2015 |
| Type | Article in Proceedings |
| Conference | 2015 International SPIN Symposium on Model Checking of Software |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-319-23404-5_6 |
| Field | Informatics |
| Keywords | linear temporal logic; Büchi automata; explicit model checking; specification refinement |
| Description | 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. |
| Related projects: |