A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
Neele, T., Valmari, A., & Willemse, T. A. C. (2021). A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. Logical Methods in Computer Science, 17(3), Article 8. https://doi.org/10.46298/lmcs-17(3:8)2021
Published in
Logical Methods in Computer ScienceDate
2021Copyright
© T. Neele, A. Valmari, and T.A.C. Willemse
One of the most popular state-space reduction techniques for model checking is partial-order reduction (POR). Of the many different POR implementations, stubborn sets are a very versatile variant and have thus seen many different applications over the past 32 years. One of the early stubborn sets works shows how the basic conditions for reduction can be augmented 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 stronger reduction condition and provide extensive new correctness proofs to ensure the issue is resolved. Furthermore, we analyse in which formalisms the problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory.
Publisher
Logical Methods in Computer Science e.V.ISSN Search the Publication Forum
1860-5974Keywords
Publication in research information system
https://converis.jyu.fi/converis/portal/detail/Publication/100398266
Metadata
Show full item recordCollections
License
Related items
Showing items with similar title or keywords.
-
The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
Neele, Thomas; Valmari, Antti; Willemse, Tim A. C (Springer, 2020)In 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 ... -
Partial-order reduction for parity games and parameterised Boolean equation systems
Neele, Thomas; Willemse, Tim A. C.; Wesselink, Wieger; Valmari, Antti (Springer, 2022)In model checking, reduction techniques can be helpful tools to fight the state-space explosion problem. Partial-order reduction (POR) is a well-known example, and many POR variants have been developed over the years. ... -
Stubborn Sets, Frozen Actions, and Fair Testing
Valmari, Antti; Vogler, Walter (IOS Press, 2021)Many partial order methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based ... -
Analysis of errors caused by incomplete knowledge of material data in mathematical models of elastic media
Mali, Olli (University of Jyväskylä, 2011) -
All congruences below stability-preserving fair testing or CFFD
Valmari, Antti (Springer, 2020)In process algebras, a congruence is an equivalence that remains valid when any subsystem is replaced by an equivalent one. Whether or not an equivalence is a congruence depends on the set of operators used in building ...