从带过去的线性时序逻辑到确定性 Rabin 自动机的直接转换
形式语言与自动机理论
2024-09-05 v3 计算机科学中的逻辑
摘要
我们提出了一种从带过去的线性时序逻辑到确定性 Rabin 自动机的转换。该转换是直接的，即它不依赖于中间的非确定性自动机，并且是渐近最优的，产生双指数大小的 Rabin 自动机。它基于两个主要概念。其一是，可以通过对公式本身进行简单的重写，将与所考虑公式相关的、包含在词前缀中的历史进行编码。因此，涉及过去算子的公式可以（通过此类重写，这涉及在公式的语法树中交替使用过去算子的弱版本和强版本）在未来任意点被正确求值，而无需在词中进行回溯。其二是，这使得我们能够将纯未来公式的语言可以分解为更简单语言的布尔组合这一结果推广到带过去的线性时序逻辑，对于这些更简单的语言，可以轻松构造具有简单接受条件的确定性自动机。
引用
@article{arxiv.2405.01178,
title = {A Direct Translation from LTL with Past to Deterministic Rabin Automata},
author = {Shaun Azzopardi and David Lidell and Nir Piterman},
journal= {arXiv preprint arXiv:2405.01178},
year = {2024}
}
备注
32 pages. This is the full version of a paper published in MFCS'24. Changes since last version: Minor errata to match published version, and minor fix in one proof