{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:41:08Z","timestamp":1725514868417},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_11","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"132-147","source":"Crossref","is-referenced-by-count":8,"title":["Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation"],"prefix":"10.1007","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[]},{"given":"Matteo","family":"Pradella","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"11_CR1","doi-asserted-by":"publisher","first-page":"1543","DOI":"10.1145\/186025.186058","volume":"16","author":"M. Abadi","year":"1994","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real-time. ACM TOPLAS\u00a016(5), 1543\u20131571 (1994)","journal-title":"ACM TOPLAS"},{"issue":"1","key":"11_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Information and Computation\u00a0104(1), 35\u201377 (1993)","journal-title":"Information and Computation"},{"issue":"5:5","key":"11_CR3","first-page":"1","volume":"2","author":"A. Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Comp. Sci.\u00a02(5:5), 1\u201364 (2006)","journal-title":"Logical Methods in Comp. Sci."},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-540-45069-6_17","volume-title":"Computer Aided Verification","author":"G. Chakravorty","year":"2003","unstructured":"Chakravorty, G., Pandya, P.K.: Digiziting interval duration logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 167\u2013179. Springer, Heidelberg (2003)"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/295558.295566","volume":"8","author":"E. Ciapessoni","year":"1999","unstructured":"Ciapessoni, E., Coen-Porisini, A., Crivelli, E., Mandrioli, D., Mirandola, P., Morzenti, A.: From formal models to formally-based methods: an industrial experience. ACM TOSEM\u00a08(1), 79\u2013113 (1999)","journal-title":"ACM TOSEM"},{"key":"11_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Manna, Z.: Verification in continuous time by discrete reasoning. In: AMAST 1995. LNCS, vol.\u00a0936, pp. 292\u2013306 (1995)","DOI":"10.1007\/3-540-60043-4_60"},{"key":"11_CR8","unstructured":"D. D\u2019Souza, R.\u00a0Mohan M., and P.\u00a0Prabhakar. Eliminating past operators in metric temporal logic. Technical Report IISc-CSA-TR-2006-11 (2006)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-75454-1_12","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G.E. Fainekos","year":"2007","unstructured":"Fainekos, G.E., Pappas, G.J.: Robust Sampling for MITL Specifications. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 147\u2013162. Springer, Heidelberg (2007)"},{"key":"11_CR10","unstructured":"Furia, C.A.: Scaling up the formal analysis of real-time systems. PhD thesis, DEI, Politecnico di Milano (May 2007)"},{"key":"11_CR11","unstructured":"Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling time in computing: A taxonomy and a comparative survey. Technical Report 2007.22, DEI, Politecnico di Milano (2007)"},{"key":"11_CR12","unstructured":"Furia, C.A., Pradella, M., Rossi, M.: Dense-time MTL verification through sampling. Technical Report 2007.37, DEI, Politecnico di Milano (April 2007)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/11867340_16","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"C.A. Furia","year":"2006","unstructured":"Furia, C.A., Rossi, M.: Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 215\u2013229. Springer, Heidelberg (2006)"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-540-75454-1_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"C.A. Furia","year":"2007","unstructured":"Furia, C.A., Rossi, M.: On the expressiveness of MTL variants over dense time. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 163\u2013178. Springer, Heidelberg (2007)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/BFb0055640","volume-title":"CONCUR \u201998 Concurrency Theory","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A.: It\u2019s about time: Real-time logics reviewed. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 439\u2013454. Springer, Heidelberg (1998)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 545\u2013558. Springer, Heidelberg (1992)"},{"issue":"1","key":"11_CR17","first-page":"1","volume":"62","author":"Y. Hirshfeld","year":"2004","unstructured":"Hirshfeld, Y., Rabinovich, A.M.: Logics for real time: Decidability and complexity. Fundamenta Informaticae\u00a062(1), 1\u201328 (2004)","journal-title":"Fundamenta Informaticae"},{"issue":"4","key":"11_CR18","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R. Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems\u00a02(4), 255\u2013299 (1990)","journal-title":"Real-Time Systems"},{"key":"11_CR19","unstructured":"Pradella, M.: Zot (March 2007), \n                    \n                      http:\/\/home.dei.polimi.it\/pradella"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future. In: Proc. of ESEC\/FSE 2007 (2007)","DOI":"10.1145\/1287624.1287669"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-540-31980-1_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Sharma","year":"2005","unstructured":"Sharma, B., Pandya, P.K., Chakraborty, S.: Bounded validity checking of interval duration logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 301\u2013316. Springer, Heidelberg (2005)"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"694","DOI":"10.1007\/3-540-58468-4_191","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"T. Wilke","year":"1994","unstructured":"Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol.\u00a0863, pp. 694\u2013715. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:43:32Z","timestamp":1620017012000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_11","relation":{},"subject":[]}}