On freeze LTL with ordered attributes

DOI10.1007/978-3-662-49630-5_16zbMATH Open1475.68179arXiv1504.06355OpenAlexW825655794MaRDI QIDQ2811345FDOQ2811345

Authors: Normann Decker, Daniel Thoma 

Publication date: 10 June 2016

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

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (8)

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

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)