Benedikt Bollig ; Alain Finkel ; Amrita Suresh - Branch-Well-Structured Transition Systems and Extensions

lmcs:10394 - Logical Methods in Computer Science, June 12, 2024, Volume 20, Issue 2 - https://doi.org/10.46298/lmcs-20(2:12)2024
Branch-Well-Structured Transition Systems and ExtensionsArticle

Authors: Benedikt Bollig ; Alain Finkel ; Amrita Suresh

    We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable only between states that are reachable one from another. Furthermore, the monotony condition is relaxed in the same way. While this retains the decidability of non-termination and boundedness, it appears that the coverability problem is undecidable. To this end, we define a new notion of monotony, called cover-monotony, which is strictly more general than the usual monotony and still allows us to decide a restricted form of the coverability problem.


    Volume: Volume 20, Issue 2
    Published on: June 12, 2024
    Accepted on: February 17, 2024
    Submitted on: November 30, 2022
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 258 times.
    This article's PDF has been downloaded 111 times.