{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:31Z","timestamp":1760202751124},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_20","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:34:07Z","timestamp":1499679247000},"page":"326-343","source":"Crossref","is-referenced-by-count":5,"title":["Theorem Proving for Metric Temporal Logic over the Naturals"],"prefix":"10.1007","author":[{"given":"Ullrich","family":"Hustadt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Ozaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"2s","key":"20_CR1","first-page":"95: 1","volume":"12","author":"H Abbas","year":"2013","unstructured":"Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. (TECS) 12(2s), 95: 1\u201395: 30 (2013)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"issue":"1","key":"20_CR2","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"issue":"1","key":"20_CR3","doi-asserted-by":"crossref","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. Inf. Comput. 104(1), 35\u201377 (1993)","journal-title":"Inf. Comput."},{"issue":"1","key":"20_CR4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181\u2013204 (1994)","journal-title":"J. ACM"},{"issue":"2","key":"20_CR5","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/s00236-015-0229-y","volume":"53","author":"MM Bersani","year":"2016","unstructured":"Bersani, M.M., Rossi, M., Pietro, P.S.: A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Informatica 53(2), 171\u2013206 (2016)","journal-title":"Acta Informatica"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: Proceedings of LICS 2007, pp. 109\u2013120. IEEE (2007)","DOI":"10.1109\/LICS.2007.49"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45657-0_29"},{"key":"20_CR8","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1023\/A:1018930406487","volume":"70","author":"S Dauz\u00e8re-P\u00e9r\u00e8s","year":"1997","unstructured":"Dauz\u00e8re-P\u00e9r\u00e8s, S., Paulli, J.: An integrated approach for modeling and solving the general multiprocessor job-shop scheduling problem using tabu search. Ann. Oper. Res. 70, 281\u2013306 (1997)","journal-title":"Ann. Oper. Res."},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-540-74621-8_11","volume-title":"Frontiers of Combining Systems","author":"C Dixon","year":"2007","unstructured":"Dixon, C., Fisher, M., Konev, B.: Temporal logic with capacity constraints. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS, vol. 4720, pp. 163\u2013177. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74621-8_11"},{"issue":"4","key":"20_CR10","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","volume":"7","author":"M Fisher","year":"1997","unstructured":"Fisher, M.: A normal form for temporal logics and its applications in theorem-proving and execution. J. Logic Comput. 7(4), 429\u2013456 (1997)","journal-title":"J. Logic Comput."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of POPL 1980, pp. 163\u2013173. ACM (1980)","DOI":"10.1145\/567446.567462"},{"issue":"5\u2014-6","key":"20_CR12","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1016\/j.artint.2008.10.012","volume":"173","author":"A Gerevini","year":"2009","unstructured":"Gerevini, A., Haslum, P., Long, D., Saetti, A., Dimopoulos, Y.: Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners. Artif. Intell. 173(5\u2014-6), 619\u2013668 (2009)","journal-title":"Artif. Intell."},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-319-08587-6_3","volume-title":"Automated Reasoning","author":"R Gor\u00e9","year":"2014","unstructured":"Gor\u00e9, R.: And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 26\u201345. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08587-6_3"},{"issue":"9","key":"20_CR14","doi-asserted-by":"crossref","first-page":"1563","DOI":"10.1002\/j.1538-7305.1966.tb01709.x","volume":"45","author":"RL Graham","year":"1966","unstructured":"Graham, R.L.: Bounds for certain multiprocessing anomalies. Bell Labs Tech. J. 45(9), 1563\u20131581 (1966)","journal-title":"Bell Labs Tech. J."},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-319-06410-9_21","volume-title":"FM 2014: Formal Methods","author":"H Gunadi","year":"2014","unstructured":"Gunadi, H., Tiu, A.: Efficient runtime monitoring with metric temporal logic: a case study in the android operating system. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 296\u2013311. Springer, Cham (2014). doi:\n10.1007\/978-3-319-06410-9_21"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-45085-6_21","volume-title":"Automated Deduction \u2013 CADE-19","author":"U Hustadt","year":"2003","unstructured":"Hustadt, U., Konev, B.: TRP++ 2.0: a temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS, vol. 2741, pp. 274\u2013278. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-45085-6_21"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Karaman, S., Frazzoli, E.: Vehicle routing problem with metric temporal logic specifications. In: Proceedings of CDC 2008, pp. 3953\u20133958. IEEE (2008)","DOI":"10.1109\/CDC.2008.4739366"},{"key":"20_CR18","unstructured":"LS4. \nhttps:\/\/github.com\/quickbeam123\/ls4"},{"key":"20_CR19","unstructured":"NuSMV. \nhttp:\/\/nusmv.fbk.eu\/"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1\u201313. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-85778-5_1"},{"key":"20_CR21","unstructured":"pltl. \nhttp:\/\/users.cecs.anu.edu.au\/rpg\/PLTLProvers\/"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of SFCS 1977, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-24372-1_28","volume-title":"Automated Technology for Verification and Analysis","author":"V Schuppan","year":"2011","unstructured":"Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 397\u2013413. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-24372-1_28"},{"issue":"3","key":"20_CR24","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-642-31365-3_42","volume-title":"Automated Reasoning","author":"M Suda","year":"2012","unstructured":"Suda, M., Weidenbach, C.: A PLTL-prover based on labelled superposition with partial model guidance. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 537\u2013543. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-31365-3_42"},{"key":"20_CR26","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/j.entcs.2004.01.029","volume":"113","author":"P Thati","year":"2005","unstructured":"Thati, P., Ro\u015fu, G.: Monitoring algorithms for metric temporal logic specifications. Electronic Notes Theoret. Comput. Sci. 113, 145\u2013162 (2005)","journal-title":"Electronic Notes Theoret. Comput. Sci."},{"key":"20_CR27","unstructured":"TRP++. \nhttp:\/\/cgi.csc.liv.ac.uk\/konev\/software\/trp++\/"},{"key":"20_CR28","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., et al. (eds.) Automation of Reasoning, pp. 466\u2013483. Springer, Heidelberg (1983)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:39:23Z","timestamp":1499679563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}