Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
复制标题
Rabinizer 2：LTL â GU 的小型确定性自动机
DOI：
10.1007/978-3-319-02444-8_32
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Ruslán Ledesma
中科院分区：
文献类型：
--
作者：
Křetínský;Ruslán Ledesma
我们提出了一个工具，生成LTL（X，F，G，U）的自动机，其中U不出现在任何G-公式（但F仍然可以）。该工具生成的确定性广义拉宾自动机（DGRA）明显小于最先进工具生成的确定性拉宾自动机（DRA）。对于复杂的属性，如公平性约束，差异是在数量级。DGRA最近已经被证明是有用的概率模型检查的，因此在大小的差异直接转化为模型检查过程的速度。
We present a tool that generates automata for LTL(X,F,G,U) whereUdoes not occur in anyG-formula (butFstill can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of magnitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures.