The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
Neele, T., Valmari, A., & Willemse, T. A. C. (2020). The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. In J. Goubault-Larrecq, & B. König (Eds.), FoSSaCS 2020 : Foundations of Software Science and Computation Structures : 23rd International Conference, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings (pp. 482-501). Springer. Lecture Notes in Computer Science, 12077. https://doi.org/10.1007/978-3-030-45231-5_25
Published inLecture Notes in Computer Science
© The Authors 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 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.
Parent publication ISBN978-3-030-45230-8
ConferenceInternational Conference on Foundations of Software Science and Computation Structures
Is part of publicationFoSSaCS 2020 : Foundations of Software Science and Computation Structures : 23rd International Conference, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings
Publication in research information system
MetadataShow full item record
Showing items with similar title or keywords.
A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction Neele, Thomas; Valmari, Antti; Willemse, Tim A. C. (Logical Methods in Computer Science e.V., 2021)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 ...
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)
An efficient functional magnetic resonance imaging data reduction strategy using neighborhood preserving embedding algorithm Zhao, Wei; Li, Huanjie; Hao, Yuxing; Hu, Guoqiang; Zhang, Yunge; Frederick, Blaise de B.; Cong, Fengyu (Wiley, 2022)High dimensionality data have become common in neuroimaging fields, especially group-level functional magnetic resonance imaging (fMRI) datasets. fMRI connectivity analysis is a widely used, powerful technique for studying ...
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 ...