On Freeze LTL with Ordered Attributes

Normann Decker, Daniel Thoma


This paper is concerned with Freeze LTL, a temporal logic on data words with registers. In a (multi-attributed) data word each position carries a letter from a finite alphabet and assigns a data value to a fixed, finite set of attributes. The satisfiability problem of Freeze LTL is undecidable if more than one register is available or tuples of data values can be stored and compared arbitrarily. Starting from the decidable one-register fragment we propose an extension that allows for specifying a dependency relation on attributes. This restricts in a flexible way how collections of attribute values can be stored and compared. This conceptual dimension is orthogonal to the number of registers or the available temporal operators. The extension is strict. Admitting arbitrary dependency relations, satisfiability becomes undecidable. Tree-like relations, however, induce a family of decidable fragments escalating the ordinalindexed hierarchy of fast-growing complexity classes, a recently introduced framework for non-primitive recursive complexities. This results in completeness for the class Fϵ0 . We employ nested counter systems and show that they relate to the hierarchy in terms of the nesting depth.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Number of pages16
Place of PublicationBerlin
PublisherSpringer Verlag
Publication date01.01.2016
ISBN (Print)978-3-662-49629-9
ISBN (Electronic)978-3-662-49630-5
Publication statusPublished - 01.01.2016
Event19th International Conference on Foundations of Software Science and Computation Structures - Eindhoven, Netherlands
Duration: 02.04.201608.04.2016
Conference number: 172389


Dive into the research topics of 'On Freeze LTL with Ordered Attributes'. Together they form a unique fingerprint.

Cite this