通过线性因子构建 LTL 语义表与交替$\omega$-自动机
形式语言与自动机理论
2017-10-19 v1
摘要
线性时序逻辑（LTL）是用于系统线性时间属性的广泛使用的规范框架。验证此类属性的标准方法是将 LTL 公式转换为合适的-自动机，然后应用模型检测。我们重新审视了 Vardi 将 LTL 公式转换为交替-自动机的方法，以及 Wolper 用于可满足性检验的 LTL 表方法。我们观察到，这两种构造实际上都依赖于将公式分解为线性因子。线性因子此前由 Antimirov 在正则表达式的背景下引入。我们为 LTL 建立了线性因子的概念，并验证了扩展性和有限性等基本性质。我们的结果揭示了交替-自动机构造与语义表之间的联系，提供了新的见解。
引用
@article{arxiv.1710.06678,
title = {LTL Semantic Tableaux and Alternating $\omega$-automata via Linear Factors},
author = {Martin Sulzmann and Peter Thiemann},
journal= {arXiv preprint arXiv:1710.06678},
year = {2017}
}