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.
翻译:本文对良构转移系统(WSTS)的定义进行了松弛化处理,同时保持了有界性与非终止性的可判定性。在此类系统中,良拟序条件被放宽为仅适用于彼此可达的状态之间。此外,单调性条件也以相同方式进行了松弛。虽然这保留了非终止性与有界性的可判定性,但覆盖性问题似乎变得不可判定。为此,我们定义了一种新的单调性概念,称为覆盖单调性,它严格地推广了通常的单调性,并且仍允许我们判定覆盖性问题的一种受限形式。