Expressiveness of propositional projection temporal logic with star

摘要

This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL~*). To this end, Buchi automata and ω-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.