{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:38Z","timestamp":1760202578666},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540857617"},{"type":"electronic","value":"9783540857624"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85762-4_9","type":"book-chapter","created":{"date-parts":[[2008,8,22]],"date-time":"2008-08-22T14:20:29Z","timestamp":1219414829000},"page":"126-140","source":"Crossref","is-referenced-by-count":9,"title":["Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers"],"prefix":"10.1007","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paola","family":"Spoletini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Information and Computation\u00a0104(1), 35\u201377 (1993)","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"Bianculli, D., Morzenti, A., Pradella, M., San Pietro, P., Spoletini, P.: Trio2Promela: A model checker for temporal metric specifications. In: ICSE Companion, pp. 61\u201362 (2007)","key":"9_CR2","DOI":"10.1109\/ICSECOMPANION.2007.79"},{"key":"9_CR3","first-page":"109","volume-title":"Proceedings of LICS 2007","author":"P. Bouyer","year":"2007","unstructured":"Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: Proceedings of LICS 2007, pp. 109\u2013120. IEEE Computer Society Press, Los Alamitos (2007)"},{"key":"9_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BFb0055335","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A. Coen-Porisini","year":"1998","unstructured":"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.\u00a01486, pp. 41\u201354. Springer, Heidelberg (1998)"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.2001.3094","volume":"174","author":"S. Demri","year":"2002","unstructured":"Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Information and Computation\u00a0174(1), 84\u2013103 (2002)","journal-title":"Information and Computation"},{"key":"9_CR7","first-page":"996","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 996\u20131072. Elsevier Science, Amsterdam (1990)"},{"unstructured":"Furia, C.A., Spoletini, P.: MTL satisfiability over the integers. Technical Report 2008.2, DEI, Politecnico di Milano (2008)","key":"9_CR8"},{"key":"9_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0013976","volume-title":"Temporal Logic : mathematical foundations and computational aspects","author":"D.M. Gabbay","year":"1994","unstructured":"Gabbay, D.M., Hodkinson, I., Reynolds, M.: Temporal Logic: mathematical foundations and computational aspects, vol.\u00a01. Oxford University Press, Oxford (1994)"},{"unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual (2003)","key":"9_CR10"},{"doi-asserted-by":"crossref","unstructured":"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\u20135 (1992)","key":"9_CR11","DOI":"10.1109\/ICCI.1992.227719"},{"key":"9_CR12","series-title":"Pure and Applied Mathematics","volume-title":"Infinite Words","author":"D. Perrin","year":"2004","unstructured":"Perrin, D., Pin, J.-\u00c9.: Infinite Words. Pure and Applied Mathematics, vol.\u00a0141. Elsevier, Amsterdam (2004)"},{"doi-asserted-by":"crossref","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future. In: Proceedings of ESEC\/FSE 2007, pp. 312\u2013320 (2007)","key":"9_CR13","DOI":"10.1145\/1287624.1287669"},{"issue":"3","key":"9_CR14","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"Journal of the ACM"},{"unstructured":"Spoletini, P.: Verification of Temporal Logic Specification via Model Checking. PhD thesis, DEI, Politecnico di Milano (May 2005)","key":"9_CR15"},{"key":"9_CR16","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 133\u2013164. Elsevier Science, Amsterdam (1990)"},{"doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Handbook of Modal Logic. In: Automata-Theoretic Techniques for Temporal Reasoning, pp. 971\u2013990 (2006)","key":"9_CR17","DOI":"10.1016\/S1570-2464(07)80020-6"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85762-4_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:34:29Z","timestamp":1606185269000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85762-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540857617","9783540857624"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85762-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}