{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:06Z","timestamp":1776333546316,"version":"3.51.2"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,4,21]],"date-time":"2015-04-21T00:00:00Z","timestamp":1429574400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2016,3]]},"DOI":"10.1007\/s00236-015-0229-y","type":"journal-article","created":{"date-parts":[[2015,4,20]],"date-time":"2015-04-20T12:28:30Z","timestamp":1429532910000},"page":"171-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["A tool for deciding the satisfiability of continuous-time metric temporal logic"],"prefix":"10.1007","volume":"53","author":[{"given":"Marcello M.","family":"Bersani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierluigi","family":"San Pietro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,21]]},"reference":[{"issue":"2","key":"229_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"229_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"},{"key":"229_CR3","doi-asserted-by":"crossref","unstructured":"Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Proceedings of FORTE, pp 243\u2013259 (2002)","DOI":"10.1007\/3-540-36135-9_16"},{"key":"229_CR4","doi-asserted-by":"crossref","unstructured":"Badban, B., Lange, M.: Exact incremental analysis of timed automata with an SMT-solver. In: FORMATS. volume 6919 of LNCS, pp. 177\u2013192 (2011)","DOI":"10.1007\/978-3-642-24310-3_13"},{"key":"229_CR5","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Lecture Notes on Concurrency and Petri Nets. volume 3098 of LNCS, pp. 87\u2013124 (2004)","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"229_CR6","unstructured":"Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., Pietro, P.S.: Constraint LTL satisfiability checking without automata. J. Appl. Logic (2014). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1570868314000615"},{"key":"229_CR7","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: TIME 2010, pp. 43\u201350. IEEE Computer Society, (2010)","DOI":"10.1109\/TIME.2010.21"},{"key":"229_CR8","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Frigeri, A., Rossi, M., San Pietro, P.: Completeness of the bounded satisfiability problem for constraint LTL. In: Reachability Problems, volume 6945 of LNCS, pp. 58\u201371 (2011)","DOI":"10.1007\/978-3-642-24288-5_7"},{"key":"229_CR9","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: Deciding continuous-time metric temporal logic with counting modalities. In: Reachability Problems, volume 8169 of LNCS, pp. 70\u201382 (2013)","DOI":"10.1007\/978-3-642-41036-9_8"},{"key":"229_CR10","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: Deciding the satisfiability of MITL specifications. In: Proceedings of the International Symposium on Games, Automata, Logics and Formal Verification (GandALF), pp. 64\u201378 (2013)","DOI":"10.4204\/EPTCS.119.8"},{"key":"229_CR11","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: On the satisfiability of metric temporal logics over the reals. In: Proceedings of the International Work on Automated Verification of Critical Systems (AVOCS), pp. 1\u201315 (2013)"},{"key":"229_CR12","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: A logical characterization of timed (non-)regular languages. In: Mathematical Foundations of Computer Science, volume 8634 of Lecture Notes in Computer Science, pp. 75\u201386 (2014)","DOI":"10.1007\/978-3-662-44522-8_7"},{"key":"229_CR13","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: An SMT-based approach to satisfiability checking of MITL. Inf. Comput. (2015, to appear)","DOI":"10.1016\/j.ic.2015.06.007"},{"issue":"5","key":"229_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-2(5:5)2006","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1\u201364 (2006)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2","key":"229_CR15","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/j.ic.2009.10.004","volume":"208","author":"P Bouyer","year":"2010","unstructured":"Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97\u2013116 (2010)","journal-title":"Inf. Comput."},{"key":"229_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Verification Model Checking and Abstract Interpretation, volume 2937 of Lecture Notes in Computer Science, pp. 85\u201396. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24622-0_9"},{"issue":"3","key":"229_CR17","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"issue":"1","key":"229_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10009-005-0214-9","volume":"9","author":"D D\u2019Souza","year":"2007","unstructured":"D\u2019Souza, D., Prabhakar, P.: On the expressiveness of mtl in the pointwise and continuous semantics. Int. J. Softw. Tools Technol. Transf. (STTT) 9(1), 1\u20134 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"229_CR19","doi-asserted-by":"crossref","unstructured":"D\u2019Souza, D., Tabareau, N.: On timed automata with input-determined guards. In: FORMATS\/FTRTFT \u201904, volume 3253 of Lecture Notes in Computer Science, pp. 68\u201383 (2004)","DOI":"10.1007\/978-3-540-30206-3_7"},{"issue":"1","key":"229_CR20","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1137\/0204006","volume":"4","author":"J Ferrante","year":"1975","unstructured":"Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69\u201376 (1975)","journal-title":"SIAM J. Comput."},{"key":"229_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: In Proceedings of the 25th International Colloquium Automata, Languages, and Programming (ICALP\u201998), pp. 580\u2013591. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055086"},{"issue":"2","key":"229_CR22","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1016\/j.ic.2004.12.002","volume":"198","author":"Y Hirshfeld","year":"2005","unstructured":"Hirshfeld, Y., Rabinovich, A.: Timer formulas and decidable metric temporal logic. Inf. Comput. 198(2), 148\u2013178 (2005)","journal-title":"Inf. Comput."},{"issue":"1","key":"229_CR23","first-page":"1","volume":"62","author":"Y Hirshfeld","year":"2004","unstructured":"Hirshfeld, Y., Rabinovich, A.M.: Logics for real time: decidability and complexity. Fundam. Inf. 62(1), 1\u201328 (2004)","journal-title":"Fundam. Inf."},{"issue":"1","key":"229_CR24","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0041-5553(80)90061-0","volume":"20","author":"L Khachiyan","year":"1980","unstructured":"Khachiyan, L.: Polynomial algorithms in linear programming. U.S.S.R. Comput. Math. Math. Phys. 20(1), 53\u201372 (1980)","journal-title":"U.S.S.R. Comput. Math. Math. Phys."},{"key":"229_CR25","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Proceedings of FORMATS, volume 4202 of LNCS, pp. 274\u2013289 (2006)","DOI":"10.1007\/11867340_20"},{"key":"229_CR26","unstructured":"Microsoft Research. Z3: An efficient SMT solver. http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/"},{"issue":"2","key":"229_CR27","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"229_CR28","doi-asserted-by":"crossref","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: FTRTFT, volume 2469 of LNCS, pp. 225\u2013243 (2002)","DOI":"10.1007\/3-540-45739-9_15"},{"issue":"3","key":"229_CR29","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12(3), 291\u2013302 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"229_CR30","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: LICS, pp. 188\u2013197 (2005)","DOI":"10.1109\/LICS.2005.33"},{"issue":"3","key":"229_CR31","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/2491509.2491514","volume":"22","author":"M Pradella","year":"2013","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Trans. Softw. Eng. Methodol. (TOSEM) 22(3), 20 (2013)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"229_CR32","unstructured":"qtlsolver. qtlsolver.googlecode.com"},{"key":"229_CR33","doi-asserted-by":"crossref","first-page":"2331","DOI":"10.1016\/j.tcs.2010.03.017","volume":"411","author":"A Rabinovich","year":"2010","unstructured":"Rabinovich, A.: Complexity of metric temporal logics with counting and the Pnueli modalities. Theor. Comput. Sci. 411, 2331\u20132342 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"229_CR34","doi-asserted-by":"crossref","unstructured":"Schobbens, P.-Y., Raskin, J.-F., Henzinger, T.A.: Axioms for real-time logics. Theor. Comput. Sci.274(1\u20132), 151\u2013182 (2002)","DOI":"10.1016\/S0304-3975(00)00308-X"},{"key":"229_CR35","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A decision method for elementary algebra and geometry","author":"A Tarski","year":"1951","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry, 2nd edn. University of California Press, Berkeley (1951)","edition":"2"},{"key":"229_CR36","unstructured":"Zot: a bounded satisfiability checker. zot.googlecode.com"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0229-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0229-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0229-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T14:52:28Z","timestamp":1651762348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0229-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,21]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["229"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0229-y","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,4,21]]}}}