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

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    2 Citaten (Scopus)

    Samenvatting

    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.

    Originele taal-2Engels
    TitelFoundations 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
    RedacteurenJean Goubault-Larrecq, Barbara König
    UitgeverijSpringer
    Pagina's482-501
    Aantal pagina's20
    ISBN van geprinte versie9783030452308
    DOI's
    StatusGepubliceerd - 17 apr 2020
    Evenement23rd 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, Ierland
    Duur: 25 apr 202030 apr 2020

    Publicatie series

    NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume12077 LNCS
    ISSN van geprinte versie0302-9743
    ISSN van elektronische versie1611-3349

    Congres

    Congres23rd 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
    Land/RegioIerland
    StadDublin
    Periode25/04/2030/04/20

    Vingerafdruk

    Duik in de onderzoeksthema's van 'The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction'. Samen vormen ze een unieke vingerafdruk.
    • EATCS Best Paper Award

      Neele, Thomas (Ontvanger), Valmari, A. (Ontvanger) & Willemse, Tim A.C. (Ontvanger), 2 jul 2020

      Prijs: AndersWerk, activiteit of publicatie gerelateerde prijzen (lifetime, best paper, poster etc.)Wetenschappelijk

    Citeer dit