Temporal Logics over Finite Strings with the Prefix Order

点击翻译按钮获取中文摘要

Temporal logics form one of the most important logical formalisms to express properties of abstract systems. Prominent examples of temporal logics are linear-time logic LTL and branching-time logics like CTL and CTL*. While being perfect to express abstract properties, these logics cannot express properties referring to concrete data values. Various extensions of temporal logics have been introduced and studied in order to address the obvious need for expressing such concrete properties. In this project, we focus on the family of temporal logics with constraints, that are parameterized by concrete domains. A concrete domain consists of a domain and a set of relation symbols, interpreted over the domain. Typical examples of concrete domains are (N;=) - the nonnegative integers with equality - or (R;<) - the real numbers with the usual ordering. Many interesting results have been achieved for temporal logics with constraints during the past years. The main problem under study is the satisfiability problem, i.e., the question whether a given formula has a model. While the satisfiability problem is decidable for the classical temporal logics (PSPACE-complete for LTL, 2EXPTIME-completen for CTL*), the complexity of this problem depends obviously on the concrete domain. For instance, it is easy to prove that the satisfiability problem LTL over (N;+) is undecidable; in contrast, it is PSPACE-complete for LTL over the class of linear orders. As a starting point for this project, we take the concrete domain of the set of finite string over an alphabet and the prefix order. This concrete domain is interesting from a practical point of view, with a lot of interesting applications e.g. in database applications, model checking, or bioinformatic. From a theoretical point of view, the prefix order is interesting, too: it is a partial order, so that standard methods developed for linear orders do not apply. It coincides with the predecessor relation of a complete tree, and the monadic second-order logics over this concrete domain is decidable. Also, for all temporal logics mentioned above, it is already known that the satisfiability problem is decidable, and PSPACE-complete for LTL. These results have been achieved using various interesting techniques, including an encoding into (N;<) and methods from the theory of well-quasi-orderings and model theory. We aim to further explore these techniques with the concrete goals to establish, amongst others, the precise complexity for the satisfiability problem for branching-time temporal logics, and the decidability status for temporal logics for concrete domains where we add to the prefix order other relations like regularity predicates and the suffix order. Besides providing the verification community with more temporal logics that can be used to model realistic applications, one main objective of this project to gain a deeper understanding about temporal logics with string constraints, and constraints in general.