On Refinement of Büchi Automata for Explicit Model Checking
From LRDE
- Authors
- František Blahoudek, Alexandre Duret-Lutz, Vojtčech Rujbr, Jan Strejček
- Where
- Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2015-06-15
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.
Documents
Bibtex (lrde.bib)
@InProceedings{ blahoudek.15.spin,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
Vojt\v{c}ech Rujbr and Jan Strej\v{c}ek},
title = {On Refinement of {B\"u}chi Automata for Explicit Model
Checking},
booktitle = {Proceedings of the 22th International SPIN Symposium on
Model Checking of Software (SPIN'15)},
year = 2015,
month = aug,
pages = {66--83},
publisher = {Springer},
volume = 9232,
series = {Lecture Notes in Computer Science},
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{\"u}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.},
doi = {10.1007/978-3-319-23404-5_6}
}