Temporal Logics over Finite Strings with the Prefix Order

时态逻辑是表达抽象系统性质的最重要的逻辑形式之一。时间逻辑的突出例子是线性时间逻辑LTL和分支时间逻辑，如CTL和CTL*。虽然这些逻辑非常适合表达抽象属性，但它们无法表达涉及具体数据值的属性。时态逻辑的各种扩展已经被引入和研究，以解决表达这些具体属性的明显需求。在这个项目中，我们专注于家庭的时间逻辑的约束，这是参数化的具体领域。一个具体的域由一个域和一组关系符号组成，关系符号在域上被解释。具体域的典型例子是（N;=）-具有相等性的非负整数-或（R;<）-具有通常顺序的真实的数。在过去的几年中，已经取得了许多有趣的结果的时间逻辑的约束。研究的主要问题是可满足性问题，即，一个给定的公式是否有一个模型。虽然可满足性问题对于经典的时态逻辑是可判定的（对于LTL是PSPACE-完全的，对于CTL* 是2 EXPTIME-完全的），但是这个问题的复杂性显然依赖于具体的域。例如，很容易证明（N;+）上的可满足性问题LTL是不可判定的;相反，线性序类上的LTL是PSPACE完全的。作为这个项目的出发点，我们采取的有限字符串的集合在一个字母表和前缀顺序的具体域。从实用的角度来看，这个具体的领域是有趣的，有很多有趣的应用，例如数据库应用，模型检查或生物信息学。从理论的角度来看，前缀序也很有趣：它是一个偏序，因此为线性序开发的标准方法不适用。它与完备树的前趋关系相一致，并且在这个具体域上的一元二阶逻辑是可判定的。此外，对于上述所有时态逻辑，已知可满足性问题是可判定的，并且对于LTL是PSPACE完全的。这些结果是使用各种有趣的技术实现的，包括编码到（N;<）和方法从理论的良好准序和模型理论。我们的目标是进一步探索这些技术的具体目标，以建立，除其他外，精确的复杂性分支时间时序逻辑的可满足性问题，和时序逻辑的具体域的可判定性状态，我们添加到前缀顺序其他关系，如规律性谓词和后缀顺序。除了为验证社区提供更多的时态逻辑，可用于建模现实的应用程序，这个项目的一个主要目标是获得更深入的了解时态逻辑与字符串约束，一般的约束。

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.