Abstract
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non-punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non-punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non-punctuality called non-adjacency for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non-adjacent 1-TPTL[U,S] appears to be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non-adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity.
This work is partially supported by the European Research Council through the SENTIENT project (ERC-2017-STG #755953).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Here T is a special symbol denoting the timestamp of the present point and x is the clock that was frozen when x. was asserted.
- 2.
We \(\mathsf {A}'_k\) instead of \(\mathsf {A}_k\) in the formulae below due to the strict inequalities in the semantics of \(\mathsf {PnEMTL}\) modalities.
- 3.
Unbounded intervals can be eliminated using \(\mathcal {F}^{k}_{\mathsf {I_1, I_2, \ldots , I_{k{-}2},} [l_1, \infty ) [l_2, \infty )}(\mathsf {A}_1, \ldots , \mathsf {A}_{k+1}) {\equiv }\) \(\mathcal {F}^{k}_{\mathsf {I_1, I_2, \ldots , I_{k{-}2},} [l_1, \mathsf {cmax}) [l_2, \infty )}(\mathsf {A}_1, \ldots , \mathsf {A}_{k+1}) {\vee } \mathcal {F}^{k-1}_{\mathsf {I_1, I_2, \ldots , I_{k{-}2},} [l_2, \infty )}(\mathsf {A}_1, \ldots , \mathsf {A}_{k-1},\mathsf {A}_{k} \cdot \mathsf {A}_{k+1})\).
References
Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)
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–203 (1994)
Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 432–443. Springer, Heidelberg (2005). https://doi.org/10.1007/11590156_35
Ferrère, T.: The compound interest in relaxing punctuality. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 147–164. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95582-7_9
Gastin, P., Oddoux, D.: LTL with past and two-way very-weak alternating automata. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 439–448. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45138-9_38
Haase, C., Ouaknine, J., Worrell, J.: On process-algebraic extensions of metric temporal logic. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, pp. 283–300. Springer, London (2010). https://doi.org/10.1007/978-1-84882-912-1_13
Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 580–591. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055086
Hirshfeld, Y., Rabinovich, A.: An expressive temporal logic for real time. In: Královič, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 492–504. Springer, Heidelberg (2006). https://doi.org/10.1007/11821069_43
Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 211–220. Springer, Heidelberg (2006). https://doi.org/10.1007/11753728_23
Ho, H.-M.: Revisiting timed logics with automata modalities. In: Ozay, N., Prabhakar, P. (eds.) Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, 16–18 April 2019, pp. 67–76. ACM (2019)
Madnani, K., Krishna, S.N., Pandya, P.K.: Partially punctual metric temporal logic is decidable. In: TIME, pp. 174–183 (2014)
Krishna, S.N., Madnani, K., Mazo Jr., M., Pandya, P.K.: Generalizing non-punctuality for timed temporal logic with freeze quantifiers. CoRR, abs/2105.09534 (2021)
Krishna, S.N., Madnani, K., Pandya, P.K.: Making metric temporal logic rational. In: Larsen, K.G., Bodlaender, H.L., Raskin, J.-F. (eds.) 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, 21–25 August 2017 - Aalborg, Denmark. LIPIcs, vol. 83, pp. 77:1–77:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
Krishna, S.N., Madnani, K., Pandya, P.K.: Logics meet 1-clock alternating timed automata. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, 4–7 September 2018, Beijing, China. LIPIcs, vol. 118, pp. 39:1–39:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
Madnani, K.N.: On decidable extensions of metric temporal logic. Ph.D. thesis, Indian Institute of Technology Bombay, Mumbai, India (2019)
Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: LICS, pp. 188–197 (2005)
Pandya, P.K., Shah, S.S.: On expressive powers of timed logics: comparing boundedness, non-punctuality, and deterministic freezing. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 60–75. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23217-6_5
Prabhakar, P., D’Souza, D.: On the expressiveness of MTL with past operators. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 322–336. Springer, Heidelberg (2006). https://doi.org/10.1007/11867340_23
Rabinovich, A.: Complexity of metric temporal logic with counting and pnueli modalities. In: FORMATS, pp. 93–108 (2008)
Rabinovich, A.: Complexity of metric temporal logics with counting and the pnueli modalities. Theor. Comput. Sci. 411(22–24), 2331–2342 (2010)
Raskin, J.F.: Logics, automata and classical theories for deciding real time. Ph.D. thesis, Universite de Namur (1999)
Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Lübeck, Germany, 19–23 September, Proceedings, pp. 694–715 (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Krishna, S.N., Madnani, K., Mazo, M., Pandya, P.K. (2021). Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science(), vol 13047. Springer, Cham. https://doi.org/10.1007/978-3-030-90870-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-90870-6_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-90869-0
Online ISBN: 978-3-030-90870-6
eBook Packages: Computer ScienceComputer Science (R0)