Ordered Navigation on Multi-attributed Data Words

Normann Decker, Peter Habermehl, Martin Leucker, Daniel Thoma


We study temporal logics and automata on multi-attributed data words. Recently, BD-LTL was introduced as a temporal logic on data words extending LTL by navigation along positions of single data values. As allowing for navigation wrt. tuples of data values renders the logic undecidable, we introduce ND-LTL, an extension of BD-LTL by a restricted form of tuple-navigation. While complete ND-LTL is still undecidable, the two natural fragments allowing for either future or past navigation along data values are shown to be Ackermann-hard, yet decidability is obtained by reduction to nested multi-counter systems. To this end, we introduce and study nested variants of data automata as an intermediate model simplifying the constructions. To complement these results we show that imposing the same restrictions on BD-LTL yields two 2ExpSpace-complete fragments while satisfiability for the full logic is known to be as hard as reachability in Petri nets.

Original languageEnglish
Title of host publicationCONCUR 2014 – Concurrency Theory
EditorsPaolo Baldan, Daniele Gorla
Number of pages15
VolumeLNCS 8704
Place of PublicationBerlin
PublisherSpringer Verlag
Publication date01.09.2014
ISBN (Print)978-3-662-44583-9
ISBN (Electronic)978-3-662-44584-6
Publication statusPublished - 01.09.2014
Event25th International Conference on Concurrency Theory
- Rome, Italy
Duration: 02.09.201405.09.2014
Conference number: 107236


Dive into the research topics of 'Ordered Navigation on Multi-attributed Data Words'. Together they form a unique fingerprint.

Cite this