A1 Journal article (refereed)
A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction (2021)

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

JYU authors or editors

Publication details

All authors or editors: Neele, Thomas; Valmari, Antti; Willemse, Tim A. C.

Journal or series: Logical Methods in Computer Science

eISSN: 1860-5974

Publication year: 2021

Publication date: 27/07/2021

Volume: 17

Issue number: 3

Article number: 8

Publisher: Logical Methods in Computer Science e.V.

Publication country: Germany

Publication language: English

DOI: https://doi.org/10.46298/lmcs-17(3:8)2021

Publication open access: Openly available

Publication channel open access: Open Access channel

Publication is parallel published (JYX): https://jyx.jyu.fi/handle/123456789/77684

Abstract

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.

Keywords: data processing; algorithmics

Free keywords: partial-order reduction; stutter equivalence; LTL; stubborn sets

Contributing organizations

Ministry reporting: Yes

Reporting Year: 2021

JUFO rating: 1