{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,6]],"date-time":"2024-10-06T00:38:28Z","timestamp":1728175108206},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040801"},{"type":"electronic","value":"9783642040818"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-04081-8_33","type":"book-chapter","created":{"date-parts":[[2009,8,31]],"date-time":"2009-08-31T12:27:08Z","timestamp":1251721628000},"page":"496-510","source":"Crossref","is-referenced-by-count":22,"title":["Time-Bounded Verification"],"prefix":"10.1007","author":[{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Rabinovich","sequence":"additional","affiliation":[]},{"given":"James","family":"Worrell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","volume-title":"Proceedings of LICS","author":"R. Alur","year":"1990","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of LICS. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci.\u00a0126 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J.\u00a0ACM\u00a043(1) (1996)","DOI":"10.1145\/227595.227602"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci.\u00a0211 (1999)","DOI":"10.1016\/S0304-3975(97)00173-4"},{"key":"33_CR5","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)"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Inf. and Comput.\u00a0104(1) (1993)","DOI":"10.1006\/inco.1993.1025"},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-31954-2_5","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2005","unstructured":"Alur, R., La Torre, S., Madhusudan, P.: Perturbed timed automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 70\u201385. Springer, Heidelberg (2005)"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci.\u00a0345(1) (2005)","DOI":"10.1016\/j.tcs.2005.07.022"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-70583-3_11","volume-title":"Automata, Languages and Programming","author":"P. Bouyer","year":"2008","unstructured":"Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: On expressiveness and complexity in real-time model checking. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 124\u2013135. Springer, Heidelberg (2008)"},{"key":"33_CR10","unstructured":"Bo\u0161na\u010dki, D.: Digitization of timed automata. In: Proceedings of FMICS (1999)"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11730637_17","volume-title":"Hybrid Systems: Computation and Control","author":"M. Emmi","year":"2006","unstructured":"Emmi, M., Majumdar, R.: Decision problems for the verification of real-time software. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol.\u00a03927, pp. 200\u2013211. Springer, Heidelberg (2006)"},{"key":"33_CR12","volume-title":"Proceedings of POPL","author":"D.M. Gabbay","year":"1980","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: Proceedings of POPL. ACM Press, New York (1980)"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BFb0014736","volume-title":"Hybrid and Real-Time Systems","author":"V. Gupta","year":"1997","unstructured":"Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol.\u00a01201, pp. 331\u2013345. Springer, Heidelberg (1997)"},{"key":"33_CR14","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":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-46430-1_15","volume-title":"Hybrid Systems: Computation and Control","author":"T.A. Henzinger","year":"2000","unstructured":"Henzinger, T.A., Raskin, J.-F.: Robust undecidability of timed and hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, p. 145. Springer, Heidelberg (2000)"},{"key":"33_CR16","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, p. 580. Springer, Heidelberg (1998)"},{"key":"33_CR17","doi-asserted-by":"crossref","unstructured":"Herrmann, P.: Timed automata and recognizability. Inf. Process. Lett.\u00a065 (1998)","DOI":"10.1016\/S0020-0190(97)00217-2"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Hirshfeld, Y., Rabinovich, A.: Future temporal logic needs infinitely many modalities. Inf. Comput.\u00a0187(2) (2003)","DOI":"10.1016\/S0890-5401(03)00163-9"},{"key":"33_CR19","unstructured":"Hirshfeld, Y., Rabinovich, A.: Logics for real time: Decidability and complexity. Fundam. Inform.\u00a062(1) (2004)"},{"key":"33_CR20","doi-asserted-by":"crossref","unstructured":"Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. Logical Methods in Computer Science\u00a03(1) (2007)","DOI":"10.2168\/LMCS-3(1:3)2007"},{"key":"33_CR21","unstructured":"Kamp, H.: Tense logic and the theory of linear order. Ph.D. Thesis (1968)"},{"key":"33_CR22","volume-title":"Proceedings of QEST","author":"J.-P. Katoen","year":"2006","unstructured":"Katoen, J.-P., Zapreev, I.S.: Safe on-the-fly steady-state detection for time-bounded reachability. In: Proceedings of QEST. IEEE Computer Society, Los Alamitos (2006)"},{"key":"33_CR23","volume-title":"Proceedings of RTSS","author":"D.K. Kaynar","year":"2003","unstructured":"Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: Timed I\/O Automata: A mathematical framework for modeling and analyzing real-time systems. In: Proceedings of RTSS. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"33_CR24","doi-asserted-by":"crossref","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems\u00a02(4) (1990)","DOI":"10.1007\/BF01995674"},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Lutz, C., Walther, D., Wolter, F.: Quantitative temporal logics over the reals: PSpace and below. Inf. and Comput.\u00a0205 (2007)","DOI":"10.1016\/j.ic.2006.08.006"},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Attiya, H.: Using mappings to prove timing properties. Distributed Computing\u00a06(2) (1992)","DOI":"10.1007\/BF02252683"},{"key":"33_CR27","series-title":"LNM","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BFb0064872","volume-title":"Logic colloquium","author":"A.R. Meyer","year":"1975","unstructured":"Meyer, A.R.: Weak monadic second-order theory of successor is not elementary-recursive. In: Logic colloquium. LNM, vol.\u00a0453, pp. 72\u201373. Springer, Heidelberg (1975)"},{"key":"33_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-46002-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Ouaknine","year":"2002","unstructured":"Ouaknine, J.: Digitisation and full abstraction for dense-time model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 37. Springer, Heidelberg (2002)"},{"key":"33_CR29","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Rabinovich, A., Worrell, J.: Time-bounded verification (full version) (in preparation, 2009)","DOI":"10.1007\/978-3-642-04081-8_33"},{"key":"33_CR30","volume-title":"Proceedings of LICS","author":"J. Ouaknine","year":"2003","unstructured":"Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: Proceedings of LICS. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"33_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/3-540-36580-X_28","volume-title":"Hybrid Systems: Computation and Control","author":"J. Ouaknine","year":"2003","unstructured":"Ouaknine, J., Worrell, J.: Universality and language inclusion for open and closed timed automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 375\u2013388. Springer, Heidelberg (2003)"},{"key":"33_CR32","volume-title":"Proceedings of LICS","author":"J. Ouaknine","year":"2004","unstructured":"Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: Proceedings of LICS. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"33_CR33","volume-title":"Proceedings of LICS","author":"J. Ouaknine","year":"2005","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of Metric Temporal Logic. In: Proceedings of LICS. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"33_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/11691372_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Ouaknine","year":"2006","unstructured":"Ouaknine, J., Worrell, J.: Safety Metric Temporal Logic is fully decidable. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 411\u2013425. Springer, Heidelberg (2006)"},{"key":"33_CR35","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability and complexity of Metric Temporal Logic over finite words. Logical Methods in Computer Science\u00a03(1) (2007)","DOI":"10.2168\/LMCS-3(1:8)2007"},{"key":"33_CR36","doi-asserted-by":"crossref","unstructured":"Rabinovich, A.: Finite variability interpretation of monadic logic of order. Theor. Comput. Sci.\u00a0275(1-2) (2002)","DOI":"10.1016\/S0304-3975(01)00126-8"},{"key":"33_CR37","unstructured":"Raskin, J.-F.: Logics, Automata and Classical Theories for Deciding Real Time. PhD thesis, University of Namur (1999)"},{"key":"33_CR38","unstructured":"Reynolds, M.: The complexity of temporal logic over the reals (2004) (submitted)"},{"key":"33_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-60472-3_21","volume-title":"Hybrid Systems II","author":"O. Roux","year":"1995","unstructured":"Roux, O., Rusu, V.: Verifying time-bounded properties for ELECTRE reactive programs with stopwatch automata. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 105\u2013116. Springer, Heidelberg (1995)"},{"key":"33_CR40","doi-asserted-by":"crossref","unstructured":"Shelah, S.: The monadic theory of order. Ann. Math.\u00a0102 (1975)","DOI":"10.2307\/1971037"},{"key":"33_CR41","unstructured":"Stockmeyer, L.J.: The complexity of decision problems in automata theory and logic. PhD thesis, MIT (1974)"},{"key":"33_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/3-540-61604-7_75","volume-title":"CONCUR \u201996: Concurrency Theory","author":"S. Ta\u015firan","year":"1996","unstructured":"Ta\u015firan, S., Alur, R., Kurshan, R.P., Brayton, R.K.: Verifying abstractions of timed systems. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 546\u2013562. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2009 - Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04081-8_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T04:47:26Z","timestamp":1558500446000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04081-8_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040801","9783642040818"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04081-8_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}