Abstract
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 language | English |
|---|---|
| Title of host publication | CONCUR 2014 – Concurrency Theory |
| Editors | Paolo Baldan, Daniele Gorla |
| Number of pages | 15 |
| Volume | LNCS 8704 |
| Place of Publication | Berlin |
| Publisher | Springer Verlag |
| Publication date | 01.09.2014 |
| Pages | 497-511 |
| ISBN (Print) | 978-3-662-44583-9 |
| ISBN (Electronic) | 978-3-662-44584-6 |
| DOIs | |
| Publication status | Published - 01.09.2014 |
| Event | 25th International Conference on Concurrency Theory - Rome, Italy Duration: 02.09.2014 → 05.09.2014 Conference number: 107236 |
