Temporal Logics with Constraints

• Applicant: Dr. Karin Quaas
• Subject Area: Theoretical Computer Science
• Term: from 2018 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 406907430

• Final Report Year: 2022

Final Report Abstract

Temporal logics are a very popular family of logical languages used to specify abstract properties of systems. Prominent examples are linear temporal logic (LTL) or computation tree logic (CTL). Both logics have decidable satisfiability and model-checking problems. To address the need to express more than just abstract properties, we study temporal logics with constraints that are parameterized by concrete domains. A concrete domain is a relational structure consisting of a potentially infinite domain together with a set of relations defined over the domain. Typical examples of concrete domains are the integers with order, or the set of all finite strings with the prefix order and the suffix order. A constraint is a formula defined in terms of the relational structure; for instance, the constraint Xx < y expresses that the value of the variable x at the next position of the model is smaller than the value of the variable y. Constraints like this form the set of atomic formulas in temporal logics; however, they also appear as labels of transitions of finite automata parameterized by concrete domains, like constraint automata or register automata. Formalisms like these are useful for analysing systems that involve data; the main objective of this project was to study the decidability and the computational complexity of important decision problems like the the satisfiability problem and the model-checking problem for temporal logics, as well as the emptiness problem and the language containment problem for automata. The decidability and the complexity of these problems heavily depend on the concrete domain. A lot of interesting results have already been known before the start of the project. For instance, for the integers with order, the satisfiability problem for LTL is PSPACE-complete, the satisfiability problem for branching-time temporal logics like CTL is decidable (no precise complexity was known), and the emptiness problem for constraint automata is PSPACE-complete. These results have been obtained by several research groups, using different techniques, and an important task of the project was to understand and compare the various methods. A survey of the state of the art concerning logics and automata over concrete domains is published. A main focus of our study was on concrete domains where the domain is the set of all finite strings, together, with, e.g., the subsequence order, or both the prefix and the suffix order. It turned out that for most of these concrete domains, it is hard if not impossible to reuse existing approaches, which work well on concrete domains with linear orders (but the above orders are not linear). For the subsequence order, we were aiming to follow a symbolic approach that was originally introduced for the integers with order, but so far we were not yet able to prove the correctness of our approach. For the concrete domain that includes both the prefix and the suffix order, we could prove decidability of the satisfiability problem for LTL respectively NLOGSPACE-completeness for the emptiness problem for the special case where only a single variable is allowed. This work is published. It is not at all clear whether and how our techniques can be generalized to multiple variables. For unambiguous register automata over the natural numbers with equality, we could build upon our previous work and prove a better complexity result for the universality problem (EXPSPACE- membership). We also prove PSPACE-membership for the same problem for the reals with order and the special case where only a single variable is allowed. Also this work is published.

Publications

• The Containment Problem for Unambiguous Register Automata and Unambiguous Timed Automata. Theory of Computing Systems, 65(4), 706-735.
  Mottet, Antoine & Quaas, Karin
  
• Concrete domains in logics. ACM SIGLOG News, 8(3), 6-29.
  Demri, Stéphane & Quaas, Karin
  
• New Techniques for Universality in Unambiguous Register Automata. In ICALP 2021: 129:1–129:16.
  W. Czerwinski & A. Mottet
  
• Deciding Emptiness for Constraint Automata on Strings with the Prefix and Suffix Order. Accepted at MFCS 2022.
  D. Peteler