2014/04/24 by Normann Decker, Decker, Normann, Peter Habermehl +5 · 1 citation
Computer Science · #F.1.1 #F.4.1 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling #Semantic Web and Ontologies #Service-Oriented Architecture and Web Services
paper · pdf · doi:10.48550/arxiv.1404.6064
openalex publication_date 2014/04/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.