{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:47Z","timestamp":1776333467832,"version":"3.51.2"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T00:00:00Z","timestamp":1587081600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council under the European Union?s Horizon 2020 research and innovation programme","award":["694277"],"award-info":[{"award-number":["694277"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2020,7,31]]},"abstract":"<jats:p>Timed Automata (TA) is de facto a standard modelling formalism to represent systems when the interest is the analysis of their behaviour as time progresses. This modelling formalism is mostly used for checking whether the behaviours of a system satisfy a set of properties of interest. Even if efficient model-checkers for Timed Automata exist, these tools are not easily configurable. First, they are not designed to easily allow adding new Timed Automata constructs, such as new synchronization mechanisms or communication procedures, but they assume a fixed set of Timed Automata constructs. Second, they usually do not support the Metric Interval Temporal Logic (MITL) and rely on a precise semantics for the logic in which the property of interest is specified, which cannot be easily modified and customized. Finally, they do not easily allow using different solvers that may speed up verification in different contexts.<\/jats:p>\n          <jats:p>This article presents a novel technique to perform model checking of Metric Interval Temporal Logic (MITL) properties on TA. The technique relies on the translation of both the TA and the MITL formula into an intermediate Constraint LTL over clocks (CLTLoc) formula, which is verified through an available decision procedure. The technique is flexible, since the intermediate logic allows the encoding of new semantics as well as new TA constructs, by just adding new CLTLoc formulae. Furthermore, our technique is not bound to a specific solver as the intermediate CLTLoc formula can be verified using different procedures.<\/jats:p>","DOI":"10.1145\/3383687","type":"journal-article","created":{"date-parts":[[2020,5,4]],"date-time":"2020-05-04T06:52:27Z","timestamp":1588575147000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking MITL Formulae on Timed Automata"],"prefix":"10.1145","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5303-8481","authenticated-orcid":false,"given":"Claudio","family":"Menghi","sequence":"first","affiliation":[{"name":"SnT-Interdisciplinary Centre for Security, Reliability and Trust, University of Luxembourg, Luxembourg"}]},{"given":"Marcello M.","family":"Bersani","sequence":"additional","affiliation":[{"name":"Dipartimento di Elettronica, Informazione e Bioingegneria, Politecnico di Milano, Milan, Italy"}]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[{"name":"Dipartimento di Meccanica, Politecnico di Milano, Milan, Italy"}]},{"given":"Pierluigi San","family":"Pietro","sequence":"additional","affiliation":[{"name":"Dipartimento di Elettronica, Informazione e Bioingegneria, Politecnico di Milano, Milan, Italy"}]}],"member":"320","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"IEEE. [n.d.]. IEEE Web Page. Retrieved from http:\/\/www.ieee802.org\/3.  IEEE. [n.d.]. IEEE Web Page. Retrieved from http:\/\/www.ieee802.org\/3."},{"key":"e_1_2_1_2_1","unstructured":"Uppaal. [n.d.]. Uppaal Web Page. Retrieved from http:\/\/www.uppaal.org\/.  Uppaal. [n.d.]. Uppaal Web Page. Retrieved from http:\/\/www.uppaal.org\/."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and Leslie Lamport. 1994. An old-fashioned recipe for real time. Trans. Program. Lang. Syst. (1994) 1543--1571.  Mart\u00edn Abadi and Leslie Lamport. 1994. An old-fashioned recipe for real time. Trans. Program. Lang. Syst. (1994) 1543--1571.","DOI":"10.1145\/186025.186058"},{"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.1145\/2851613.2851833"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.16"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.119.8"},{"key":"e_1_2_1_9_1","first-page":"72","article-title":"An SMT-based approach to satisfiability checking of MITL. Info","volume":"245","author":"Bersani Marcello M.","year":"2015","journal-title":"Comp."},{"key":"e_1_2_1_10_1","volume-title":"A logical characterization of timed regular languages. Theoretical Computer Science 658, Part A","author":"Bersani Marcello M.","year":"2017"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0229-y"},{"key":"e_1_2_1_12_1","first-page":"97","article-title":"On the expressiveness of TPTL and MTL. Info","volume":"208","author":"Bouyer Patricia","year":"2010","journal-title":"Comput."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS2018.2018.00027"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_21"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Symposium on Temporal Representation and Reasoning (TIME\u201917)","volume":"90","author":"Brihaye Thomas","year":"2017"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the International Verification Workshop (VERIFY\u201910)","author":"Carioni Alessandro","year":"2010"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00743-0"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_19_1","first-page":"380","article-title":"An automata-theoretic approach to constraint LTL. Info","volume":"205","author":"Demri St\u00e9phane","year":"2007","journal-title":"Comput."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220894.3221079"},{"key":"e_1_2_1_21_1","volume-title":"Modeling Time in Computing","author":"Furia Carlo A."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370629.2370631"},{"key":"e_1_2_1_23_1","volume-title":"FDDI Handbook: High-speed Networking Using Fiber and Other Media","author":"Jain Raj"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer.","author":"Kant Gijs"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.25"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_6"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11867340_20"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47846-3_13"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_1"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201901)","author":"Wang Farn","year":"2001"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3383687","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3383687","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:33:19Z","timestamp":1750199599000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3383687"}},"subtitle":["A Logic-based Approach"],"short-title":[],"issued":{"date-parts":[[2020,4,17]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,7,31]]}},"alternative-id":["10.1145\/3383687"],"URL":"https:\/\/doi.org\/10.1145\/3383687","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,17]]},"assertion":[{"value":"2018-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}