Ordered Navigation on Multi-attributed Data Words

Normann Decker; Peter Habermehl; Martin Leucker; Daniel Thoma

doi:10.1007/978-3-662-44584-6_34

Ordered Navigation on Multi-attributed Data Words

Normann Decker, Peter Habermehl, Martin Leucker, Daniel Thoma

Institute of Software Engineering and Programming Languages

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	https://doi.org/10.1007/978-3-662-44584-6_34
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

Access to Document

10.1007/978-3-662-44584-6_34

Cite this

@inproceedings{9517e2256f70472b9b08dee9bbf5f467,

title = "Ordered Navigation on Multi-attributed Data Words",

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.",

author = "Normann Decker and Peter Habermehl and Martin Leucker and Daniel Thoma",

year = "2014",

month = sep,

day = "1",

doi = "10.1007/978-3-662-44584-6_34",

language = "English",

isbn = "978-3-662-44583-9",

volume = "LNCS 8704",

series = "Lecture Notes in Computer Science ",

publisher = "Springer Verlag",

pages = "497--511",

editor = "Baldan, {Paolo } and Gorla, {Daniele }",

booktitle = "CONCUR 2014 – Concurrency Theory",

note = "25th International Conference on Concurrency Theory <br/>, CONCUR 2014 ; Conference date: 02-09-2014 Through 05-09-2014",

}

Decker, N, Habermehl, P, Leucker, M & Thoma, D 2014, Ordered Navigation on Multi-attributed Data Words. in P Baldan & D Gorla (eds), CONCUR 2014 – Concurrency Theory. vol. LNCS 8704, Lecture Notes in Computer Science , vol. LNCS 8704, Springer Verlag, Berlin, pp. 497-511, 25th International Conference on Concurrency Theory
, Rome, Italy, 02.09.14. https://doi.org/10.1007/978-3-662-44584-6_34

Ordered Navigation on Multi-attributed Data Words. / Decker, Normann; Habermehl, Peter; Leucker, Martin et al.

CONCUR 2014 – Concurrency Theory. ed. / Paolo Baldan; Daniele Gorla. Vol. LNCS 8704 Berlin : Springer Verlag, 2014. p. 497-511 (Lecture Notes in Computer Science ; Vol. LNCS 8704).

Research output: Chapters in Books/Reports/Conference Proceedings › Conference contribution › peer-review

TY - GEN

T1 - Ordered Navigation on Multi-attributed Data Words

AU - Decker, Normann

AU - Habermehl, Peter

AU - Leucker, Martin

AU - Thoma, Daniel

N1 - Conference code: 107236

PY - 2014/9/1

Y1 - 2014/9/1

N2 - 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.

AB - 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.

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-84906766157&origin=inward&txGid=719c258fbb53079b713c2723da601bb8

U2 - 10.1007/978-3-662-44584-6_34

DO - 10.1007/978-3-662-44584-6_34

M3 - Conference contribution

SN - 978-3-662-44583-9

VL - LNCS 8704

T3 - Lecture Notes in Computer Science

SP - 497

EP - 511

BT - CONCUR 2014 – Concurrency Theory

A2 - Baldan, Paolo

A2 - Gorla, Daniele

PB - Springer Verlag

CY - Berlin

T2 - 25th International Conference on Concurrency Theory <br/>

Y2 - 2 September 2014 through 5 September 2014

ER -

Ordered Navigation on Multi-attributed Data Words

Abstract

Access to Document

Other files and links

Fingerprint

Cite this