{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T22:00:02Z","timestamp":1761948002072,"version":"3.40.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,10,1]],"date-time":"2014-10-01T00:00:00Z","timestamp":1412121600000},"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-014-0350-1","type":"journal-article","created":{"date-parts":[[2014,9,30]],"date-time":"2014-09-30T12:19:06Z","timestamp":1412079546000},"page":"377-395","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["On hypothesis testing for statistical model checking"],"prefix":"10.1007","volume":"17","author":[{"given":"Dani\u00ebl","family":"Reijsbergen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pieter-Tjerk","family":"de Boer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Werner","family":"Scheinhardt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boudewijn","family":"Haverkort","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,1]]},"reference":[{"key":"350_CR1","unstructured":"Companion website to this paper. http:\/\/wwwhome.ewi.utwente.nl\/~ptdeboer\/hyptest-for-smc\/"},{"issue":"1","key":"350_CR2","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM TOCL 1(1), 162\u2013170 (2000)","journal-title":"ACM TOCL"},{"key":"350_CR3","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume":"1102","author":"A Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous-time Markov chains. Lect Notes Comput Sci 1102, 269\u2013276 (1996)","journal-title":"Lect Notes Comput Sci"},{"key":"350_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: On the logical characterisation of performability properties. In Automata, Languages and Programming, pages 780\u2013792. LNCS Volume 1853, Springer, 2000","DOI":"10.1007\/3-540-45022-X_65"},{"issue":"6","key":"350_CR5","doi-asserted-by":"crossref","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 Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"350_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)"},{"key":"350_CR7","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: Proceedings of the Eighth International Conference on the Quantitative Evaluation of Systems (QEST), pp. 143\u2013144. IEEE (2011)","DOI":"10.1109\/QEST.2011.24"},{"key":"350_CR8","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL\u2014a tool suite for automatic verification of real-time systems. Hybrid Syst. III, 232\u2013243 (1996)","DOI":"10.1007\/BFb0020949"},{"key":"350_CR9","volume-title":"An Introduction to Optimization","author":"E Chong","year":"2004","unstructured":"Chong, E., \u017bak, S.: An Introduction to Optimization. Wiley, Hoboken (2004)"},{"issue":"2","key":"350_CR10","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":"3","key":"350_CR11","doi-asserted-by":"crossref","first-page":"804","DOI":"10.1073\/pnas.61.3.804","volume":"61","author":"DA Darling","year":"1968","unstructured":"Darling, D.A., Robbins, H.: Some nonparametric sequential tests with power one. Proc. Nat. Acad. Sci. USA 61(3), 804\u2013809 (1968)","journal-title":"Proc. Nat. Acad. Sci. USA"},{"key":"350_CR12","doi-asserted-by":"crossref","unstructured":"El Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: Automated Technology for Verification and Analysis, pp. 120\u2013134. LNCS Volume 5799, Springer (2009)","DOI":"10.1007\/978-3-642-04761-9_11"},{"key":"350_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3552-9","volume-title":"Discrete-Event Simulation: Modeling, Programming, and Analysis","author":"GS Fishman","year":"2001","unstructured":"Fishman, G.S.: Discrete-Event Simulation: Modeling, Programming, and Analysis. Springer, Berlin (2001)"},{"issue":"1","key":"350_CR14","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/5.21067","volume":"77","author":"PW Glynn","year":"1989","unstructured":"Glynn, P.W.: A GSMP formalism for discrete event systems. Proc. IEEE 77(1), 14\u201323 (1989)","journal-title":"Proc. IEEE"},{"key":"350_CR15","doi-asserted-by":"crossref","unstructured":"Grubbs, F.E.: On designing single sampling inspection plans. The Ann. Math. Stat., pp. 242\u2013256 (1949)","DOI":"10.1214\/aoms\/1177730033"},{"issue":"4","key":"350_CR16","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1109\/32.16599","volume":"15","author":"PJ Haas","year":"1989","unstructured":"Haas, P.J., Shedler, G.S.: Stochastic Petri net representation of discrete event simulations. IEEE Trans. Softw. Eng. 15(4), 381\u2013393 (1989)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"5","key":"350_CR17","doi-asserted-by":"crossref","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 6(5), 512\u2013535 (1994)","journal-title":"Formal aspects of computing"},{"key":"350_CR18","first-page":"307","volume":"2937","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. Lect. Notes Comput. Sci. 2937, 307\u2013329 (2004)","journal-title":"Lect. Notes Comput. Sci."},{"key":"350_CR19","doi-asserted-by":"crossref","unstructured":"H\u00e9rault, T., Lassaigne, R., Peyronnet, S.: APMC 3.0: Approximate verification of discrete and continuous time markov chains. In: Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST), pp. 129\u2013130. IEEE (2006)","DOI":"10.1109\/QEST.2006.5"},{"key":"350_CR20","doi-asserted-by":"crossref","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. pp. 13\u201330 (1963)","DOI":"10.1080\/01621459.1963.10500830"},{"key":"350_CR21","volume-title":"Theory of Probability","author":"H Jeffreys","year":"1961","unstructured":"Jeffreys, H.: Theory of Probability. Oxford University Press, Oxford (1961)"},{"key":"350_CR22","doi-asserted-by":"crossref","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking\u2014PLASMA. Tools and Algorithms for the Construction and Analysis of Systems, pp. 498\u2013503 (2012)","DOI":"10.1007\/978-3-642-28756-5_37"},{"key":"350_CR23","doi-asserted-by":"crossref","unstructured":"Jha, S., Clarke, E., Langmead, C., Legay, A., Platzer, A., Zuliani, P.: A Bayesian approach to model checking biological systems. In: Computational Methods in Systems Biology, pp. 218\u2013234. Springer (2009)","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"350_CR24","doi-asserted-by":"crossref","unstructured":"Katoen, J. P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Second International Conference on the Quantitative Evaluation of Systems (QEST), pp. 243\u2013244. IEEE (2005)","DOI":"10.1109\/QEST.2005.2"},{"key":"350_CR25","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Computer Performance Evaluation: Modelling Techniques and Tools, pp. 113\u2013140. LNCS Volume 2324, Springer (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"350_CR26","doi-asserted-by":"crossref","unstructured":"Lai, T.L.: Nearly optimal sequential tests of composite hypotheses. Ann. Stat. pp. 856\u2013886 (1988)","DOI":"10.1214\/aos\/1176350840"},{"key":"350_CR27","doi-asserted-by":"crossref","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Runtime Verification, pp. 122\u2013135. Springer (2010)","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"350_CR28","unstructured":"Matthes, K.: Zur Theorie der Bedienungsprozesse. In: Proceedings of the Third Prague Conference on Information Theory, Statistical Decision Functions and Random Processes, pp. 513\u2013528. Publishing House of the Czechoslovak Academy of Sciences (1962)"},{"key":"350_CR29","unstructured":"Reijsbergen, D.: Efficient simulation techniques for stochastic model checking. PhD thesis, University of Twente, Enschede (2013)"},{"key":"350_CR30","unstructured":"Reijsbergen, D., de Boer, P.T., Scheinhardt, W.: A sequential hypothesis test based on a generalized azuma inequality. Forthcoming"},{"key":"350_CR31","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316726","volume-title":"Stochastic Simulation","author":"BD Ripley","year":"1987","unstructured":"Ripley, B.D.: Stochastic Simulation. Wiley, Hoboken (1987)"},{"key":"350_CR32","volume-title":"Stochastic Processes","author":"SM Ross","year":"1996","unstructured":"Ross, S.M.: Stochastic Processes. Wiley, Hoboken (1996)"},{"key":"350_CR33","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: Statistical model checking for discrete event simulators. In: Proceedings of the 7th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS) (2013)"},{"key":"350_CR34","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Computer Aided Verification, pp. 202\u2013215. LNCS Volume 3114, Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"350_CR35","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Computer Aided Verification, pp. 266\u2013280. LNCS Volume 3576, Springer (2005)","DOI":"10.1007\/11513988_26"},{"key":"350_CR36","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 Second International Conference on the Quantitative Evaluation of Systems (QEST), pp. 251\u2013252. IEEE (2005)","DOI":"10.1109\/QEST.2005.42"},{"issue":"2","key":"350_CR37","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"key":"350_CR38","unstructured":"Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. PhD thesis, Carnegie Mellon (2005)"},{"key":"350_CR39","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S.: Error control for probabilistic model checking. In Verification, Model Checking, and Abstract Interpretation, pp. 142\u2013156. Springer (2006)","DOI":"10.1007\/11609773_10"},{"key":"350_CR40","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Clarke, E., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. Formal Methods: Foundations and Applications, pp. 144\u2013160 (2011)","DOI":"10.1007\/978-3-642-19829-8_10"},{"issue":"3","key":"350_CR41","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., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transf. (STTT) 8(3), 216\u2013228 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"350_CR42","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Computer Aided Verification, pp. 223\u2013235. LNCS Volume 2404, Springer (2002)","DOI":"10.1007\/3-540-45657-0_17"},{"issue":"9","key":"350_CR43","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. Inform. Comput. 204(9), 1368\u20131409 (2006)","journal-title":"Inform. Comput."}],"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-014-0350-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0350-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0350-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T22:49:48Z","timestamp":1746398988000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0350-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,1]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["350"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0350-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,10,1]]}}}