Linear Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness

Abstract. We consider linear time temporal logic enriched with semiextended regular expressions through various operators that have been proposed in the literature, in particular in Accelera’s Property Specification Language. We obtain results about the expressive power of fragments of this logic when restricted to certain operators only: basically, all operators alone suffice for expressive completeness w.r.t. ω-regular expressions, just the closure operator is too weak. We also obtain complexity results. Again, almost all operators alone suffice for EXPSPACEcompleteness, just the closure operator needs some help.

• Type: Conference
• Year: 2007
• Where: CONCUR
• Authors: Martin Lange
• Keywords: Closure Operator, CONCUR 2007, Operator, Semiextended Regular Expressions