{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T18:50:05Z","timestamp":1784919005422,"version":"3.55.0"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T00:00:00Z","timestamp":1558569600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Z211-N23, S11402-N23"],"award-info":[{"award-number":["Z211-N23, S11402-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2019,6,30]]},"abstract":"<jats:p>We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a \u201csimple\u201d formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.<\/jats:p>","DOI":"10.1145\/3286976","type":"journal-article","created":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T16:04:16Z","timestamp":1558713856000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["From Real-time Logic to Timed Automata"],"prefix":"10.1145","volume":"66","author":[{"given":"Thomas","family":"Ferr\u00e8re","sequence":"first","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[{"name":"CNRS-Verimag, University of Grenoble-Alpes"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5468-0396","authenticated-orcid":false,"given":"Dejan","family":"Ni\u010dkovi\u0107","sequence":"additional","affiliation":[{"name":"AIT Austrian Institute of Technology, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[{"name":"Weizmann Institute of Science and New York University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,5,23]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2010. IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005). IEEE Standard for Property Specification Language (PSL).  2010. IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005). IEEE Standard for Property Specification Language (PSL)."},{"key":"e_1_2_1_2_1","first-page":"1800","year":"2012","unstructured":"2012 . ANSI\/IEEE 1800 - 2012 . IEEE Standard for SystemVerilog. Unified Hardware Design, Specification, and Verification Language. 2012. ANSI\/IEEE 1800-2012. IEEE Standard for SystemVerilog. Unified Hardware Design, Specification, and Verification Language.","journal-title":"ANSI\/IEEE"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733787"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1992.267774"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/648143.749966"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_9_1","first-page":"106","article-title":"Challenges in timed languages: From applied theory to basic theory","volume":"83","author":"Asarin Eugene","year":"2004","unstructured":"Eugene Asarin . 2004 . Challenges in timed languages: From applied theory to basic theory . Bull. Eur. Assoc. Theor. Comput. Sci. 83 (2004), 106 -- 120 . Eugene Asarin. 2004. Challenges in timed languages: From applied theory to basic theory. Bull. Eur. Assoc. Theor. Comput. Sci. 83 (2004), 106--120.","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/506147.506151"},{"key":"e_1_2_1_11_1","volume-title":"Balanced timed regular expressions1. Electr. Not. Theor. Comput. Sci. 68, 5","author":"Asarin Eugene","year":"2003","unstructured":"Eugene Asarin and C\u0103t\u0103lin Dima . 2003. Balanced timed regular expressions1. Electr. Not. Theor. Comput. Sci. 68, 5 ( 2003 ). Eugene Asarin and C\u0103t\u0103lin Dima. 2003. Balanced timed regular expressions1. Electr. Not. Theor. Comput. Sci. 68, 5 (2003)."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1373322"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_6"},{"key":"e_1_2_1_14_1","volume-title":"Systems and Software Verification: Model-checking Techniques and Tools","author":"B\u00e9rard B\u00e9atrice","unstructured":"B\u00e9atrice B\u00e9rard , Michel Bidoit , Alain Finkel , Fran\u00e7ois Laroussinie , Antoine Petit , Laure Petrucci , and Philippe Schnoebelen . 2013. Systems and Software Verification: Model-checking Techniques and Tools . Springer Science 8 Business Media. B\u00e9atrice B\u00e9rard, Michel Bidoit, Alain Finkel, Fran\u00e7ois Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. 2013. Systems and Software Verification: Model-checking Techniques and Tools. Springer Science 8 Business Media."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.06.007"},{"key":"e_1_2_1_16_1","first-page":"1001","article-title":"Model checking real-time systems. In Clarke et\u00a0al. {28}","volume":"29","author":"Bouyer Patricia","year":"2018","unstructured":"Patricia Bouyer , Uli Fahrenberg , Kim G. Larsen , Nicolas Markey , Jo\u00ebl Ouaknine , and James Worrell . 2018 . Model checking real-time systems. In Clarke et\u00a0al. {28} , Chapter 29 , 1001 -- 1046 . Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, Jo\u00ebl Ouaknine, and James Worrell. 2018. Model checking real-time systems. In Clarke et\u00a0al. {28}, Chapter 29, 1001--1046.","journal-title":"Chapter"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40229-6_4"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40229-6_4"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 24th International Symposium on Temporal Representation and Reasoning (TIME\u201917)","author":"Brihaye Thomas","year":"2017","unstructured":"Thomas Brihaye , Gilles Geeraerts , Hsi-Ming Ho , and Benjamin Monmege . 2017 . Timed-automata-based verification of MITL over signals . In Proceedings of the 24th International Symposium on Temporal Representation and Reasoning (TIME\u201917) . 7:1--7:19. Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. 2017. Timed-automata-based verification of MITL over signals. In Proceedings of the 24th International Symposium on Temporal Representation and Reasoning (TIME\u201917). 7:1--7:19."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Thomas Brihaye Gilles Geeraerts Hsi-Ming Ho and Benjamin Monmege. 2017. MightyL: A compositional translation from MITL to timed automata. In Computer Aided Verification. 421--440.  Thomas Brihaye Gilles Geeraerts Hsi-Ming Ho and Benjamin Monmege. 2017. MightyL: A compositional translation from MITL to timed automata. In Computer Aided Verification. 421--440.","DOI":"10.1007\/978-3-319-63387-9_21"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90069-9"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1976.4"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.19"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647763.735667"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/332656"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/3264692"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Deepak D\u2019Souza and R. Matteplackel. 2013. A Clock-optimal Hierarchical Monitoring Automaton Construction for MITL. Technical Report.  Deepak D\u2019Souza and R. Matteplackel. 2013. A Clock-optimal Hierarchical Monitoring Automaton Construction for MITL. Technical Report.","DOI":"10.1007\/978-3-642-32943-2_2"},{"key":"e_1_2_1_30_1","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"D\u2019Souza Deepak","unstructured":"Deepak D\u2019Souza and Nicolas Tabareau . 2004. On timed automata with input-determined guards . In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems . Springer , 68--83. Deepak D\u2019Souza and Nicolas Tabareau. 2004. On timed automata with input-determined guards. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 68--83."},{"key":"e_1_2_1_31_1","volume-title":"Functional specification of hardware via temporal logic. Handbook of Model Checking","author":"Eisner Cindy","year":"2018","unstructured":"Cindy Eisner and Dana Fisman . 2018. Functional specification of hardware via temporal logic. Handbook of Model Checking ( 2018 ), 795--829. Cindy Eisner and Dana Fisman. 2018. Functional specification of hardware via temporal logic. Handbook of Model Checking (2018), 795--829."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_20"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/647770.734262"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/645837.670574"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/646220.682186"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701319"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/646252.686189"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647849.737075"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370629.2370631"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/1085478.1709506"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/11821069_43"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11753728_23"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/975331"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.023"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/646252.756784"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.25"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/2044973.2044994"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/800221.806721"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0065-1"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/11603009_2"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/11867340_20"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/1805839.1805865"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_25"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/648140.749663"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_2_1_60_1","first-page":"122","article-title":"Temporal logic with past is exponentially more succinct","volume":"79","author":"Markey Nicolas","year":"2003","unstructured":"Nicolas Markey . 2003 . Temporal logic with past is exponentially more succinct . EATCS Bull. 79 (2003), 122 -- 128 . Nicolas Markey. 2003. Temporal logic with past is exponentially more succinct. EATCS Bull. 79 (2003), 122--128.","journal-title":"EATCS Bull."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/646501.695960"},{"key":"e_1_2_1_62_1","volume-title":"Computation of temporal operators. Logique Anal. 28, 110\/111","author":"Michel Max","year":"1985","unstructured":"Max Michel . 1985. Computation of temporal operators. Logique Anal. 28, 110\/111 ( 1985 ), 137--152. Max Michel. 1985. Computation of temporal operators. Logique Anal. 28, 110\/111 (1985), 137--152."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802176"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.33"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/648230.752639"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_38"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_11"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/647325.721668"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.5555\/646883.710932"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_22"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734097"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370629.2370633"},{"key":"e_1_2_1_75_1","volume-title":"Computer Science Today","author":"Vardi Moshe Y.","unstructured":"Moshe Y. Vardi . 1995. Alternating automata and program verification . In Computer Science Today . Springer , 471--485. Moshe Y. Vardi. 1995. Alternating automata and program verification. In Computer Science Today. Springer, 471--485."},{"key":"e_1_2_1_76_1","volume-title":"Proceedings of the 1st Symposium on Logic in Computer Science. IEEE Computer Society, 322--331","author":"Moshe","unstructured":"Moshe Y. Vardi and Pierre Wolper. 1986. An automata-theoretic approach to automatic program verification . In Proceedings of the 1st Symposium on Logic in Computer Science. IEEE Computer Society, 322--331 . Moshe Y. Vardi and Pierre Wolper. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st Symposium on Logic in Computer Science. IEEE Computer Society, 322--331."},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.5555\/646843.706617"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3286976","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3286976","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3286976"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,23]]},"references-count":76,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6,30]]}},"alternative-id":["10.1145\/3286976"],"URL":"https:\/\/doi.org\/10.1145\/3286976","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,5,23]]},"assertion":[{"value":"2018-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-05-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}