Expressiveness of propositional projection temporal logic with star |
| |
Authors: | Cong TianZhenhua Duan |
| |
Affiliation: | ICTT and ISN Laboratory, Xidian University, Xi’an, 710071, PR China |
| |
Abstract: | 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. |
| |
Keywords: | Temporal logic Expressiveness Automata theory Regular expressions Verification |
本文献已被 ScienceDirect 等数据库收录! |
|