Name
Abstract | ||
|---|---|---|
This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness assumptions and then extend the algorithm to handle arbitrary ones. Notably, by making use of some syntactic transformations, our algorithm avoids constructing corresponding Büchi automata for the whole fairness assumptions, which can be very large in practice. We implement our algorithm in NuSMV and consider a large selection of formulas. Our experiments show that in many cases our approach exceeds the automata-theoretic approach up to several orders of magnitude, in both time and memory. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1109/TIME.2016.12 | 2016 23rd International Symposium on Temporal Representation and Reasoning (TIME) |
Keywords | DocType | Volume |
fairness assumptions,model checking problems,LTL properties,algorithm,syntactic transformations,Buchi automata | Conference | abs/1606.08116 |
ISBN | Citations | PageRank |
978-1-5090-3826-8 | 1 | 0.36 |
References | Authors | |
28 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yong Li | 1 | 3 | 3.77 |
| Lei Song | 2 | 31 | 5.45 |
| Yuan Feng | 3 | 218 | 38.29 |
| Lijun Zhang | 4 | 245 | 37.10 |