Converting A Subset of LTL Formula to Buchi Automata
Converting A Subset of LTL Formula to Buchi Automata
复制标题
将 LTL 公式的子集转换为 Buchi 自动机
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Ali Kansou
中科院分区：
文献类型：
--
作者：
B. Kanso;Ali Kansou
将线性时态逻辑（LTL）公式转换为等价的布奇自动机在许多LTL模型检验算法中起着重要作用，这些算法包括获取一个等同于软件系统规范的布奇自动机以及另一个等同于属性否定的布奇自动机。如果模型满足该属性，那么这两个布奇自动机的交集为空。
在最坏的情况下，生成与一个LTL公式对应的布奇自动机在公式规模上可能是指数级的，这使得模型检验的工作量在原始公式规模上是指数级的。对于检查交集的空性没有多项式解。这源于将LTL公式转换为有限状态模型的步骤。这使得验证方法在实践中难以甚至无法实施。在本文中，我们提出了LTL公式的一个子集，它可以转换为规模是多项式的布奇自动机。
The translation of LTL formula into equivalent Buchi automata plays an important role in many algorithms for LTL model checking, which consist in obtaining a Buchi automaton that is equivalent to the software system specification and another one that is equivalent to the negation of the property. The intersection of the two Buchi automata is empty if the model satisfies the property.
Generating the Buchi automaton corresponding to an LTL formula may, in the worst case, be exponential in the size of the formula, making the model checking effort exponential in the size of the original formula. There is no polynomial solution for checking emptiness of the intersection. That comes from the translation step of LTL formula into finite state models. This makes verification methods hard or even impossible to be implemented in practice. In this paper, we propose a subset of LTL formula which can be converted to Buchi automata whose the size is polynomial.