A4 Article in conference proceedings
The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction (2020)


Neele, Thomas; Valmari, Antti; Willemse, Tim A. C (2020). The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. In Goubault-Larrecq, Jean; König, Barbara (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, Lecture Notes in Computer Science, 12077. Cham: Springer, 482-501. DOI: 10.1007/978-3-030-45231-5_25


JYU authors or editors


Publication details

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

Parent publication: 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

Parent publication editors: Goubault-Larrecq, Jean; König, Barbara

Place and date of conference: Dublin, Ireland, 25.-30.4.2020

ISBN: 978-3-030-45230-8

eISBN: 978-3-030-45231-5

Journal or series: Lecture Notes in Computer Science

ISSN: 0302-9743

eISSN: 1611-3349

Publication year: 2020

Number in series: 12077

Pages range: 482-501

Number of pages in the book: 644

Publisher: Springer

Place of Publication: Cham

Publication country: Switzerland

Publication language: English

DOI: http://doi.org/10.1007/978-3-030-45231-5_25

Open Access: Publication published in an open access channel

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


Abstract

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.


Keywords: data processing; automata theory

Free keywords: model checking; partial-order reduction; stubborn sets


Contributing organizations


Ministry reporting: Yes

Reporting Year: 2020

Preliminary JUFO rating: 1


Last updated on 2020-28-10 at 08:52