Temporal Logics with 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.