6533b82afe1ef96bd128c1e0
RESEARCH PRODUCT
The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
Thomas NeeleAntti ValmariTim A.c. WillemseJean Goubault-larrecqBarbara Königsubject
FOS: Computer and information sciencesModel checkingComputer Science - Logic in Computer ScienceTheoretical computer sciencepartial-order reductionComputer scienceautomaattien teoria020207 software engineering02 engineering and technologymodel checkingArticleLogic in Computer Science (cs.LO)Partial order reductionstubborn sets0202 electrical engineering electronic engineering information engineeringState space020201 artificial intelligence & image processingEquivalence (formal languages)Equivalence (measure theory)tietojenkäsittelydescription
AbstractIn model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is sufficient to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a solution together with an updated correctness proof. Furthermore, we analyse in which formalisms this problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2020-04-17 |