{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:23:01Z","timestamp":1762323781901,"version":"3.40.5"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,2,4]],"date-time":"2015-02-04T00:00:00Z","timestamp":1423008000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,8]]},"DOI":"10.1007\/s10009-015-0368-z","type":"journal-article","created":{"date-parts":[[2015,2,3]],"date-time":"2015-02-03T07:31:35Z","timestamp":1422948695000},"page":"417-427","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Statistical model checking for unbounded until formulas"],"prefix":"10.1007","volume":"17","author":[{"given":"Nima","family":"Roohi","sequence":"first","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,2,4]]},"reference":[{"key":"368_CR1","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for hybrid automata stochastic logic. In: Proceedings of the International Conference on the Quantitative Evaluation of Systems, pp. 143\u2013144 (2011)","DOI":"10.1109\/QEST.2011.24"},{"key":"368_CR2","doi-asserted-by":"crossref","unstructured":"Basu, S., Ghosh, A.P., He, R.: Approximate model checking of PCTL involving unbounded path properties. In: Proceedings of the International Conference on Formal Engineering Methods, pp. 326\u2013346 (2009)","DOI":"10.1007\/978-3-642-10373-5_17"},{"issue":"2","key":"368_CR3","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1214\/aoms\/1177700156","volume":"36","author":"YS Chow","year":"1965","unstructured":"Chow, Y.S., Robbins, H.: On the asymptotic theory of fixed-width sequential confidence intervals for the mean. Ann. Math. Stat. 36(2), 457\u2013462 (1965)","journal-title":"Ann. Math. Stat."},{"issue":"4","key":"368_CR4","doi-asserted-by":"crossref","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. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"issue":"4","key":"368_CR5","doi-asserted-by":"crossref","first-page":"127","DOI":"10.2307\/2002508","volume":"31","author":"GE Forsythe","year":"1950","unstructured":"Forsythe, G.E., Leibler, R.: Matrix inversion by a Monte Carlo method. Math. Tables Other Aids Comput. 31(4), 127\u2013129 (1950)","journal-title":"Math. Tables Other Aids Comput."},{"key":"368_CR6","doi-asserted-by":"crossref","unstructured":"Grosu, R., Smolka, S.: Monte-carlo model checking. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 271\u2013286 (2005)","DOI":"10.1007\/978-3-540-31980-1_18"},{"key":"368_CR7","doi-asserted-by":"crossref","unstructured":"Herault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 73\u201384 (2004)","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"368_CR8","doi-asserted-by":"crossref","unstructured":"Herault, T., Lassaigne, R., Peyronnet, S.: APMC 3.0: Approximate verification of discrete and continuous time Markov chains. In: Proceedings of the International Conference on the Quantitative Evaluation of Systems, pp. 129\u2013130 (2006)","DOI":"10.1109\/QEST.2006.5"},{"key":"368_CR9","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Proceedings of the International Workshop on Numerical Solution of Markov Chains, pp. 188\u2013207 (1999)"},{"key":"368_CR10","doi-asserted-by":"crossref","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. J. Am. Stat. Assoc. 58, 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"issue":"9","key":"368_CR11","doi-asserted-by":"crossref","first-page":"1649","DOI":"10.1109\/49.62852","volume":"8","author":"O Ibe","year":"1990","unstructured":"Ibe, O., Trivedi, K.: Stochastic Petri net models of polling systems. IEEE J. Sel. Areas Commun. 8(9), 1649\u20131657 (1990)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"368_CR12","doi-asserted-by":"crossref","unstructured":"Jegourel, C., Legay, A., Sedwards, A.: A platform for high performance statistical model checking\u2014PLASMA. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 498\u2013503 (2012)","DOI":"10.1007\/978-3-642-28756-5_37"},{"key":"368_CR13","doi-asserted-by":"crossref","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate verification of probabilistic systems. In: Proceedings of the Second Joint International Workshop in Process Algebra and Probabilistic Methods, Performance Modeling and Verification, pp. 213\u2013214 (2002)","DOI":"10.1007\/3-540-45605-8_16"},{"issue":"1\u20133","key":"368_CR14","doi-asserted-by":"crossref","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. Ann. Pure Appl. Logic 152(1\u20133), 122\u2013131 (2008)","journal-title":"Ann. Pure Appl. Logic"},{"key":"368_CR15","doi-asserted-by":"crossref","unstructured":"Propp, D., Wilson, J.: Exact sampling with coupled Markov chains and applications to statistical mechanics. Random Struct. Algorithms 9(1), 223\u2013252 (1996)","DOI":"10.1002\/(SICI)1098-2418(199608\/09)9:1\/2<223::AID-RSA14>3.0.CO;2-O"},{"key":"368_CR16","doi-asserted-by":"crossref","unstructured":"El Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: Proceedings of the International Symposium on Automated Technology for Verification and Analysis, pp. 120\u2013134 (2009)","DOI":"10.1007\/978-3-642-04761-9_11"},{"key":"368_CR17","unstructured":"Sebastio, S., Vandin, A.: Multivesta: Statistical model checking for discrete event simulators. In: Proceedings of the International Conference on Performance Evaluation Methodologies and Tools, pp. 310\u2013315 (2013)"},{"key":"368_CR18","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Proceedings of the International Conference on Computer-Aided Verification, pp. 202\u2013215 (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"368_CR19","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Proceedings of the International Conference on Computer-Aided Verification, pp. 266\u2013280 (2005)","DOI":"10.1007\/11513988_26"},{"key":"368_CR20","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: Proceedings of the International Conference on the Quantitative Evaluation of Systems, pp. 251\u2013252 (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"368_CR21","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the IEEE Symposium on Foundations of Computer Science, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"368_CR22","unstructured":"Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon University (2005)"},{"key":"368_CR23","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: Proceedings of the Brazilian Symposium on Formal Methods, pp. 144\u2013160 (2010)","DOI":"10.1007\/978-3-642-19829-8_10"},{"issue":"3","key":"368_CR24","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"HLS Younes","year":"2006","unstructured":"Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Softw. Tools Technol. Transf. 8(3), 216\u2013228 (2006)","journal-title":"Softw. Tools Technol. Transf."},{"key":"368_CR25","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Proceedings of the International Conference on Computer-Aided Verification, pp. 223\u2013235 (2002)","DOI":"10.1007\/3-540-45657-0_17"},{"issue":"9","key":"368_CR26","doi-asserted-by":"crossref","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"HLS Younes","year":"2006","unstructured":"Younes, H.L.S., Simmons, R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368\u20131409 (2006)","journal-title":"Inf. Comput."},{"key":"368_CR27","unstructured":"Zapreev, I.S.: Model checking Markov chains: techniques and tools. Ph.D. thesis, University of Twente (2008)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0368-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0368-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0368-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:50:24Z","timestamp":1747551024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0368-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,4]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["368"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0368-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2015,2,4]]}}}