A4 Artikkeli konferenssijulkaisussa
The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction (2020)
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.), 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 (pp. 482-501). Springer. Lecture Notes in Computer Science, 12077. https://doi.org/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
Julkaisun avoin saatavuus: Avoimesti saatavilla
Julkaisukanavan avoin saatavuus: Kokonaan avoin julkaisukanava
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
JUFO-taso: 1
