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 EXPSPACE-completeness, just the closure operator needs some help. © Springer-Verlag Berlin Heidelberg 2007.