Abstract
We investigate the satisfiability problem for metric temporal logic (MTL) with both past and future operators over linear discrete bi-infinite time models isomorphic to the integer numbers, where time is unbounded both in the future and in the past. We provide a technique to reduce satisfiability over the integers to satisfiability over the well-known mono-infinite time model of natural numbers, and we show how to implement the technique through an automata-theoretic approach. We also prove that MTL satisfiability over the integers is EXPSPACE-complete, hence the given algorithm is optimal in the worst case.
Work partially supported by the MIUR FIRB ArtDeco project.
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
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Information and Computation 104(1), 35–77 (1993)
Bianculli, D., Morzenti, A., Pradella, M., San Pietro, P., Spoletini, P.: Trio2Promela: A model checker for temporal metric specifications. In: ICSE Companion, pp. 61–62 (2007)
Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: Proceedings of LICS 2007, pp. 109–120. IEEE Computer Society Press, Los Alamitos (2007)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Coen-Porisini, A., Pradella, M., San Pietro, P.: A finite-domain semantics for testing temporal logic specifications. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 41–54. Springer, Heidelberg (1998)
Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Information and Computation 174(1), 84–103 (2002)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 996–1072. Elsevier Science, Amsterdam (1990)
Furia, C.A., Spoletini, P.: MTL satisfiability over the integers. Technical Report 2008.2, DEI, Politecnico di Milano (2008)
Gabbay, D.M., Hodkinson, I., Reynolds, M.: Temporal Logic: mathematical foundations and computational aspects, vol. 1. Oxford University Press, Oxford (1994)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual (2003)
Muller, D.E., Schupp, P.E., Saoudi, A.: On the decidability of the linear Z-temporal logic and the monadic second order theory. In: Proc. of ICCI 1992, pp. 2–5 (1992)
Perrin, D., Pin, J.-É.: Infinite Words. Pure and Applied Mathematics, vol. 141. Elsevier, Amsterdam (2004)
Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future. In: Proceedings of ESEC/FSE 2007, pp. 312–320 (2007)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the ACM 32(3), 733–749 (1985)
Spoletini, P.: Verification of Temporal Logic Specification via Model Checking. PhD thesis, DEI, Politecnico di Milano (May 2005)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–164. Elsevier Science, Amsterdam (1990)
Vardi, M.Y.: Handbook of Modal Logic. In: Automata-Theoretic Techniques for Temporal Reasoning, pp. 971–990 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Furia, C.A., Spoletini, P. (2008). Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)