从LTL与极限确定性Büchi自动机到确定性奇偶自动机
计算机科学中的逻辑
2018-05-04 v1 形式语言与自动机理论
摘要
通用线性时序逻辑（LTL）目标的控制器综合是一项具有挑战性的任务。标准方法涉及通过Safra-Piterman构造将LTL目标转换为确定性奇偶自动机（DPA）。挑战之一是DPA的大小，其在实践中常快速增长，并可能达到LTL公式长度的双指数大小。本文描述了从极限确定性Büchi自动机（LDBA）到DPA的单指数转换，并展示其可与近期高效的LTL到LDBA转换连接，从而产生双指数、无Safra的LTL到DPA构造。我们还报告了一项实现、与SPOT库的比较，以及在多组公式上的性能，包括来自2016年SyntComp竞赛的实例。
引用
@article{arxiv.1701.06103,
title = {From LTL and Limit-Deterministic B\"uchi Automata to Deterministic Parity Automata},
author = {Javier Esparza and Jan Křetínský and Jean-François Raskin and Salomon Sickert},
journal= {arXiv preprint arXiv:1701.06103},
year = {2018}
}