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. © 2010 Elsevier B.V. All rights reserved.
Tian, C., & Duan, Z. (2011). Expressiveness of propositional projection temporal logic with star. In Theoretical Computer Science (Vol. 412, pp. 1729–1744). https://doi.org/10.1016/j.tcs.2010.12.047