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)定义的放宽,同时保持有界性和非终止性的可判定性。在该类系统中,良拟序(wqo)条件被放宽,仅适用于彼此可达的状态之间。此外,单调性条件也以相同方式放宽。虽然这保留了非终止性和有界性的可判定性,但覆盖性问题是不可判定的。为此,我们定义了一种新的单调性概念,称为覆盖单调性,它严格比通常的单调性更一般,并且仍然允许我们判定覆盖性问题的受限形式。