{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:06:14Z","timestamp":1760043974530},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253884"},{"type":"electronic","value":"9783540319825"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31982-5_9","type":"book-chapter","created":{"date-parts":[[2011,1,14]],"date-time":"2011-01-14T02:29:02Z","timestamp":1294972142000},"page":"140-154","source":"Crossref","is-referenced-by-count":15,"title":["Model Checking Durational Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Laroussinie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Sproston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S. Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 88\u2013104. Springer, Heidelberg (2004)"},{"issue":"6","key":"9_CR3","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"9_CR4","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing\u00a011(3), 125\u2013155 (1998)","journal-title":"Distributed Computing"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"9_CR6","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1109\/REAL.1994.342709","volume-title":"Proc. IEEE Real-Time Systems Symposium (RTSS 1994)","author":"S. Campos","year":"1994","unstructured":"Campos, S., Clarke, E.M., Marrero, W.R., Minea, M., Hiraishi, H.: Computing quantitative characteristic of finite-state real-time systems. In: Proc. IEEE Real-Time Systems Symposium (RTSS 1994), pp. 266\u2013270. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"9_CR7","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)"},{"issue":"4","key":"9_CR8","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. PhD thesis, Stanford University, Department of Computer Science (1997)","key":"9_CR9"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BFb0023457","volume-title":"STACS 97","author":"L. Alfaro de","year":"1997","unstructured":"de Alfaro, L.: Temporal logics for the specification of performance and reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 165\u2013176. Springer, Heidelberg (1997)"},{"issue":"4","key":"9_CR11","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E.A. Emerson","year":"1992","unstructured":"Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. Real Time Systems\u00a04(4), 331\u2013352 (1992)","journal-title":"Real Time Systems"},{"key":"9_CR12","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, New York (1979)"},{"issue":"5","key":"9_CR13","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H.A. Hansson","year":"1994","unstructured":"Hansson, H.A., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1109\/LICS.2003.1210075","volume-title":"Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003)","author":"M. Kwiatkowska","year":"2003","unstructured":"Kwiatkowska, M.: Model checking for probability and time: From theory to practice. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 351\u2013360. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"286","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science\u00a0286, 101\u2013150 (2002)","journal-title":"Theoretical Computer Science"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/3-540-45931-6_19","volume-title":"Foundations of Software Science and Computation Structures","author":"F. Laroussinie","year":"2002","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: On model checking durational Kripke structures (extended abstract). In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 264\u2013279. Springer, Heidelberg (2002)"},{"unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete time systems (2004) (submitted)","key":"9_CR17"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 299\u2013314. Springer, Heidelberg (1999)"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1109\/SFCS.1985.12","volume-title":"Proc. 16th Annual Symp. on Foundations of Computer Science (FOCS 1985)","author":"M.Y. Vardi","year":"1985","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. 16th Annual Symp. on Foundations of Computer Science (FOCS 1985), pp. 327\u2013338. IEEE Computer Society Press, Los Alamitos (1985)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31982-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:40:29Z","timestamp":1558294829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31982-5_9"}},"subtitle":["(Extended Abstract)"],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253884","9783540319825"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31982-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}