Constructing Automata from Temporal Logic Formulas: A Tutorial
Constructing Automata from Temporal Logic Formulas: A Tutorial
复制标题
DOI：
10.1007/3-540-44667-2_7
复制
发表时间：
2002-01
期刊：
影响因子：
--
通讯作者：
P. Wolper
中科院分区：
文献类型：
--
作者：
P. Wolper
本文介绍了如何利用线性时间时态逻辑公式来构造无限字上的有限自动机。在定义了源形式和目标形式之后，描述了第一个结构，它的正确性很容易建立，但其行为总是等于最坏情况的上界。然后转向可以用来改进该算法的技术，以便获得现在正在使用的相当有效的算法。
This paper presents a tutorial introduction to the construction of finite-automata on infinite words from linear-time temporal logic formulas. After defining the source and target formalisms, it describes a first construction whose correctness is quite direct to establish, but whose behavior is always equal to the worst-case upper bound. It then turns to the techniques that can be used to improve this algorithm in order to obtain the quite effective algorithms that are now in use.