Automata Constructions for LTL with Past
No Thumbnail Available
Date
2024
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Department of Computer Science and Engineering University of Gothenburg | Chalmers University of Technology
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.
Description
Keywords
Linear temporal logic, ω-automata, model checking, reactive synthesis