Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
复制标题
在无限词上寻找自动机非空性的最短见证
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Sarai Sheinvald
中科院分区：
文献类型：
--
作者：
O. Kupferman;Sarai Sheinvald
在形式验证的自动机理论方法中，线性时序逻辑的可满足性和模型检查问题被简化为无限字上自动机的非空性问题。修改非空性算法以返回非空性的最短见证（即自动机接受的 uvω 形式的单词，且 |uv| 最小）在综合和反例分析中具有应用。与文献中研究的最短接受运行不同，最短见证的定义是语义的，并且独立于属性或系统的规范形式主义。特别是，它的鲁棒性使其适合分析并发系统的反例。
我们研究在具有各种并发类型的自动机中寻找最短见证人的问题。我们表明，虽然寻找最短见证比仅检查非确定性和并发计算模型中的非空性更复杂，但在交替模型中并不更复杂。由此可见，当系统是并发组件组成时，找到一个最短的反例来证明其正确性并不比找到一些反例更难。我们的结果给出了将时间逻辑公式转换为交替自动机的计算动机，而不是一直转换为非确定性自动机。
In the automata-theoretic approach to formal verification, the satisfiability and the model-checking problems for linear temporal logics are reduced to the nonemptiness problem of automata on infinite words. Modifying the nonemptiness algorithm to return a shortest witness to the nonemptiness (that is, a word of the form uvω that is accepted by the automaton and for which |uv| is minimal) has applications in synthesis and counterexample analysis. Unlike shortest accepting runs, which have been studied in the literature, the definition of shortest witnesses is semantic and is independent on the specification formalism of the property or the system. In particular, its robustness makes it appropriate for analyzing counterexamples of concurrent systems.
We study the problem of finding shortest witnesses in automata with various types of concurrency. We show that while finding shortest witnesses is more complex than just checking nonemptiness in the nondeterministic and in the concurrent models of computation, it is not more complex in the alternating model. It follows that when the system is the composition of concurrent components, finding a shortest counterexample to its correctness is not harder than finding some counterexample. Our results give a computational motivation to translating temporal logic formulas to alternating automata, rather than going all the way to nondeterministic automata.