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

Thomas Neele; Antti Valmari; Tim A.C. Willemse

doi:10.1007/978-3-030-45231-5_25

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

Thomas Neele, Antti Valmari, Tim A.C. Willemse

EAISI High Tech Systems

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

4 Citations (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 language	English
Title of host publication	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
Editors	Jean Goubault-Larrecq, Barbara König
Publisher	Springer
Pages	482-501
Number of pages	20
ISBN (Print)	9783030452308
DOIs	https://doi.org/10.1007/978-3-030-45231-5_25
Publication status	Published - 17 Apr 2020
Event	23rd 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 2020 → 30 Apr 2020

Publication series

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

Conference

Conference	23rd 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
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20

Access to Document

10.1007/978-3-030-45231-5_25

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

Neele, Thomas ; Valmari, Antti ; Willemse, Tim A.C. / The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. 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. editor / Jean Goubault-Larrecq ; Barbara König. Springer, 2020. pp. 482-501 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{fd8390c0ff41401b9537f020653a6fa7,

title = "The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction",

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.",

author = "Thomas Neele and Antti Valmari and Willemse, {Tim A.C.}",

year = "2020",

month = apr,

day = "17",

doi = "10.1007/978-3-030-45231-5_25",

language = "English",

isbn = "9783030452308",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "482--501",

editor = "Jean Goubault-Larrecq and Barbara K{\"o}nig",

booktitle = "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",

address = "Germany",

note = "23rd 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 ; Conference date: 25-04-2020 Through 30-04-2020",

}

Neele, T, Valmari, A & Willemse, TAC 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12077 LNCS, Springer, pp. 482-501, 23rd 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, 25/04/20. https://doi.org/10.1007/978-3-030-45231-5_25

The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. / Neele, Thomas; Valmari, Antti; Willemse, Tim A.C.
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. ed. / Jean Goubault-Larrecq; Barbara König. Springer, 2020. p. 482-501 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12077 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Neele, Thomas

AU - Valmari, Antti

AU - Willemse, Tim A.C.

PY - 2020/4/17

Y1 - 2020/4/17

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85083963614&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-45231-5_25

DO - 10.1007/978-3-030-45231-5_25

M3 - Conference contribution

AN - SCOPUS:85083963614

SN - 9783030452308

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 482

EP - 501

BT - 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

A2 - Goubault-Larrecq, Jean

A2 - König, Barbara

PB - Springer

T2 - 23rd 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

Y2 - 25 April 2020 through 30 April 2020

ER -

Neele T, Valmari A, Willemse TAC. The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. In Goubault-Larrecq J, König B, editors, 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. Springer. 2020. p. 482-501. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-45231-5_25

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

EATCS Best Paper Award

Cite this

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Prizes

EATCS Best Paper Award

Cite this