Branch-Well-Structured Transition Systems and Extensions

TL;DR

This paper introduces a relaxed class of well-structured transition systems that maintains decidability for boundedness and non-termination, but explores the implications for coverability and proposes a new monotony concept.

Contribution

It defines branch-well-structured transition systems with relaxed conditions and introduces cover-monotony, expanding the theoretical framework for analyzing transition systems.

Findings

Decidability of boundedness and non-termination is preserved.

Coverability becomes undecidable in the relaxed system.

Introduction of cover-monotony for restricted coverability analysis.

Abstract

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.