良结构迁移系统的正则可分性
Regular Separability of Well Structured Transition Systems
摘要：
本文研究了具有向上兼容性和向下兼容性的良构转换系统（WSTS）所识别的语言。我们的第一个结果表明，在非常温和的假设下，每两个不相交的WSTS语言都是正则可分的：存在一个正则语言包含其中一个，并且与另一个不相交。因此，如果一种语言及其补语都能被WSTS识别，那么它们必然是正则的。特别地，除了正则语言之外，WSTS语言的子类没有一个是在补数下封闭的。我们的第二个结果表明，对于Petri网，向后可覆盖性算法的复杂性产生了一个定期分离器的大小上界。我们用一个下界构造来补充它。
英文摘要：
We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
