From LTL to deterministic automata
From LTL to deterministic automata
复制标题
从 LTL 到确定性自动机
DOI：
10.1007/s10703-016-0259-2
复制
发表时间：
2016
影响因子：
0.8
通讯作者：
Salomon Sickert
中科院分区：
文献类型：
--
作者：
Javier Esparza;Jan Kretínský;Salomon Sickert
提出了一种构造LTL公式的（广义）确定性Rabin自动机的新算法。自动机是一个co- b<s:1>自动机和一组Rabin自动机的乘积，每个Rabin自动机的子公式一个。拉宾的自动机负责识别是否存在。该信息被传递给决定是否接受的co- bchi自动机。与基于Safra确定的标准过程相反，我们所有自动机的状态都有一个清晰的逻辑结构，可以进行各种优化。实验结果表明，与现有方法相比，所得到的自动机的大小有所改善。
We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula. The automaton is the product of a co-Büchi automaton forand an array of Rabin automata, one for each-subformula of. The Rabin automaton foris in charge of recognizing whetherholds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.