论文标题
线性时间逻辑和非常弱的交替自动机的有效归一化过程
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
论文作者
论文摘要
在80年代中期，Lichtenstein，Pnueli和Zuck证明了一个经典的定理，表明过去的LTL的每个公式（LTL与过去的运营商的扩展）相当于$ \ bigWedge_ {i = 1}^n \ Mathbf {G}^g} {g} {g} \ nathbf {g} \ Mathbf {f} \ Mathbf {g}ψ_i$，其中$φ_i$和$ψ_i$仅包含过去的运营商。几年后，Chang，Manna和Pnueli建立在此结果基础上，从而得出了LTL的类似正常形式。这两种归一化过程均具有非元素最差的爆炸，并遵循从公式到无抗衡自动机再到无星条正则表达式的涉及路径，再到公式。我们在这两个点上有所提高。我们提出了一种直接且纯粹的句法归一化程序，用于LTL产生正常形式，与Chang，Manna和Pnueli相当，该形式仅具有单个指数爆炸。作为应用程序，我们得出了一种简单的算法，以将LTL转换为确定性的Rabin Automata。该算法将公式归一化，将其转换为特殊的非常弱的交替自动机，并应用了一个简单的确定过程，仅适用于这些特殊的自动机。
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} φ_i \vee \mathbf{F}\mathbf{G} ψ_i$, where $φ_i$ and $ψ_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.
