一句话：提出分支良结构迁移系统，放宽良拟序与单调性，保持有界性/非终止性可判定，并界定覆盖性可判定边界。
良结构迁移系统（WSTS）是分析无限状态系统的经典框架，但其良拟序与单调性条件要求过强。本文提出分支良结构迁移系统：仅要求互相可达的状态之间满足良拟序，并以同样方式弱化单调性。作者证明，在该松弛定义下，有界性与非终止性仍然可判定；然而一般覆盖性问题变为不可判定。为此，论文进一步引入 cover-monotony——一种严格弱于通常单调性的新条件，并证明在满足 cover-monotony 的系统中，受限形式的覆盖性问题仍可判定。该工作刻画了 WSTS 可判定性的边界，为更广泛系统的验证提供了理论工具。
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.
@article{paperbot2756,
title = {Branch-Well-Structured Transition Systems and Extensions},
author = {Benedikt Bollig and Alain Finkel and Amrita Suresh},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 2},
year = {2024},
doi = {10.46298/lmcs-20(2:12)2024}
}