一句话：证明仅需无无限反链的单调迁移系统仍可判定覆盖性，并定义其严格超类 WBTS。
本文研究定义 well-structured transition systems（WSTS）的 well-quasi-ordering 是否是可判定 coverability 的最弱假设。作者放松良拟序条件，只要求单调迁移系统不存在无限反链，并将由此得到的 WSTS 真超类称为 well behaved transition systems（WBTS）。他们证明 WBTS 上 coverability 仍然可判定；但在通常假设下，boundedness 与 termination 对 WBTS 不可判定，并表明更强的单调性条件可强制这些问题的可判定性。证明与已有 WSTS 证明类似甚至相同，但结论出人意料：二十年来被视为最小的隐含假设可被有意义地放松，从而以抽象方式处理更多序关系。
The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone transition systems that only require the absence of infinite antichains and call well behaved transitions systems (WBTS) the new strict superclass of the class of WSTS that arises. By contrast, we confirm that boundedness and termination are undecidable for WBTS under the usual hypotheses, and show that stronger monotonicity conditions can enforce decidability. Proofs are similar or even identical to existing proofs but the surprising message is that a hypothesis implicitely assumed minimal for twenty years in the theory of WSTS can meaningfully be relaxed, allowing more orderings to be handled in an abstract way.Comment: 19 pages, 3 figures
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BlondinFM17,
title = {Well Behaved Transition Systems},
author = {Michael Blondin and Alain Finkel and Pierre McKenzie},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:24)2017}
}