Ordered Navigation on Multi-attributed Data Words

  • Normann Decker
  • Peter Habermehl
  • Martin Leucker
  • Daniel Thoma
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


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.


Temporal Logic Transition Relation Atomic Proposition Class String Reachability Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bulletin of Symbolic Logic 16(4), 457–515 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Björklund, H., Bojańczyk, M.: Shuffle expressions and words with nested data. In: Kučera, L., Kučera, A. (eds.) MFCS 2007. LNCS, vol. 4708, pp. 750–761. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Björklund, H., Schwentick, T.: On notions of regularity for data languages. Theor. Comput. Sci. 411(4-5), 702–715 (2010)CrossRefzbMATHGoogle Scholar
  4. 4.
    Bojanczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4), 27 (2011)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 323–333. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Bouyer, P., Petit, A., Thérien, D.: An algebraic approach to data languages and timed languages. Inf. Comput. 182(2), 137–162 (2003)CrossRefzbMATHGoogle Scholar
  7. 7.
    Demri, S., D’Souza, D., Gascon, R.: Temporal logics of repeating values. J. Log. Comput. 22(5), 1059–1096 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Demri, S., Figueira, D., Praveen, M.: Reasoning about data repetitions with counter systems. In: LICS, pp. 33–42. IEEE Computer Society (2013)Google Scholar
  9. 9.
    Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)Google Scholar
  10. 10.
    Demri, S., Lazic, R., Nowak, D.: On the freeze quantifier in constraint LTL: Decidability and complexity. Inf. Comput. 205(1), 2–24 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Habermehl, P.: On the complexity of the linear-time μ-calculus for Petri nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 102–116. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  13. 13.
    Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Kara, A., Schwentick, T., Zeume, T.: Temporal logics on words with multiple data values. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS. LIPIcs, vol. 8, pp. 481–492 (2010)Google Scholar
  15. 15.
    Kara, A., Schwentick, T., Zeume, T.: Temporal logics on words with multiple data values. CoRR abs/1010.1139 (2010)Google Scholar
  16. 16.
    Leroux, J.: Vector addition system reachability problem: A short self-contained proof. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 307–316. ACM (2011)Google Scholar
  17. 17.
    Lomazova, I.A., Schnoebelen, P.: Some decidability results for nested Petri nets. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol. 1755, pp. 208–220. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  18. 18.
    Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403–435 (2004)CrossRefMathSciNetGoogle Scholar
  19. 19.
    Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978)CrossRefzbMATHMathSciNetGoogle Scholar
  20. 20.
    Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  21. 21.
    Schwentick, T., Zeume, T.: Two-variable logic with two order relations. Logical Methods in Computer Science 8(1) (2012)Google Scholar
  22. 22.
    Tzevelekos, N., Grigore, R.: History-register automata. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 17–33. Springer, Heidelberg (2013)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Normann Decker
    • 1
  • Peter Habermehl
    • 2
  • Martin Leucker
    • 1
  • Daniel Thoma
    • 1
  1. 1.ISPUniversity of LübeckGermany
  2. 2.Univ Paris Diderot, Sorbonne Paris Cité, LIAFA, CNRSFrance

Personalised recommendations