Automata Constructions for LTL with Past

Abstract

Linear temporal logic (LTL) is a popular language in formal verification, especially in the domains of model checking and reactive synthesis. Because its semantics is defined in terms of infinite sequences of symbols that can be interpreted as system variables, it is suitable for expressing how the state of a continuously operating system evolves over time. Due to the tight connection between the semantics of LTL and that of automata over infinite words, and because many common approaches to formal verification are automata-theoretic in nature, it is not surprising that various translations from LTL to automata over infinite words have been developed over the years, both for theoretical and practical purposes. Although many properties are naturally and succinctly expressed in terms of past events, the majority of these translations are restricted to formulae that only refer to the present and future. Those that do handle past are often indirect or lead to automata with an unnecessarily large number of states. In this thesis we present several translations from linear temporal logic with past to various types of automata over infinite words. We also suggest a framework for extending existing tools that are based on manipulating LTL formulae to handle past, together with a prototype tool intended to serve as a proof of this concept.