一句话：引入泛化子词序的良拟序，将分段可测语言可分离性与向下闭包计算归约到同时无界问题，并证明一阶片段 BΣ1[<, mod] 的可分离性可判定。
论文引入一类词上的灵活良拟序（WQO），它推广了（不一定连续的）子词序。每个这样的 WQO 都诱导出一类分段可测语言（PTL），即向上闭集的布尔组合，从而产生多种正则语言类作为 PTL；同时每个 WQO 都保证所有向下闭集是正则的。作者研究两个问题：给定语言能否被相对于某 WQO 的 PTL 分离，以及如何有效计算相对于这些 WQO 的向下闭包。主要结果表明，在温和假设下，这两个问题都可归约到同时无界问题（SUP），因而对许多强系统模型可判定。作为应用，论文证明正则语言被一阶逻辑片段 BΣ1[<, mod]（含模谓词）分离的可判定性。
We introduce a flexible class of well-quasi-orderings (WQOs) on words that generalizes the ordering of (not necessarily contiguous) subwords. Each such WQO induces a class of piecewise testable languages (PTLs) as Boolean combinations of upward closed sets. In this way, a range of regular language classes arises as PTLs. Moreover, each of the WQOs guarantees regularity of all downward closed sets. We consider two problems. First, we study which (perhaps non-regular) language classes allow to decide whether two given languages are separable by a PTL with respect to a given WQO. Second, we want to effectively compute downward closures with respect to these WQOs. Our first main result is that for each of the WQOs, under mild assumptions, both problems reduce to the simultaneous unboundedness problem (SUP) and are thus solvable for many powerful system models. In the second main result, we apply the framework to show decidability of separability of regular languages by B∑1[<, mod], a fragment of first-order logic with modular predicates.
DOI 原文 ·
@inproceedings{paperbot4342,
title = {Separability by piecewise testable languages and downward closures beyond subwords},
author = {Georg Zetzsche},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209201}
}