{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T01:06:28Z","timestamp":1794359188861,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540881933","type":"print"},{"value":"9783540881940","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88194-0_19","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T10:56:21Z","timestamp":1224240981000},"page":"298-317","source":"Crossref","is-referenced-by-count":3,"title":["Practical Automated Partial Verification of Multi-paradigm Real-Time Models"],"prefix":"10.1007","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matteo","family":"Pradella","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2","key":"19_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"19_CR2","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R. Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM\u00a043(1), 116\u2013146 (1996)","journal-title":"Journal of the ACM"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/BFb0031988","volume-title":"Real-Time: Theory in Practice","author":"R. Alur","year":"1992","unstructured":"Alur, R., Henzinger, T.A.: Logics and models of real time: A survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol.\u00a0600, pp. 74\u2013106. Springer, Heidelberg (1992)"},{"issue":"1","key":"19_CR4","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":"3","key":"19_CR5","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s00165-005-0067-8","volume":"17","author":"M. De Wulf","year":"2005","unstructured":"De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: from timed models to timed implementations. Formal Aspects of Computing\u00a017(3), 319\u2013341 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2007)"},{"key":"19_CR7","unstructured":"Furia, C.A.: Scaling up the formal analysis of real-time systems. PhD thesis, DEI, Politecnico di Milano (May 2007)"},{"key":"19_CR8","unstructured":"Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling time in computing. Technical Report 2007.22, DEI, Politecnico di Milano (January 2007)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-68237-0_11","volume-title":"FM 2008: Formal Methods","author":"C.A. Furia","year":"2008","unstructured":"Furia, C.A., Pradella, M., Rossi, M.: Automated verification of dense-time MTL specifications via discrete-time approximation. In: Cuellar, J., Maibaum, T.S.E. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 132\u2013147. Springer, Heidelberg (2008)"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Pradella, M., Rossi, M.: Practical automated partial verification of multi-paradigm real-time models (April 2008), http:\/\/arxiv.org\/abs\/0804.4383","DOI":"10.1007\/978-3-540-88194-0_19"},{"key":"19_CR11","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":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1007\/BFb0055086","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 580\u2013591. Springer, Heidelberg (1998)"},{"issue":"4","key":"19_CR14","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":"19_CR15","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1\u20132) (1997)","DOI":"10.1007\/s100090050010"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/11867340_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"O. Maler","year":"2006","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 274\u2013289. Springer, Heidelberg (2006)"},{"key":"19_CR17","unstructured":"Pradella, M.: zot (March 2007), http:\/\/home.dei.polimi.it\/pradella"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. In: Proc. of ESEC\/FSE 2007 (2007)","DOI":"10.1145\/1287624.1287669"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T15:08:08Z","timestamp":1557846488000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_19","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}