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 ORCID; Alain Finkel ORCID; Amrita Suresh ORCID

    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
    Funding:
      Source : OpenAIRE Graph
    • POST: Protocols, Observabilities and Session Types; Funder: UK Research and Innovation; Code: EP/T006544/2
    • FoRmal mEthods for the Design of Distributed Algorithms; Funder: French National Research Agency (ANR); Code: ANR-17-CE40-0013
    • Trustworthy and Resilient Decentralised Intelligence for Edge Systems; Funder: European Commission; Code: 101093006
    • IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS; Funder: French National Research Agency (ANR); Code: ANR-17-CE40-0028

    Consultation statistics

    This page has been seen 668 times.
    This article's PDF has been downloaded 182 times.