On the Construction of Fine Automata for Safety Properties
On the Construction of Fine Automata for Safety Properties
复制标题
安全性能精细自动机的构建
DOI：
10.1007/11901914_11
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Robby Lampert
中科院分区：
文献类型：
--
作者：
O. Kupferman;Robby Lampert
对正式验证特别感兴趣的是安全属性，它断言系统始终保持在某个允许的区域内。每个安全属性ψ可以与一组坏前缀相关联：一组有限计算，使得无限计算违反ψ当且仅当它在该集中有前缀。通过将安全属性转换为其坏前缀集的自动机，验证可以简化为关于有限字的推理：如果系统的所有计算都没有坏前缀，则该系统是正确的。这种转换的一个缺点在于自动机的大小：虽然安全LTL公式ψ到非确定Büchi自动机的转换是指数的，但是它到紧坏前缀自动机的转换是双指数的。紧坏前缀自动机接受ψ的所有坏前缀。库普费尔曼和瓦迪证明，为了验证的目的，一个人可以用一个精细的自动机取代紧密的自动机--一个接受每个违反ψ的无限计算的至少一个坏前缀的自动机。他们还证明了对于许多安全的LTL公式，精细自动机与公式的Büchi自动机具有相同的结构。构造一般安全LTL公式的精细自动机的问题一直悬而未决。在这篇文章中，我们解决了这个问题，并证明了尽管精细自动机一般不能具有与公式的Büchi自动机相同的结构，但精细自动机的大小仍然只是公式长度的指数。
Of special interest in formal verification aresafetyproperties, which assert that the system always stays within some allowed region. Each safety propertyψcan be associated with a set ofbad prefixes: a set of finite computations such that an infinite computation violatesψiff it has a prefix in the set. By translating a safety property to an automaton for its set of bad prefixes, verification can be reduced to reasoning about finite words: a system is correct if none of its computations has a bad prefix. Checking the latter circumvents the need to reason about cycles and simplifies significantly methods like symbolic fixed-point based verification, bounded model checking, and more.A drawback of the translation lies in the size of the automata: while the translation of a safety LTL formulaψto a nondeterministic Büchi automaton is exponential, its translation to a tight bad-prefix automaton — one that accepts all the bad prefixes ofψ, is doubly exponential. Kupferman and Vardi showed that for the purpose of verification, one can replace the tight automaton by a fine automaton — one that accepts at least one bad prefix of each infinite computation that violatesψ. They also showed that for many safety LTL formulas, a fine automaton has the same structure as the Büchi automaton for the formula. The problem of constructing fine automata for general safety LTL formulas was left open. In this paper we solve this problem and show that while a fine automaton cannot, in general, have the same structure as the Büchi automaton for the formula, the size of a fine automaton is still only exponential in the length of the formula.