We propose a relaxation to the definition of well-structured transition systems (WSTS) while retaining the decidability of boundedness and termination. In our class, we ease the well-quasi-ordered (wqo) condition to be applicable only between states that are reachable one from another. Furthermore, we also relax the monotony condition in the same way. While this retains the decidability of 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)条件放宽至仅适用于彼此可达的状态之间。此外,我们以相同方式放宽单调性条件。虽然这保留了终止性和有界性的可判定性,但覆盖性问题被证明是不可判定的。为此,我们定义了一种新的单调性概念——覆盖单调性,它严格比通常的单调性更一般,并且仍然允许我们判定覆盖性问题的受限形式。