Temporal Logics with Constraints

时间逻辑是一个非常流行的逻辑语言家族，用于指定抽象系统的属性。时间逻辑的突出例子是线性时间逻辑LTL和分支时间逻辑CTL和CTL*。为了满足表达不仅仅是抽象属性的需求，已经提出了这些逻辑的各种扩展。具有局部约束的时间逻辑是在经典时间逻辑的基础上，用具体域的约束代替原子命题而得到的。这样的约束允许在一个词的有限（局部）距离内表示有限数量变量的数据值之间的关系。与此相反，具有全局约束的时间逻辑能够表示先验无界的单词位置上的数据值的条件。为了实现这一点，像LTL这样的经典逻辑使用某些语法工具进行扩展；例如，逻辑MTL允许对具有时间约束的时态模式进行注释，逻辑Freeze LTL使用冻结量词，该量词可用于将当前数据值存储到寄存器中，以便以后进行比较。这两种带约束的时间逻辑都是验证界积极研究的焦点。对于正在研究的两个主要问题，即可满足性问题和模型检验问题，最近取得了显著的新成果，在某些情况下是借助有前途的创新技术。我们项目的目标是进一步探索这些新技术，以便更好地理解具有可判决性和计算复杂性约束的时间逻辑。我们的工作计划分为三个主线：具有(i)局部约束的时间逻辑，（ii）全局约束，以及（iii）局部和全局约束。对于(1)，最重要的问题是哪些具体域的可满足性问题是可确定的。我们计划调查最近提出的方法的全部潜力。对于具有可判定可满足性问题的具体域，我们要研究其计算复杂度。此外，我们想研究约束满足相关领域的技术是否可以应用。对于（ii），我们的重点将放在MTL和Freeze LTL的非负整数和片段上的数据字上，在实时验证领域，已经取得了一些有希望的结果。在项目的最后阶段，我们计划将我们对本地和全球约束的研究结合起来，并将这两个特征整合到（iii）中。响应时间逻辑领域的最新趋势，我们还计划解决正在研究的逻辑的参数版本。

Temporal logics are a very popular family of logical languages, used to specify properties of abstract systems. Prominent examples of temporal logics are the linear-time logic LTL and the branching-time logics CTL and CTL*. To address the need to express more than just abstract properties, a variety of extensions of these logics have been proposed. Temporal logics with local constraints are obtained from classical temporal logics by replacing atomic propositions by constraints in a concrete domain. Such constraints allow to express relations between the data values of a finite number of variables within a bounded (local) distance of a word. In contrast to this, temporal logics with global constraints are able to express conditions on the data values in positions of a word that are a priori unbounded. To achieve this, classical logics like LTL are extended with certain syntactical tools; for instance, the logic MTL allows the annotation of the temporal modalities with time constraints, and the logic Freeze LTL uses a freeze quantifier that can be used to store the current data value into a register for later comparisons. Both kinds of temporal logics with constraints are in the focus of active research in the verification community. For the two main problems under study, the satisfiability problem and the model-checking problem, remarkable new results have recently been achieved, in some cases with the help of promising innovative techniques. The goal of our project is to explore further these and new techniques with the aim to obtain a better understanding of temporal logics with constraints in terms of decidability and computational complexity. Our work program is structured into three main threads: temporal logics with (i) local constraints, (ii) global constraints, and (iii) local and global constraints. For (i), the most important question is for which concrete domains the satisfiability problem is decidable. We plan to investigate the full potential of recently proposed methods. For concrete domains with decidable satisfiability problem, we want to study the computational complexity. In addition, we would like to investigate whether techniques from the related field of constraint satisfaction can be applied. For (ii), our focus will be on data words over the nonnegative integers and fragments of MTL and Freeze LTL, for which, in the area of real-time verification, some promising results have been achieved. In the final stage of the project, we plan to combine our studies on local and global constraints and integrate both features into (iii). Responding to recent trends in the domain of temporal logics, we also plan to address parametric versions of the logics under study.