{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:44:23Z","timestamp":1782873863167,"version":"3.54.5"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_33","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:51:02Z","timestamp":1776289862000},"page":"640-659","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2471-5997","authenticated-orcid":false,"given":"S","family":"Akshay","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-7452-9940","authenticated-orcid":false,"given":"Prerak","family":"Contractor","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1313-7722","authenticated-orcid":false,"given":"Paul","family":"Gastin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1634-5893","authenticated-orcid":false,"given":"R","family":"Govind","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2666-0691","authenticated-orcid":false,"given":"B","family":"Srivathsan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"33_CR1","unstructured":"Akshay, S., Contractor, P., Gastin, P., Govind, R., Srivathsan, B.: Efficient verification of metric temporal properties with past in pointwise semantics (2025), https:\/\/arxiv.org\/abs\/2510.14699"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Akshay, S., Gastin, P., Govind, R., Joshi, A.R., Srivathsan, B.: A unified model for real-time systems: Symbolic techniques and implementation. In: CAV (1). Lecture Notes in Computer Science, vol. 13964, pp. 266\u2013288. Springer (2023)","DOI":"10.1007\/978-3-031-37706-8_14"},{"key":"33_CR3","unstructured":"Akshay, S., Gastin, P., Govind, R., Srivathsan, B.: MITL model checking via generalized timed automata and a new liveness algorithm. In: CONCUR. LIPIcs, vol.\u00a0311, pp. 5:1\u20135:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Akshay, S., Gastin, P., Govind, R., Srivathsan, B.: Simulations for event-clock automata. Log. Methods Comput. Sci. 20(3) (2024)","DOI":"10.46298\/lmcs-20(3:2)2024"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: ICALP. LNCS, vol.\u00a0443, pp. 322\u2013335. Springer (1990)","DOI":"10.1007\/BFb0032042"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183\u2013235 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","DOI":"10.1145\/227595.227602"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. In: LICS. pp. 390\u2013401. IEEE Computer Society (1990)","DOI":"10.1109\/LICS.1990.113764"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Artale, A., Geatti, L., Gigante, N., Mazzullo, A., Montanari, A.: Complexity of safety and cosafety fragments of linear temporal logic. In: AAAI. pp. 6236\u20136244. AAAI Press (2023)","DOI":"10.1609\/aaai.v37i5.25768"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: SFM. Lecture Notes in Computer Science, vol.\u00a03185, pp. 200\u2013236. Springer (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.: Acacia+, a tool for LTL synthesis. In: CAV. Lecture Notes in Computer Science, vol.\u00a07358, pp. 652\u2013657. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"33_CR12","unstructured":"Bouyer, P., Haddad, S., Reynier, P.: Timed unfoldings for networks of timed automata. In: ATVA. Lecture Notes in Computer Science, vol.\u00a04218, pp. 292\u2013306. Springer (2006)"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Brihaye, T., Esti\u00e9venart, M., Geeraerts, G.: On MITL and alternating timed automata. In: FORMATS. LNCS, vol.\u00a08053, pp. 47\u201361. Springer (2013)","DOI":"10.1007\/978-3-642-40229-6_4"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Brihaye, T., Esti\u00e9venart, M., Geeraerts, G.: On MITL and alternating timed automata over infinite words. In: FORMATS. LNCS, vol.\u00a08711, pp. 69\u201384. Springer (2014)","DOI":"10.1007\/978-3-319-10512-3_6"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Brihaye, T., Geeraerts, G., Ho, H., Monmege, B.: MightyL: A compositional translation from MITL to timed automata. In: CAV (1). Lecture Notes in Computer Science, vol. 10426, pp. 421\u2013440. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_21"},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Li, G.: Efficient controller synthesis for a fragment of MTL$$_{0, \\infty }$$. Acta Informatica 51(3-4), 165\u2013192 (2014)","DOI":"10.1007\/s00236-013-0189-z"},{"key":"33_CR17","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: CAV. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer (1999)"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Magnago, E., Roveri, M., Tonetta, S.: Extending nuXmv with timed transition systems and timed temporal properties. In: CAV (1). Lecture Notes in Computer Science, vol. 11561, pp. 376\u2013386. Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_21"},{"key":"33_CR19","unstructured":"Cimatti, A., Griggio, A., Magnago, E., Roveri, M., Tonetta, S.: SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. Inf. Comput. 272, 104502 (2020)"},{"key":"33_CR20","doi-asserted-by":"crossref","unstructured":"Couvreur, J.: On-the-fly verification of linear temporal logic. In: World Congress on Formal Methods. Lecture Notes in Computer Science, vol.\u00a01708, pp. 253\u2013271. Springer (1999)","DOI":"10.1007\/3-540-48119-2_16"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 - A framework for LTL and $$\\omega $$-automata manipulation. In: ATVA. LNCS, vol.\u00a09938, pp. 122\u2013129 (2016)","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"33_CR22","doi-asserted-by":"crossref","unstructured":"Ferr\u00e8re, T., Maler, O., Nickovic, D., Pnueli, A.: From real-time logic to timed automata. J. ACM 66(3), 19:1\u201319:31 (2019)","DOI":"10.1145\/3286976"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: CAV. LNCS, vol.\u00a02102, pp. 53\u201365. Springer (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"33_CR24","unstructured":"Govind, R., Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Revisiting local time semantics for networks of timed automata. In: CONCUR. LIPIcs, vol.\u00a0140, pp. 16:1\u201316:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"33_CR25","unstructured":"Herbreteau, F., Point, G., Sankur, O.: TChecker. https:\/\/github.com\/ticktac-project\/tchecker (v08 - September 2023)"},{"key":"33_CR26","unstructured":"Ho, H.M., Krishna, S.N., Madnani, K., Majumdar, R., Pandya, P.: MightyPPL: Verification of MITL with past and pnueli modalities (2025), https:\/\/arxiv.org\/abs\/2510.01490"},{"key":"33_CR27","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997)","DOI":"10.1109\/32.588521"},{"key":"33_CR28","doi-asserted-by":"crossref","unstructured":"Kant, G., Laarman, A., Meijer, J., van\u00a0de Pol, J., Blom, S., van Dijk, T.: LTSmin: High-performance language-independent model checking. In: TACAS. Lecture Notes in Computer Science, vol.\u00a09035, pp. 692\u2013707. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"33_CR29","doi-asserted-by":"crossref","unstructured":"Kindermann, R., Junttila, T.A., Niemel\u00e4, I.: Bounded model checking of an MITL fragment for timed automata. In: ACSD. pp. 216\u2013225. IEEE Computer Society (2013)","DOI":"10.1109\/ACSD.2013.25"},{"key":"33_CR30","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1-2), 134\u2013152 (1997)","DOI":"10.1007\/s100090050010"},{"key":"33_CR31","doi-asserted-by":"crossref","unstructured":"Lee, J., Yu, G., Bae, K.: Efficient SMT-based model checking for signal temporal logic. In: ASE. pp. 343\u2013354. IEEE (2021)","DOI":"10.1109\/ASE51524.2021.9678719"},{"key":"33_CR32","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: Real time temporal logic: Past, present, future. In: FORMATS. Lecture Notes in Computer Science, vol.\u00a03829, pp. 2\u201316. Springer (2005)"},{"key":"33_CR33","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: FORMATS. LNCS, vol.\u00a04202, pp. 274\u2013289. Springer (2006)","DOI":"10.1007\/11867340_20"},{"key":"33_CR34","doi-asserted-by":"publisher","unstructured":"Menghi, C., Bersani, M.M., Rossi, M., San Pietro, P.: Model checking MITL formulae on timed automata: A logic-based approach. ACM Trans. Comput. Log. 21(3), 26:1\u201326:44 (2020). https:\/\/doi.org\/10.1145\/3383687, https:\/\/doi.org\/10.1145\/3383687","DOI":"10.1145\/3383687"},{"key":"33_CR35","doi-asserted-by":"crossref","unstructured":"Nickovic, D., Piterman, N.: From mtl to deterministic timed automata. In: FORMATS. Lecture Notes in Computer Science, vol.\u00a06246, pp. 152\u2013167. Springer (2010)","DOI":"10.1007\/978-3-642-15297-9_13"},{"key":"33_CR36","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On metric temporal logic and faulty turing machines. In: FoSSaCS. LNCS, vol.\u00a03921, pp. 217\u2013230. Springer (2006)","DOI":"10.1007\/11690634_15"},{"key":"33_CR37","doi-asserted-by":"crossref","unstructured":"Plaku, E., Karaman, S.: Motion planning with temporal-logic specifications: Progress and challenges. Artificial Intelligence 232, 1\u201320 (2015)","DOI":"10.3233\/AIC-150682"},{"key":"33_CR38","unstructured":"Pradella, M.: A user\u2019s guide to Zot. CoRR abs\/0912.5014 (2009)"},{"key":"33_CR39","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Tonetta, S.: \u201cMore Deterministic\u201d vs. \u201cSmaller\u201d b\u00fcchi automata for efficient LTL model checking. In: Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2003). pp. 126\u2013140 (2003)","DOI":"10.1007\/978-3-540-39724-3_12"},{"key":"33_CR40","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards flexible verification under fairness. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"33_CR41","doi-asserted-by":"crossref","unstructured":"Tsay, Y.K., Vardi, M.Y.: From linear temporal logics to b\u00fcchi automata: The early and simple principle. In: Proceedings of the 2021 International Conference on Model Checking Software (SPIN 2021). pp. 8\u201340 (2021)","DOI":"10.1007\/978-3-030-91384-7_2"},{"key":"33_CR42","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. LNCS 1043, 238\u2013266 (1996)","DOI":"10.1007\/3-540-60915-6_6"},{"key":"33_CR43","doi-asserted-by":"crossref","unstructured":"Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: FTRTFT. LNCS, vol.\u00a0863, pp. 694\u2013715. Springer (1994)","DOI":"10.1007\/3-540-58468-4_191"},{"key":"33_CR44","doi-asserted-by":"crossref","unstructured":"Zhou, Y., Maity, D., Baras, J.S.: Timed automata approach for motion planning using metric interval temporal logic. In: ECC. pp. 690\u2013695. IEEE (2016)","DOI":"10.1109\/ECC.2016.7810369"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22752-2_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T01:56:00Z","timestamp":1782870960000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"16 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}