Expressiveness of propositional projection temporal logic with star
Expressiveness of propositional projection temporal logic with star
复制标题
DOI：
10.1016/j.tcs.2010.12.047
复制
发表时间：
2011-04
期刊：
影响因子：
--
通讯作者：
Cong Tian;Zhenhua Duan
中科院分区：
文献类型：
--
作者：
Cong Tian;Zhenhua Duan
研究了带星星的命题投影时序逻辑（PPTL*）的表达性.为此，Büchi自动机和ω-正则表达式首先被扩展为Stutter Büchi自动机（SBA）和扩展正则表达式（ERE），以包括有限和无限字符串。通过PPTL* 公式、SBAs和ERE之间的等价变换，证明了PPTL* 是完全正则语言的表示.最后，将PPTL * 及其片段分为五个不同的语言类。
This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Büchi automata and ω-regular expressions are first extended as Stutter Büchi Automata (SBA) and Extended Regular Expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL* formulas, SBAs and EREs, PPTL* is proved to represent exactly the full regular language. Moreover, some fragments of PPTL* are characterized, and finally, PPTL* and its fragments are classified into five different language classes.