Satisfiability for MTL and TPTL over Non-monotonic Data Words

1. Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993)

   Article  MATH  MathSciNet  Google Scholar 

2. Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–204 (1994)

   Article  MATH  MathSciNet  Google Scholar 

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)

   Article  MathSciNet  Google Scholar 

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)

   Chapter  Google Scholar 

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)

   Chapter  Google Scholar 

6. Bouyer, P.: A logical characterization of data languages. Inf. Process. Lett. 84(2), 75–85 (2002)

   Article  MATH  MathSciNet  Google Scholar 

7. Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97–116 (2010)

   Article  MATH  MathSciNet  Google Scholar 

8. Carapelle, C., Feng, S., Fernandez Gil, O., Quaas, K.: Ehrenfeucht-Fraïssé games for TPTL and MTL over data words, http://arxiv.org/abs/1311.6250

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. Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)

    Google Scholar 

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)

    Chapter  Google Scholar 

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)

    Chapter  Google Scholar 

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)

    Chapter  Google Scholar 

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)

    Article  MATH  MathSciNet  Google Scholar 

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)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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)

    Chapter  Google Scholar 

Download references