{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T23:26:28Z","timestamp":1725578788673},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642198281"},{"type":"electronic","value":"9783642198298"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-19829-8_10","type":"book-chapter","created":{"date-parts":[[2011,3,16]],"date-time":"2011-03-16T10:20:41Z","timestamp":1300270841000},"page":"144-160","source":"Crossref","is-referenced-by-count":26,"title":["Statistical Verification of Probabilistic Properties with Unbounded Until"],"prefix":"10.1007","author":[{"given":"H\u00e5kan L. S.","family":"Younes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Zuliani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"6","key":"10_CR1","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.R., 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"},{"key":"10_CR2","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-10373-5_17","volume-title":"Formal Methods and Software Engineering","author":"S. Basu","year":"2009","unstructured":"Basu, S., Ghosh, A.P., He, R.: Approximate model checking of PCTL involving unbounded path properties. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 326\u2013346. Springer, Heidelberg (2009)"},{"issue":"2","key":"10_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"issue":"2","key":"10_CR5","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1214\/aoms\/1177700156","volume":"36","author":"Y.S. Chow","year":"1965","unstructured":"Chow, Y.S., Robbins, H.: On the asymptotic theory of fixed-width sequential confidence intervals for the mean. Annals of Mathematical Statistics\u00a036(2), 457\u2013462 (1965)","journal-title":"Annals of Mathematical Statistics"},{"key":"10_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-04761-9_11","volume-title":"Automated Technology for Verification and Analysis","author":"D. Rabih El","year":"2009","unstructured":"El Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 120\u2013134. Springer, Heidelberg (2009)"},{"key":"10_CR8","series-title":"LNCS","volume-title":"Proc. 17th CAV","year":"2005","unstructured":"Etessami, K., Rajamani, S.K. (eds.): CAV 2005. LNCS, vol.\u00a03576. Springer, Heidelberg (2005)"},{"key":"10_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2553-7","volume-title":"Monte Carlo: Concepts, Algorithms, and Applications","author":"G.S. Fishman","year":"1996","unstructured":"Fishman, G.S.: Monte Carlo: Concepts, Algorithms, and Applications. Springer, Heidelberg (1996)"},{"issue":"31","key":"10_CR10","doi-asserted-by":"publisher","first-page":"127","DOI":"10.2307\/2002508","volume":"4","author":"G.E. Forsythe","year":"1950","unstructured":"Forsythe, G.E., Leibler, R.A.: Matrix inversion by a Monte Carlo method. Mathematical Tables and Other Aids to Computation\u00a04(31), 127\u2013129 (1950)","journal-title":"Mathematical Tables and Other Aids to Computation"},{"key":"10_CR11","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-94-009-5819-7_7","volume-title":"Monte Carlo Methods","author":"J.M. Hammersley","year":"1964","unstructured":"Hammersley, J.M., Handscomb, D.C.: Solution of linear operator equations. In: Monte Carlo Methods, ch. 7, pp. 85\u201396. Methuen & Co, New York (1964)"},{"issue":"5","key":"10_CR12","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(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"10_CR13","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation\u00a0111(2), 193\u2013244 (1994)","journal-title":"Information and Computation"},{"key":"10_CR14","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Proc. 3rd International Workshop on the Numerical Solution of Markov Chains, pp. 188\u2013207, Prensas Universitarias de Zaragoza (1999)"},{"issue":"301","key":"10_CR15","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","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(301), 13\u201330 (1963)","journal-title":"Journal of the American Statistical Association"},{"issue":"9","key":"10_CR16","doi-asserted-by":"publisher","first-page":"1649","DOI":"10.1109\/49.62852","volume":"8","author":"O.C. Ibe","year":"1990","unstructured":"Ibe, O.C., Trivedi, K.S.: Stochastic Petri net models of polling systems. IEEE Journal on Selected Areas in Communications\u00a08(9), 1649\u20131657 (1990)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"issue":"2","key":"10_CR17","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"M. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer\u00a06(2), 128\u2013142 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"1\u20133","key":"10_CR18","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/j.apal.2007.11.006","volume":"152","author":"R. Lassaigne","year":"2008","unstructured":"Lassaigne, R., Peyronnet, S.: Probabilistic verification and approximation. Annals of Pure and Applied Logic\u00a0152(1\u20133), 122\u2013131 (2008)","journal-title":"Annals of Pure and Applied Logic"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1109\/WSC.2006.323046","volume-title":"Proc. 2006 Winter Simulation Conference","author":"P. L\u2019Ecuyer","year":"2006","unstructured":"L\u2019Ecuyer, P., Demers, V., Tuffin, B.: Splitting for rare-event simulation. In: Proc. 2006 Winter Simulation Conference, pp. 137\u2013148. IEEE, Los Alamitos (2006)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: An abstract monte-carlo method for the analysis of probabilistic programs. In: Proc. 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 93\u2013101. Association for Computing Machinery (2001)","DOI":"10.1145\/360204.360211"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 266\u2013280. Springer, Heidelberg (2005)"},{"key":"10_CR22","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"W.J. Stewart","year":"1994","unstructured":"Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)"},{"issue":"2","key":"10_CR23","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A. Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Annals of Mathematical Statistics\u00a016(2), 117\u2013186 (1945)","journal-title":"Annals of Mathematical Statistics"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 429\u2013433. Springer, Heidelberg (2005)"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11609773_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.L.S. Younes","year":"2005","unstructured":"Younes, H.L.S.: Error control for probabilistic model checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 142\u2013156. Springer, Heidelberg (2005)"},{"issue":"9","key":"10_CR26","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"H.L.S. Younes","year":"2006","unstructured":"Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation\u00a0204(9), 1368\u20131409 (2006)","journal-title":"Information and Computation"},{"key":"10_CR27","unstructured":"Zapreev, I.S.: Model checking Markov chains: Techniques and tools. PhD thesis, University of Twente (2008)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19829-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,19]],"date-time":"2019-01-19T11:27:35Z","timestamp":1547897255000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19829-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198281","9783642198298"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19829-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}