1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University
We consider linear time temporal logic enriched with semi-extended 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.\ omega-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.
Proc. of the 18th Int. Conf. on Concurrency Theory, 2007, p. 90-104