{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,25]],"date-time":"2026-10-25T17:06:17Z","timestamp":1792947977973,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540208037","type":"print"},{"value":"9783540246220","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_8","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T11:33:53Z","timestamp":1283686433000},"page":"73-84","source":"Crossref","is-referenced-by-count":187,"title":["Approximate Probabilistic Model Checking"],"prefix":"10.1007","author":[{"given":"Thomas","family":"H\u00e9rault","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard","family":"Lassaigne","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Magniette","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sylvain","family":"Peyronnet","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. In: Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pp. 207\u2013218 (1996)","DOI":"10.1109\/LICS.1996.561320"},{"key":"8_CR2","unstructured":"APMC homepage, http:\/\/www.lri.fr\/~syp\/APMC"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDD\u2019s. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"issue":"4","key":"8_CR5","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"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: Proc. of the joint PAPM\/PROBMIV (2001)","DOI":"10.1007\/3-540-44804-7_3"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of concurrent probabilistic processes using MTBDDs and the kronecker representation. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 395. Springer, Heidelberg (2000)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-48778-6_6","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"V. Hartonas-Garmhausen","year":"1999","unstructured":"Hartonas-Garmhausen, V., Campos, S., Clarke, E.: Probverus: Probabilistic symbolic model checking. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, p. 96. Springer, Heidelberg (1999)"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06, 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: Markov chain model checker. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 347\u2013362. Springer, Heidelberg (2000)"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"13","DOI":"10.2307\/2282952","volume":"58","author":"W. Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association\u00a058, 13\u201330 (1963)","journal-title":"Journal of the American Statistical Association"},{"key":"8_CR12","unstructured":"Jeannet, B., D\u2019Argenio, P.R., Larsen, K.G.: RAPTURE: A tool for verifying Markov Decision Processes. In: Proc. of CONCUR 2002 (2002)"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1016\/0196-6774(89)90038-2","volume":"10","author":"R.M. Karp","year":"1989","unstructured":"Karp, R.M., Luby, M., Madras, N.: Monte-Carlo algorithms for enumeration and reliability problems. Journal of Algorithms\u00a010, 429\u2013448 (1989)","journal-title":"Journal of Algorithms"},{"key":"8_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable markov chains","author":"J. Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable markov chains. Springer, Heidelberg (1976)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 52. Springer, Heidelberg (2002)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45605-8_16","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"R. Lassaigne","year":"2002","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate Verification of Probabilistic Systems. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 213\u2013214. Springer, Heidelberg (2002)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Lovasz, L., Winkler, P.: Exact mixing time in an unknown markov chain. Electronic journal of combinatorics (1995)","DOI":"10.37236\/1209"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: An abstract Monte-Carlo method for the analysis of probabilistic programs (extended abstract). In: 28th Symposium on Principles of Programming Languages (POPL 2001), pp. 93\u2013101. Association for Computer Machinery (2001)","DOI":"10.1145\/360204.360211"},{"key":"8_CR19","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R. Motwani","year":"1995","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)"},{"key":"8_CR20","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distributed Computing\u00a01, 53\u201372 (1986)","journal-title":"Distributed Computing"},{"issue":"1","key":"8_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.: Probabilistic verification. Information and Computation\u00a0103(1), 1\u201329 (1993)","journal-title":"Information and Computation"},{"key":"8_CR23","unstructured":"PRISM homepagem, http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_78","volume-title":"Automata, Languages and Programming","author":"A. Rabinovich","year":"2003","unstructured":"Rabinovich, A.: Quantitative analysis of probabilistic channel systems. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, Springer, Heidelberg (2003)"},{"issue":"3","key":"8_CR25","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"Journal of the ACM"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. 26th Annual Symposium on Foundations of Computer Science, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"8_CR27","unstructured":"Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). In: Proceedings of the first IEEE Symposium on Logic in Computer Science, pp. 332\u2013344 (1986)"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic Verication of Discrete Event Systems using Acceptance Sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 223\u2013235. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24622-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T08:07:19Z","timestamp":1591862839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}