{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:32:58Z","timestamp":1750307578357,"version":"3.41.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2010,10,1]],"date-time":"2010-10-01T00:00:00Z","timestamp":1285891200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["227977SMScom"],"award-info":[{"award-number":["227977SMScom"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2010,10]]},"abstract":"<jats:p>This article revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of metric temporal logic (MTL) formulas over continuous-time models and over discrete-time models is studied. It is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. The main results apply to \u201cflat\u201d formulas that do not nest temporal operators and can be applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete time, resulting in an automated partial practically efficient discretization technique.<\/jats:p>","DOI":"10.1145\/1838552.1838560","type":"journal-article","created":{"date-parts":[[2010,11,3]],"date-time":"2010-11-03T14:16:37Z","timestamp":1288793797000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["A theory of sampling for continuous-time metric temporal logic"],"prefix":"10.1145","volume":"12","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, Milan, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,11,26]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1025"},{"volume":"1466","volume-title":"Proceedings of the 9th International Conference on Concurrency Theory (CONCUR). D. Sangiorgi and R. de Simone, Eds. Lecture Notes in Computer Science","author":"Asarin E.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Benedetto J. J. and Ferreira P. J. S. G. Eds. 2001. Modern Sampling Theory. Birk\u00e4user Boston MA.  Benedetto J. J. and Ferreira P. J. S. G. Eds. 2001. Modern Sampling Theory. Birk\u00e4user Boston MA.","DOI":"10.1007\/978-1-4612-0143-4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.16"},{"volume-title":"Rabbit: A tool for BDD-based verification of real-time systems. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV). W. A. H. Jr","year":"2003","author":"Beyer D.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSECOMPANION.2007.79"},{"volume-title":"Proceedings of the 4th International Workshop on Formal Methods for Industrial Critical Systems (FMICS). 283--302","year":"1999","author":"Bo\u0161na\u010dki D.","key":"e_1_2_1_8_1"},{"volume":"863","volume-title":"Proceedings of the 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). Lecture Notes in Computer Science","author":"Bouajjani A.","key":"e_1_2_1_9_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.49"},{"volume":"1703","volume-title":"Proceedings of the 10th Correct Hardware Design and Verification Methods Advanced Research Working Conference (CHARME). L. Pierre and T. Kropf, Eds. Lecture Notes in Computer Science","author":"Bozga M.","key":"e_1_2_1_11_1"},{"volume":"2725","volume-title":"Proceedings of the 15th International Conference on Computer Aided Verification (CAV), W. A. Hunt, Jr. and F. Somenzi, Eds. Lecture Notes in Computer Science","author":"Chakravorty G.","key":"e_1_2_1_12_1"},{"volume":"2404","volume-title":"Proceedings of the 14th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science","author":"Cimatti A.","key":"e_1_2_1_13_1"},{"volume-title":"Proceedings of the GM R&amp;D Workshop on Next Generation Design and Verification Methodologies for Distributed Embedded Control System.","author":"Clarke E. M.","key":"e_1_2_1_14_1"},{"volume":"1862","volume-title":"Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic. Lecture Notes in Computer Science","author":"Comon H.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/7.1.55"},{"volume":"936","volume-title":"Proceedings of the 4th International Conference on Algebraic Methodology and Software Technology (AMAST), V. S. Alagar and M. Nivat, Eds. Lecture Notes in Computer Science","author":"de Alfaro L.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_21"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3094"},{"key":"e_1_2_1_20_1","unstructured":"D'Souza D. Mohan M. R. and Prabhakar P. 2007. Flattening metric temporal logic. Manuscript.  D'Souza D. Mohan M. R. and Prabhakar P. 2007. Flattening metric temporal logic. Manuscript."},{"volume-title":"Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press","author":"Etessami K.","key":"e_1_2_1_21_1"},{"volume":"4763","volume-title":"Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science","author":"Fainekos G. E.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_2_1_24_1","unstructured":"Furia C. A. 2007. Scaling up the formal analysis of real-time systems. Ph.D. dissertation Dipartimento di Elettronica e Informazione Politecnico di Milano Milan Italy.  Furia C. A. 2007. Scaling up the formal analysis of real-time systems. Ph.D. dissertation Dipartimento di Elettronica e Informazione Politecnico di Milano Milan Italy."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667062.1667063"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1423684.1423699"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88194-0_19"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11867340_16"},{"volume":"4763","volume-title":"Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). J.-F. Raskin and P. S. Thiagarajan, Eds. Lecture Notes in Computer Science","author":"Furia C. A.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_9"},{"volume-title":"Proceedings of the 33rd Conference on Decision and Control. 957--958","author":"G\u00f6ll\u00fc A.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","volume-title":"Concrete Mathematics: A Foundation for Computer Science","author":"Graham R. L.","year":"1994","edition":"2"},{"key":"e_1_2_1_33_1","unstructured":"Heitmeier C. and Mandrioli D. Eds. 1996. Formal Methods for Real-Time Computing. John Wiley &amp; Sons New York NY.   Heitmeier C. and Mandrioli D. Eds. 1996. Formal Methods for Real-Time Computing. John Wiley &amp; Sons New York NY."},{"volume":"623","volume-title":"19th International Colloquium on Automata, Languages and Programming (ICALP). W. Kuich, Ed. Lecture Notes in Computer Science","author":"Henzinger T. A.","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370629.2370631"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.12.002"},{"volume":"1135","volume-title":"Proceedings of the 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). B. Jonsson and J. Parrow, Eds. Lecture Notes in Computer Science","author":"Hung D. V.","key":"e_1_2_1_38_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"volume-title":"Proceedings of the REX Workshop: \u201cReal-Time: Theory in Practice","author":"Koymans R.","key":"e_1_2_1_40_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/11590156_25"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0164-4"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/11867340_20"},{"volume":"987","volume-title":"Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods. P. Camurati and H. Eveking, Eds. Lecture Notes in Computer Science","author":"Maler O.","key":"e_1_2_1_44_1"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694629"},{"volume-title":"Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press","author":"Ouaknine J.","key":"e_1_2_1_46_1"},{"key":"e_1_2_1_47_1","unstructured":"Pandya P. K. 2008. Personal communication.  Pandya P. K. 2008. Personal communication."},{"volume":"4424","volume-title":"Proceeding of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science","author":"Pandya P. K.","key":"e_1_2_1_48_1"},{"volume":"141","volume-title":"Infinite Words. Pure and Applied Mathematics","author":"Perrin D.","key":"e_1_2_1_49_1"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287669"},{"volume-title":"Proceedings of 1st International Workshop on Automated Technology for Verification and Analysis (ATVA). F. Wang and I. Lee, Eds. 135--146","author":"Pradella M.","key":"e_1_2_1_51_1"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00331-6"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-003-1109-3"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1838552.1838560","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1838552.1838560","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:41:11Z","timestamp":1750250471000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1838552.1838560"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,10]]},"references-count":53,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,10]]}},"alternative-id":["10.1145\/1838552.1838560"],"URL":"https:\/\/doi.org\/10.1145\/1838552.1838560","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2010,10]]},"assertion":[{"value":"2009-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-11-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}