On freeze LTL with ordered attributes

DOI10.1007/978-3-662-49630-5_16MaRDI QIDQ2811345zbMATH OpenOpenAlexFDO

Authors Normann Decker, Daniel Thoma

Publication date 10 June 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1504.06355

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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 ordinal-indexed hierarchy of fast-growing complexity classes, a recently introduced framework for non-primitive recursive complexities. This results in completeness for the class $$. We employ nested counter systems and show that they relate to the hierarchy in terms of the nesting depth.

Recommendations

• LTL with the freeze quantifier and register automata
• Safely Freezing LTL
• Ordered navigation on multi-attributed data words
• Temporal logics on words with multiple data values
• Future-Looking Logics on Data Words and Trees

Cites work

• A really temporal logic
• Alternating register automata on finite words and trees
• Demystifying Reachability in Vector Addition Systems
• Hierarchies of modal and temporal logics with reference pointers
• scientific article; zbMATH DE number 1522994 (Why is no real title available?)
• LTL with the freeze quantifier and register automata
• Mixing Lossy and Perfect Fifo Channels
• Modal Logics Between Propositional and First-order
• Ordered navigation on multi-attributed data words
• Ordinal recursive complexity of unordered data nets
• Reasoning about data repetitions with counter systems
• Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets
• Safely Freezing LTL
• Shuffle Expressions and Words with Nested Data
• Temporal logics on words with multiple data values
• The power of priority channel systems
• Two-variable logic on data words

Cited in

(9)

• Complexity hierarchies beyond elementary
• LTL with the freeze quantifier and register automata
• Ordered navigation on multi-attributed data words
• On temporal logics with data variable quantifications: decidability and complexity
• The Parametric Complexity of Lossy Counter Machines
• Consistently-detecting monitors
• Safely Freezing LTL
• The ideal view on Rackoff's coverability technique
• Branching in well-structured transition systems (invited talk)

This page was built for publication: On freeze LTL with ordered attributes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811345)