Abstract
We study two unary fragments of the well-known metric interval temporal logic \(\mathit{MITL[\textsf{U}_I,\textsf{S}_I]}\) that was originally proposed by Alur and Henzinger, and we pin down their expressiveness as well as satisfaction complexities. We show that \(\mbox{$\mathit{MITL[\textsf{F}_\infty,\textsf{P}_\infty]}$}\) which has unary modalities with only lower-bound constraints is (surprisingly) expressively complete for Partially Ordered 2-Way Deterministic Timed Automata (po2DTA) and the reduction from logic to automaton gives us its NP-complete satisfiability. We also show that the fragment \(\mbox{$\mathit{MITL[\textsf{F}_b,\textsf{P}_b]}$}\) having unary modalities with only bounded intervals has NEXPTIME-complete satisfiability. But strangely, \(\mathit{MITL[\textsf{F}_b,\textsf{P}_b]}\) is strictly less expressive than \(\mathit{MITL[\textsf{F}_\infty,\textsf{P}_\infty]}\). We provide a comprehensive picture of the decidability and expressiveness of various unary fragments of MITL.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.A.: Back to the future: Towards a theory of timed regular languages. In: FOCS, pp. 177–186 (1992)
Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993)
Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.B.: On Expressiveness and Complexity in Real-Time Model Checking. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 124–135. Springer, Heidelberg (2008)
Van Emde Boas, P.: The convenience of tilings. In: Complexity, Logic, and Recursion Theory, pp. 331–363. Marcel Dekker Inc. (1997)
Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)
Fürer, M.: The Computational Complexity of the Unconstrained Limited Domino Problem (with Implications for Logical Decision Problems). In: Börger, E., Rödding, D., Hasenjaeger, G. (eds.) Rekursive Kombinatorik 1983. LNCS, vol. 171, pp. 312–319. Springer, Heidelberg (1984)
Henzinger, T.A.: The Temporal Specification and Verification of Real-Time Systems. PhD thesis, Stanford University (1991)
Pandya, P.K., Shah, S.S.: Unambiguity in Timed Regular Languages: Automata and Logics. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 168–182. Springer, Heidelberg (2010)
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)
Schwentick, T., Thérien, D., Vollmer, H.: Partially-ordered two-way automata: A new characterization of DA. In: Kuich, W., Rozenberg, G., Salomaa, A. (eds.) DLT 2001. LNCS, vol. 2295, pp. 239–250. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pandya, P.K., Shah, S.S. (2012). The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower Bound Constraints. In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-33386-6_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33385-9
Online ISBN: 978-3-642-33386-6
eBook Packages: Computer ScienceComputer Science (R0)