The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

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.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures- 23rd International Conference, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings
EditorsJean Goubault-Larrecq, Barbara König
PublisherSpringer
Pages482-501
Number of pages20
ISBN (Print)9783030452308
DOIs
Publication statusPublished - 17 Apr 2020
Event23rd International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Ireland
Duration: 25 Apr 202030 Apr 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12077 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
CountryIreland
CityDublin
Period25/04/2030/04/20

Fingerprint Dive into the research topics of 'The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction'. Together they form a unique fingerprint.

  • Prizes

    EATCS Best Paper Award

    Neele, Thomas S. (Recipient), Antti Valmari (Recipient) & Willemse, Tim A.C. (Recipient), 2 Jul 2020

    Prize: OtherCareer, activity or publication related prizes (lifetime, best paper, poster etc.)Scientific

  • Cite this

    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.), Foundations of Software Science and Computation Structures- 23rd International Conference, FOSSACS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings (pp. 482-501). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12077 LNCS). Springer. https://doi.org/10.1007/978-3-030-45231-5_25