Michael Blondin ; Alain Finkel ; Pierre McKenzie - Well Behaved Transition Systems

lmcs:3928 - Logical Methods in Computer Science, September 13, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:24)2017
Well Behaved Transition SystemsArticle

Authors: Michael Blondin ; Alain Finkel ; Pierre McKenzie

    The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone transition systems that only require the absence of infinite antichains and call well behaved transitions systems (WBTS) the new strict superclass of the class of WSTS that arises. By contrast, we confirm that boundedness and termination are undecidable for WBTS under the usual hypotheses, and show that stronger monotonicity conditions can enforce decidability. Proofs are similar or even identical to existing proofs but the surprising message is that a hypothesis implicitely assumed minimal for twenty years in the theory of WSTS can meaningfully be relaxed, allowing more orderings to be handled in an abstract way.


    Volume: Volume 13, Issue 3
    Published on: September 13, 2017
    Accepted on: September 13, 2017
    Submitted on: September 13, 2017
    Keywords: Computer Science - Logic in Computer Science,F.1.1,F.3.1

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1921 times.
    This article's PDF has been downloaded 496 times.