Expressiveness of propositional projection temporal logic with star

作     者：Tian, Cong Duan, Zhenhua 

作者机构：Xidian Univ ICTT & ISN Lab Xian 710071 Peoples R China 

出 版 物：《THEORETICAL COMPUTER SCIENCE》 (理论计算机科学)

年 卷 期：2011年第412卷第18期

页      面：1729-1744页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Temporal logic Expressiveness Automata theory Regular expressions Verification 

摘      要：This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Buchi automata and omega-regular expressions are first extended as Stutter Buchi 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. (C) 2010 Elsevier B.V. All rights reserved.