LTL 的 (F,G)-片段的确定性自动机
计算机科学中的逻辑
2015-03-20 v1 形式语言与自动机理论
摘要
在游戏或概率系统等场景中处理线性时序逻辑（LTL）属性时，通常需要将其表示为确定性 omega-自动机。将 LTL 转换为确定性 omega-自动机的传统方法是先将公式转换为非确定性 B"uchi 自动机，然后执行如 Safra 算法之类的确定化过程，从而得到确定性 \omega-自动机。我们提出了一种将 LTL 的 (F,G)-片段直接转换为确定性 \omega-自动机的方法，无需涉及任何确定化过程。由于我们的方法专为 LTL 定制，通常可以避免通用确定化算法导致的典型且不必要的状态爆炸。我们研究了该转换的复杂性，提供了实验结果，并将其与传统方法进行了比较。
引用
@article{arxiv.1204.5057,
title = {Deterministic Automata for the (F,G)-fragment of LTL},
author = {Jan Křetínský and Javier Esparza},
journal= {arXiv preprint arXiv:1204.5057},
year = {2015}
}