# Deterministic Temporal Logics and Interval Constraints

## TL;DR

This paper explores deterministic temporal logics with interval constraints, analyzing their expressive power and decision problem complexities, and introduces tools like Rankers to characterize these logics over finite words.

## Contribution

It introduces a unified framework for deterministic temporal logics with interval constraints, characterizes their expressive power, and analyzes their computational complexity.

## Key findings

- All these logics have NP satisfiability.
- Recursive modalities extend logic to full first-order expressiveness.
- Interval constraints lead to PSpace complexity.

## Abstract

In temporal logics, a central question is about the choice of modalities and their relative expressive power, in comparison to the complexity of decision problems such as satisfiability. In this tutorial, we will illustrate the study of such questions over finite word models, first with logics for Unambiguous Starfree Regular Languages (UL), originally defined by Schutzenberger, and then for extensions with constraints, which appear in interval logics. We present Deterministic temporal logics, with diverse sets of modalities, which also characterize UL. The tools and techniques used go under the name of "Turtle Programs" or "Rankers". These are simple kinds of automata. We use properties such as Ranker Directionality and Ranker Convexity to show that all these logics have NP satisfiability. A recursive extension of some of these modalities gives us the full power of first-order logic over finite linear orders. We also discuss Interval Constraint modalities extending Deterministic temporal logics, with intermediate expressiveness. These allow counting or simple algebraic operations on paths. The complexity of these extended logics is PSpace, as of full temporal logic (and ExpSpace when using binary notation).