SeqLTL and ωLTL

Abstract

Linear Temporal Logic (LTL) is worthwhile for its applications in, among others, model checking, runtime verification and reactive synthesis. However, many useful properties are not expressible in LTL, or not in a natural way. We find that existing solutions rely on low-level constructions such as regular expressions and automata, or new less intuitive operators. We suggest the language SeqLTL, which uses tight witnesses to gain expressiveness and succinctness, compared to LTL. This language is arguably more intuitive and compositional—which can be useful for applications like reactive synthesis, where the state explosion is limiting. As SeqLTL does not reach full ω-regularity, we present an additional language, ωLTL, that uses the same underlying concept for full ω-regular expressive power, although at an extra exponential cost in the translation to automata. To evaluate the results we consider expressiveness, succinctness and example properties. We find an example that suggests SeqLTL is combinatorially more succinct than LTL. Based on an extended version of this example, we conjecture that SeqLTL is still more succinct than that.