Abstract
Precise complexity results are derived for the model checking problems for \(\mathsf {MTL}\) and \(\mathsf {TPTL}\) on (in)finite data words and deterministic one-counter machines. Depending on the number of register variables and the encoding of constraint numbers (unary or binary), the complexity is P-complete or PSPACE-complete. Proofs can be found in the long version [10].
S. Feng—The author is supported by the German Research Foundation (DFG), GRK 1763.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Alur, R., Henzinger, T.A.: Real-Time Logics: Complexity and Expressiveness. Inf. Comput. 104(1), 35–77 (1993)
Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–204 (1994)
Bouyer, P., Larsen, K.G., Markey. Model checking one-clock priced timed automata. Log. Meth. Comput. Sci. 4(2) (2008)
Bundala, D., Ouaknine, J.: On the complexity of temporal-logic path checking. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 86–97. Springer, Heidelberg (2014)
Carapelle, C., Feng, S., Gil, O.F., Quaas, K.: On the expressiveness of TPTL and MTL over \(\omega \)-data words. In: Proc. AFL 2014. EPTCS, vol. 151, pp. 174–187 (2014)
Carapelle, C., Feng, S., Fernández Gil, O., Quaas, K.: Satisfiability for MTL and TPTL over non-monotonic data words. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 248–259. Springer, Heidelberg (2014)
Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)
Demri, S., Lazić, R., Sangnier, A.: Model checking memoryful linear-time logics over one-counter automata. Theor. Comput. Sci. 411(22–24), 2298–2316 (2010)
Etessami, K., Wilke, T.: An until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic. Inf. Comput. 160(1–2), 88–108 (2000)
Feng, S., Lohrey, M., Quaas, K.: Path-Checking for MTL and TPTL, arXiv.org (2014). 1412.3644
Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallel Computation: P-completeness Theory. Oxford University Press (1995)
Hesse, W., Allender, E., Barrington, D.A.M.: Uniform constant-depth threshold circuits for division and iterated multiplication. J. Comput. System Sci. 65, 695–716 (2002)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)
Kuhtz, L., Finkbeiner, B.: Efficient parallel path checking for linear-time temporal logic with past and bounds. Log. Meth. Comput. Sci. 8(4) (2012)
Laroussinie, F., Markey, N., Schnoebelen, P.: On model checking durational kripke structures. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 264–279. Springer, Heidelberg (2002)
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)
Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Log. Meth. Comput. Sci. 3(1) (2007)
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)
Travers, S.: The complexity of membership problems for circuits over sets of integers. Theor. Comput. Sci. 369(1), 211–229 (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Feng, S., Lohrey, M., Quaas, K. (2015). Path Checking for MTL and TPTL over Data Words. In: Potapov, I. (eds) Developments in Language Theory. DLT 2015. Lecture Notes in Computer Science(), vol 9168. Springer, Cham. https://doi.org/10.1007/978-3-319-21500-6_26
Download citation
DOI: https://doi.org/10.1007/978-3-319-21500-6_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21499-3
Online ISBN: 978-3-319-21500-6
eBook Packages: Computer ScienceComputer Science (R0)