{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:23:53Z","timestamp":1777519433511,"version":"3.51.4"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,6,6]],"date-time":"2015-06-06T00:00:00Z","timestamp":1433548800000},"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-0383-0","type":"journal-article","created":{"date-parts":[[2015,6,5]],"date-time":"2015-06-05T00:57:23Z","timestamp":1433465843000},"page":"469-484","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":51,"title":["Smart sampling for lightweight verification of Markov decision processes"],"prefix":"10.1007","volume":"17","author":[{"given":"Pedro","family":"D\u2019Argenio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sean","family":"Sedwards","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louis-Marie","family":"Traonouez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,6]]},"reference":[{"key":"383_CR1","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"383_CR2","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)"},{"key":"383_CR3","doi-asserted-by":"crossref","unstructured":"Bianco, A., De Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Foundations of Software Technology and Theoretical Computer Science, pp. 499\u2013513. Springer, New York (1995)","DOI":"10.1007\/3-540-60692-0_70"},{"key":"383_CR4","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: Formal Techniques for Distributed Systems, pp. 59\u201374. Springer, New York (2011)","DOI":"10.1007\/978-3-642-21461-5_4"},{"key":"383_CR5","doi-asserted-by":"crossref","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) Quantitative Evaluation of Systems. LNCS, vol. 8054, pp. 160\u2013164. Springer, New York (2013)","DOI":"10.1007\/978-3-642-40196-1_12"},{"key":"383_CR6","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 8837, pp. 98\u2013114. Springer, New York (2014)","DOI":"10.1007\/978-3-319-11936-6_8"},{"issue":"11","key":"383_CR7","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"key":"383_CR8","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)"},{"key":"383_CR9","doi-asserted-by":"crossref","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout D.: Reasoning with temporal logic on truncated paths. In: Computer Aided Verification, pp. 27\u201339. Springer, New York (2003)","DOI":"10.1007\/978-3-540-45069-6_3"},{"issue":"2","key":"383_CR10","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/S1571-0661(04)00252-X","volume":"55","author":"MCW Geilen","year":"2001","unstructured":"Geilen, M.C.W.: On the construction of monitors for temporal logic properties. Electron. Notes Theor. Comput. Sci. 55(2), 181\u2013199 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"383_CR11","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification Testing and Verification, pp. 3\u201318. Chapman & Hall, London (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"383_CR12","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proceedings of 16th Annual International Conference on Automated Software Engineering (ASE\u201901), pp. 412\u2013416. IEEE (2001)","DOI":"10.1109\/ASE.2001.989841"},{"key":"383_CR13","doi-asserted-by":"crossref","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512\u2013535 (1994)","DOI":"10.1007\/BF01211866"},{"key":"383_CR14","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Timmer, M.: On-the-fly confluence detection for statistical model checking. In: NASA Formal Methods, pp. 337\u2013351. Springer, New York (2013)","DOI":"10.1007\/978-3-642-38088-4_23"},{"key":"383_CR15","doi-asserted-by":"crossref","unstructured":"Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke Edmund, M.: Statistical model checking for Markov decision processes. In: Ninth International Conference on Quantitative Evaluation of Systems, pp. 84\u201393. IEEE (2012)","DOI":"10.1109\/QEST.2012.19"},{"key":"383_CR16","doi-asserted-by":"crossref","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","DOI":"10.1080\/01621459.1963.10500830"},{"key":"383_CR17","doi-asserted-by":"crossref","unstructured":"Horner, W.G.: A new method of solving numerical equations of all orders, by continuous approximation. Philos. Trans. R. Soc. Lond. 109, 308\u2013335 (1819)","DOI":"10.1098\/rstl.1819.0023"},{"key":"383_CR18","doi-asserted-by":"crossref","unstructured":"Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizating mutual exclusion. In: Proceedings of 9th Annual ACM Symposium on Principles of Distributed Computing (PODC\u201990), pp. 119\u2013131. ACM, New York (1990)","DOI":"10.1145\/93385.93409"},{"key":"383_CR19","doi-asserted-by":"crossref","unstructured":"Kearns, M., Mansour, Y., Ng, A.Y.: A sparse sampling algorithm for near-optimal planning in large Markov decision processes. Mach. Learn. 49(2\u20133), 193\u2013208 (2002)","DOI":"10.1023\/A:1017932429737"},{"key":"383_CR20","unstructured":"Knuth, D.E.: The Art of Computer Programming, 3rd edn. Addison-Wesley, Menlo Park (1998)"},{"key":"383_CR21","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM\u201907). LNCS (Tutorial Volume), vol. 4486, pp. 220\u2013270. Springer, New York (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"383_CR22","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Analysis of a gossip protocol in PRISM. SIGMETRICS Perform. Eval. Rev. 36(3), 17\u201322 (2008)","DOI":"10.1145\/1481506.1481511"},{"key":"383_CR23","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design 29, 33\u201378 (2006)","DOI":"10.1007\/s10703-006-0005-2"},{"key":"383_CR24","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Vigliotti, M.G.: Probabilistic mobile ambients. Theor. Comput. Sci. 410(12\u201313), 1272\u20131303 (2009)","DOI":"10.1016\/j.tcs.2008.12.058"},{"key":"383_CR25","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Proceedings of $$2{\\rm {nd}}$$ 2 nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, pp. 169\u2013187. Springer, New York (2002)","DOI":"10.1007\/3-540-45605-8_11"},{"key":"383_CR26","doi-asserted-by":"crossref","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. In: Proceedings of $$27{\\rm th}$$ 27 th Annual ACM Symposium on Applied Computing, pp. 1314\u20131319. ACM, New York (2012)","DOI":"10.1145\/2245276.2231984"},{"key":"383_CR27","doi-asserted-by":"crossref","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of Markov decision processes. In: 4th Workshop on Formal Methods in the Development of Software (FMDS\u201914), LNCS. Springer, New York (2014)","DOI":"10.1007\/978-3-319-15201-1_23"},{"key":"383_CR28","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety, vol. 2. Springer, New York (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"383_CR29","doi-asserted-by":"crossref","unstructured":"Ndukwu, U., McIver, A.: An expectation transformer approach to predicate abstraction and data independence for probabilistic programs. In: Proceedings of 8th Workshop on Quantitative Aspects of Programming Languages (QAPL\u201910) (2010)","DOI":"10.4204\/EPTCS.28.9"},{"key":"383_CR30","doi-asserted-by":"crossref","unstructured":"Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10(1), 29\u201335 (1958)","DOI":"10.1007\/BF02883985"},{"key":"383_CR31","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley-Interscience, USA (1994)","DOI":"10.1002\/9780470316887"},{"key":"383_CR32","doi-asserted-by":"crossref","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat.16(2), 117\u2013186 (1945)","DOI":"10.1214\/aoms\/1177731118"},{"key":"383_CR33","doi-asserted-by":"crossref","unstructured":"White, D.J.: Real applications of Markov decision processes. Interfaces 15(6), 73\u201383 (1985)","DOI":"10.1287\/inte.15.6.73"},{"key":"383_CR34","doi-asserted-by":"crossref","unstructured":"White, D.J.: Further real applications of Markov decision processes. Interfaces 18(5), 55\u201361 (1988)","DOI":"10.1287\/inte.18.5.55"},{"key":"383_CR35","doi-asserted-by":"crossref","unstructured":"White, D.J.: A survey of applications of Markov decision processes. J. Oper. Res. Soc. 44(11), 1073\u20131096 (1993)","DOI":"10.1057\/jors.1993.181"},{"key":"383_CR36","unstructured":"Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. PhD thesis, Carnegie Mellon University, Pittsburgh (2005)"},{"key":"383_CR37","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. Springer, New York (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-015-0383-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0383-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0383-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,26]],"date-time":"2019-08-26T01:40:47Z","timestamp":1566783647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0383-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,6]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["383"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0383-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,6]]}}}