A4 Artikkeli konferenssijulkaisussa
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-tekijät tai -toimittajat


Julkaisun tiedot

Julkaisun kaikki tekijät tai toimittajat: Neele, Thomas; Valmari, Antti; Willemse, Tim A. C

Emojulkaisu: 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

Emojulkaisun toimittajat: Goubault-Larrecq, Jean; König, Barbara

Konferenssin paikka ja aika: Dublin, Ireland, 25.-30.4.2020

ISBN: 978-3-030-45230-8

eISBN: 978-3-030-45231-5

Lehti tai sarja: Lecture Notes in Computer Science

ISSN: 0302-9743

eISSN: 1611-3349

Julkaisuvuosi: 2020

Sarjan numero: 12077

Artikkelin sivunumerot: 482-501

Kirjan kokonaissivumäärä: 644

Kustantaja: Springer

Kustannuspaikka: Cham

Julkaisumaa: Sveitsi

Julkaisun kieli: englanti

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

Avoin saatavuus: Open access -julkaisukanavassa ilmestynyt julkaisu

Julkaisu on rinnakkaistallennettu (JYX): https://jyx.jyu.fi/handle/123456789/68692


Tiivistelmä

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.


YSO-asiasanat: tietojenkäsittely; automaattien teoria

Vapaat asiasanat: model checking; partial-order reduction; stubborn sets


Liittyvät organisaatiot


OKM-raportointi: Kyllä

Raportointivuosi: 2020

Alustava JUFO-taso: 1


Viimeisin päivitys 2020-28-10 klo 08:52