# Ordered Navigation on Multi-attributed Data Words

arXiv: https://arxiv.org/abs/1404.6064 · HTML: https://mlsanity.com/paper/1404.6064/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Apr 2014.

## Built on by (most cited first, 1 of 1)

- [Improved Ackermannian lower bound for the Petri nets reachability problem](https://mlsanity.com/paper/2105.08551/) (2021)

## Abstract (arXiv)

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.