LTL$_f$ 约束下具有当前状态不确定性的自动机遍历
形式语言与自动机理论
2023-11-30 v1 计算机科学中的逻辑
摘要
在本文中，我们考虑一个我们称之为路径上的 LTL 模型检测的问题：给定一个 DFA 和一个有限迹上的 LTL 公式 ，是否存在一个词 ，使得从 的某个状态出发且标记为 的每条路径都满足 ？该问题的原始动机来自 [Petra Wolf, “Synchronization Under Dynamic Constraints”, FSTTCS 2020] 中引入的约束零件定向问题，其中输入约束限制了在读取词 （该词还需同步 ）时某些状态首次或末次被访问的顺序。我们确定了路径上的 LTL 模型检测可在多项式空间内可解的非常一般的条件。对于零件定向问题中的特定约束，我们考虑了 PSPACE 完全的情况和一个 NP 完全的情况。前者为路径上的 LTL 模型检测提供了很强的下界。后者与仅含 until 模态且无算子嵌套的（经典）LTL 模型检测相关。我们还考虑了给定 DFA 的幂集自动机的 LTL 模型检测，并对此设定得到了类似结果。对于我们所有的问题，我们考虑所需词还必须同步的情况，并证明若问题未变为平凡，则该附加约束不改变复杂度。
引用
@article{arxiv.2311.17849,
title = {Traversing automata with current state uncertainty under LTL$_f$ constraints},
author = {Andrew Ryzhikov and Petra Wolf},
journal= {arXiv preprint arXiv:2311.17849},
year = {2023}
}