LTL with Local and Remote Data Constraints

TL;DR

This paper extends linear-time temporal logic with local and remote data constraints, proving the decidability of its satisfiability problem and highlighting the limits of increasing its expressiveness.

Contribution

It introduces a new extension of LTL with data constraints and demonstrates its decidability, building on previous logics and exploring the boundaries of expressiveness.

Findings

Satisfiability for the extended logic is decidable.

Extending the logic's expressiveness can lead to undecidability.

The extension builds on constraint LTL and the Temporal Logic of Repeating Values.

Abstract

We consider an extension of linear-time temporal logic (LTL) with both local and remote data constraints interpreted over a concrete domain. This extension is a natural extension of constraint LTL and the Temporal Logic of Repeating Values, which have been studied before. We shall use previous results to prove that the satisfiability problem for this logic is decidable. Further, we shall see that trying to extend this logic by making it more expressive can lead to undecidability.