Satisfiability for MTL and TPTL over Non-monotonic Data Words

  • Claudia Carapelle
  • Shiguang Feng
  • Oliver Fernández Gil
  • Karin Quaas
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8370)


In the context of real-time systems, Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent and widely used extensions of Linear Temporal Logic. In this paper, we examine the possibility of using MTL and TPTL to specify properties about classes of non-monotonic data languages over the natural numbers. Words in this class may model the behaviour of, e.g., one-counter machines. We proved, however, that the satisfiability problem for many reasonably expressive fragments of MTL and TPTL is undecidable, and thus the use of these logics is rather limited. On the positive side we prove that satisfiability for the existential fragment of TPTL is NP-complete.


Model Check Temporal Logic Linear Temporal Logic Propositional Variable Data Word 
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.
    Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–204 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    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
  4. 4.
    Bollig, B.: An automaton over data words that captures EMSO logic. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 171–186. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  5. 5.
    Bollig, B., Cyriac, A., Gastin, P., Narayan Kumar, K.: Model checking languages of data words. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 391–405. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  6. 6.
    Bouyer, P.: A logical characterization of data languages. Inf. Process. Lett. 84(2), 75–85 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97–116 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Carapelle, C., Feng, S., Fernandez Gil, O., Quaas, K.: Ehrenfeucht-Fraïssé games for TPTL and MTL over data words,
  9. 9.
    Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, Second Edition, 2nd edn. The MIT Press and McGraw-Hill Book Company (2001)Google Scholar
  10. 10.
    Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)Google Scholar
  11. 11.
    Demri, S., Lazić, R.S., Sangnier, A.: Model checking Freeze LTL over one-counter automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 490–504. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. 12.
    Figueira, D., Segoufin, L.: Future-looking logics on data words and trees. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 331–343. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  13. 13.
    Jaffar, J., Maher, M.J., Stuckey, P.J., Yap, R.H.C.: Beyond finite domains. In: Borning, A. (ed.) PPCP 1994. LNCS, vol. 874, pp. 86–94. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  14. 14.
    Minsky, M.L.: Recursive unsolvability of Post’s problem of “tag” and other topics in theory of Turing machines. Annals of Mathematics 74(3), 437–455 (1961)CrossRefzbMATHMathSciNetGoogle Scholar
  15. 15.
    Ouaknine, J., Worrell, J.B.: On metric temporal logic and faulty Turing machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 217–230. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Logical Methods in Computer Science 3(1) (2007)Google Scholar
  17. 17.
    Quaas, K.: Model checking metric temporal logic over automata with one counter. In: Dediu, A.-H., Martín-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 468–479. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  18. 18.
    Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41–57. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Claudia Carapelle
    • 1
  • Shiguang Feng
    • 1
  • Oliver Fernández Gil
    • 1
  • Karin Quaas
    • 1
  1. 1.Institut für InformatikUniversität LeipzigLeipzigGermany

Personalised recommendations