דנה פיסמן

Regular-LTL (RLTL), extends LTL with regular expressions, and it is the core of the IEEE standard temporal logic PSL. Safety formulas of RLTL, as well as of other temporal logics, are easier to verify than other formulas. This is because verification of safety formulas can be reduced to invariance checking using an auxiliary automaton recognizing violating prefixes. In this paper we define a special subset of safety RLTL formulas, called RLTL ^LV, for which the automaton built is linear in the size of the formula. We then give two procedures for constructing such an automaton, the first provides a translation into a regular expression of linear size, while the second constructs the automaton directly from the given formula. We have derived the definition of RLTL ^LV by combining several results in the literature, and we devote a major part of the paper to reviewing these results and exploring the involved relationships.