Ordered Navigation on Multi-attributed Data Words

We consider temporal logics on multi-attributed data words which are words where each position additionally carries multiple data values. 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 satisfiability problem of the logic undecidable, we introduce ND-LTL, an extension of BD-LTL by a restricted form of tuple-navigation. We impose a tree order on the attributes that has to be respected during navigation. Tree orders can model naturally occurring dependency relations in object oriented or parallel systems. While complete ND-LTL is still undecidable, the two natural fragments allowing for either future or past navigation along data values are Ackermann-hard, yet decidable. 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.

Authors

• Normann Decker

Keywords

No keywords are indexed for this paper.