{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T12:07:49Z","timestamp":1763726869803},"reference-count":41,"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-0349-7","type":"journal-article","created":{"date-parts":[[2014,9,30]],"date-time":"2014-09-30T08:38:32Z","timestamp":1412066312000},"page":"429-456","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Sound statistical model checking for MDP using partial order and confluence reduction"],"prefix":"10.1007","volume":"17","author":[{"given":"Arnd","family":"Hartmanns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Timmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,1]]},"reference":[{"issue":"2","key":"349_CR1","first-page":"119","volume":"52","author":"A Agresti","year":"1998","unstructured":"Agresti, A., Coull, B.A.: Approximate is better than \u201cexact\u201d for interval estimation of binomial proportions. Am. Stat. 52(2), 119\u2013126 (1998)","journal-title":"Am. Stat."},{"issue":"7","key":"349_CR2","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1109\/MC.2006.242","volume":"39","author":"TR Andel","year":"2006","unstructured":"Andel, T.R., Yasinsac, A.: On the credibility of MANET simulations. IEEE Comput. 39(7), 48\u201354 (2006)","journal-title":"IEEE Comput."},{"issue":"2","key":"349_CR3","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/j.entcs.2005.10.034","volume":"153","author":"C Baier","year":"2006","unstructured":"Baier, C., D\u2019Argenio, P.R., Gr\u00f6\u00dfer, M.: Partial order reduction for probabilistic branching time. Electron. Notes Theor. Comput. Sci. 153(2), 97\u2013116 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"349_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Ciesinski, F.: Partial order reduction for probabilistic systems. In: QEST, pp. 230\u2013239. IEEE Computer Society, New York (2004)","DOI":"10.1109\/QEST.2004.1348037"},{"key":"349_CR5","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":"349_CR6","unstructured":"Blom, S.: Partial $$\\tau $$ \u03c4 -confluence for efficient state space generation. Technical Report SEN-R0123, CWI (2001)"},{"key":"349_CR7","doi-asserted-by":"crossref","unstructured":"Blom, S., van de Pol, J.: State space reduction by proving confluence. In: Brinksma, E., Larsen, K.G. (eds.) CAV. Lecture Notes in Computer Science, vol. 2404, pp. 596\u2013609. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_50"},{"key":"349_CR8","doi-asserted-by":"crossref","unstructured":"Bogdoll, J., Fioriti, L.M.F., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE. Lecture Notes in Computer Science, vol. 6722, pp. 59\u201374. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-21461-5_4"},{"key":"349_CR9","doi-asserted-by":"crossref","unstructured":"Bogdoll, J., Hartmanns, A., Hermanns, H.: Simulation and statistical model checking for modestly nondeterministic models. In: Schmitt, J.B. (ed.) MMB\/DFT. Lecture Notes in Computer Science, vol. 7201, pp. 249\u2013252. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28540-0_20"},{"key":"349_CR10","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kret\u00ednsk\u00fd, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. CoRR, abs\/1402.2967 (2014)","DOI":"10.1007\/978-3-319-11936-6_8"},{"issue":"1","key":"349_CR11","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D Chaum","year":"1988","unstructured":"Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptol. 1(1), 65\u201375 (1988)","journal-title":"J. Cryptol."},{"key":"349_CR12","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P.R., Niebert, P.: Partial order reduction on concurrent probabilistic programs. In: QEST, pp. 240\u2013249. IEEE Computer Society, New York (2004)","DOI":"10.1109\/QEST.2004.1348038"},{"issue":"2","key":"349_CR13","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/s10009-010-0137-y","volume":"12","author":"S Evangelista","year":"2010","unstructured":"Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. STTT 12(2), 155\u2013170 (2010)","journal-title":"STTT"},{"key":"349_CR14","doi-asserted-by":"crossref","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM. Lecture Notes in Computer Science, vol. 6659, pp. 53\u2013113. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"349_CR15","doi-asserted-by":"crossref","unstructured":"Giro, S., D\u2019Argenio, P.R., Fioriti, L.M.F.: Partial order reduction for probabilistic systems: a revision for distributed schedulers. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR. Lecture Notes in Computer Science, vol. 5710, pp. 338\u2013353. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04081-8_23"},{"key":"349_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems\u2014an approach to the state-explosion problem. Lecture Notes in Computer Science, vol. 1032. Springer, Berlin (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"349_CR17","doi-asserted-by":"crossref","unstructured":"Groote, J.F., van de Pol, J.: State space reduction using partial tau-confluence. In: Nielsen, M., Rovan, B. (eds.) MFCS. Lecture Notes in Computer Science, vol. 1893, pp. 383\u2013393. Springer, Berlin (2000)","DOI":"10.1007\/3-540-44612-5_34"},{"key":"349_CR18","doi-asserted-by":"crossref","unstructured":"Hansen, H., Kwiatkowska, M.Z., Qu, H.: Partial order reduction for model checking Markov decision processes under unconditional fairness. In: QEST, pp. 203\u2013212. IEEE Computer Society, New York (2011)","DOI":"10.1109\/QEST.2011.35"},{"key":"349_CR19","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.tcs.2013.07.014","volume":"538C","author":"H Hansen","year":"2014","unstructured":"Hansen, H., Timmer, M.: A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time. Theor. Comput. Sci. 538C, 103\u2013123 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"349_CR20","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: A modest approach to checking probabilistic timed automata. In: QEST, pp. 187\u2013196. IEEE Computer Society, New York (2009)","DOI":"10.1109\/QEST.2009.41"},{"key":"349_CR21","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS. Lecture Notes in Computer Science, vol. 8413, pp. 593\u2013598. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"349_CR22","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Timmer, M.: On-the-fly confluence detection for statistical model checking. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 7871, pp. 337\u2013351. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38088-4_23"},{"key":"349_CR23","doi-asserted-by":"crossref","unstructured":"Henriques, D., Martins, J., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: QEST, pp. 84\u201393. IEEE Computer Society, New York (2012)","DOI":"10.1109\/QEST.2012.19"},{"key":"349_CR24","doi-asserted-by":"crossref","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI. Lecture Notes in Computer Science, vol. 2937, pp. 73\u201384. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24622-0_8"},{"issue":"301","key":"349_CR25","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(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"349_CR26","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol. 6806, pp. 585\u2013591. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"349_CR27","doi-asserted-by":"crossref","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. In: Ossowski, S., Lecca, P. (eds.) SAC, pp. 1314\u20131319. ACM, New York (2012)","DOI":"10.1145\/2245276.2231984"},{"key":"349_CR28","doi-asserted-by":"crossref","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.) RV. Lecture Notes in Computer Science, vol. 6418, pp. 122\u2013135. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"349_CR29","unstructured":"Legay, A., Sedwards, S.: Lightweight Monte Carlo algorithm for Markov decision processes. CoRR, abs\/1310.3609 (2013)"},{"issue":"10\u201311","key":"349_CR30","doi-asserted-by":"crossref","first-page":"1075","DOI":"10.1016\/j.scico.2011.07.004","volume":"77","author":"R Mateescu","year":"2012","unstructured":"Mateescu, R., Wijs, A.: Sequential and distributed on-the-fly computation of weak tau-confluence. Sci. Comput. Program. 77(10\u201311), 1075\u20131094 (2012)","journal-title":"Sci. Comput. Program."},{"key":"349_CR31","unstructured":"Nimal, V.: Statistical approaches for probabilistic model checking. Master\u2019s thesis, Oxford University (2010)"},{"key":"349_CR32","doi-asserted-by":"crossref","unstructured":"Pace, G.J., Lang, F., Mateescu, R.: Calculating-confluence compositionally. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV. Lecture Notes in Computer Science, vol. 2725, pp. 446\u2013459. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_41"},{"key":"349_CR33","doi-asserted-by":"crossref","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV. Lecture Notes in Computer Science, vol. 818, pp. 377\u2013390. Springer, Berlin (1994)","DOI":"10.1007\/3-540-58179-0_69"},{"issue":"1","key":"349_CR34","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D Peled","year":"1996","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. Formal Methods Syst. Des. 8(1), 39\u201364 (1996)","journal-title":"Formal Methods Syst. Des."},{"key":"349_CR35","volume-title":"Simulation","author":"SM Ross","year":"2006","unstructured":"Ross, S.M.: Simulation, 4th edn. Elsevier Academic Press, Amsterdam (2006)","edition":"4"},{"key":"349_CR36","unstructured":"Timmer, M.: Efficient Modelling, Generation and Analysis of Markov Automata. PhD thesis, University of Twente, The Netherlands (2013)"},{"key":"349_CR37","doi-asserted-by":"crossref","unstructured":"Timmer, M., Stoelinga, M., van de Pol, J.: Confluence reduction for probabilistic systems. In: Abdulla, P.A., Rustan, K., Leino, M. (eds.) TACAS. Lecture Notes in Computer Science, vol. 6605, pp. 311\u2013325. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-19835-9_29"},{"key":"349_CR38","doi-asserted-by":"crossref","unstructured":"Timmer, M., van de Pol, J., Stoelinga, M.: Confluence reduction for Markov automata. In: Braberman, V.A., Fribourg, L. (eds.) FORMATS. Lecture Notes in Computer Science, vol. 8053, pp. 243\u2013257. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40229-6_17"},{"key":"349_CR39","doi-asserted-by":"crossref","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV. Lecture Notes in Computer Science, vol. 531, pp. 156\u2013165. Springer, Berlin (1990)","DOI":"10.1007\/BFb0023729"},{"issue":"3","key":"349_CR40","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. STTT 8(3), 216\u2013228 (2006)","journal-title":"STTT"},{"key":"349_CR41","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV. Lecture Notes in Computer Science, vol. 2404, pp. 223\u2013235. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_17"}],"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-0349-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0349-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0349-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,15]],"date-time":"2019-08-15T16:40:11Z","timestamp":1565887211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0349-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,1]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["349"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0349-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,1]]}}}