Temporal Logics with Constraints

有约束的时态逻辑

• 批准号: 406907430
• 负责人: Dr. Karin Quaas
• 金额: --
• 依托单位: Abteilung Algebraische und logische Grundlagen der Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2018
• 资助国家: 德国
• 起止时间: 2017-12-31 至 2021-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/406907430?language=en
• 关键词: Temporal; Logics; Constraints

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.

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