{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T14:37:46Z","timestamp":1777559866308,"version":"3.51.4"},"reference-count":23,"publisher":"SAGE Publications","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2016,3,2]]},"DOI":"10.3233\/aic-150689","type":"journal-article","created":{"date-parts":[[2016,3,4]],"date-time":"2016-03-04T09:37:31Z","timestamp":1457084251000},"page":"287-299","source":"Crossref","is-referenced-by-count":6,"title":["Evaluating probabilistic model checking tools for verification of robot control policies"],"prefix":"10.1177","volume":"29","author":[{"given":"Shashank","family":"Pathak","sequence":"first","affiliation":[{"name":"iCub Facility, Istituto Italiano di Tecnologia, Genova, Italy. E-mail:\u00a0Shashank.Pathak@iit.it"},{"name":"DIBRIS, Universit\u00e0 degli Studi di Genova, Genova, Italy. E-mail:\u00a0armando.tacchella@unige.it"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Pulina","sequence":"additional","affiliation":[{"name":"POLCOMING, Universit\u00e0 degli Studi di Sassari, Sassari, Italy. E-mail:\u00a0lpulina@uniss.it"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[{"name":"DIBRIS, Universit\u00e0 degli Studi di Genova, Genova, Italy. E-mail:\u00a0armando.tacchella@unige.it"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","reference":[{"key":"10.3233\/AIC-150689_ref1","doi-asserted-by":"crossref","unstructured":"[1]E.\u00a0Abrah\u00e1m, N.\u00a0Jansen, R.\u00a0Wimmer, J.\u00a0Katoen and B.\u00a0Becker, DTMC model checking by SCC reduction, in: Seventh International Conference on the Quantitative Evaluation of Systems (QEST) 2010, IEEE, 2010, pp.\u00a037\u201346.","DOI":"10.1109\/QEST.2010.13"},{"key":"10.3233\/AIC-150689_ref2","doi-asserted-by":"crossref","unstructured":"[2]A.\u00a0Aziz, V.\u00a0Singhal, F.\u00a0Balarin, R.K.\u00a0Brayton and A.L. Sangiovanni-Vincentelli, It usually works: The temporal logic of stochastic systems, in: Computer Aided Verification, Springer, 1995, pp.\u00a0155\u2013165.","DOI":"10.1007\/3-540-60045-0_48"},{"issue":"2","key":"10.3233\/AIC-150689_ref3","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1177\/0278364907088064","article-title":"Editorial: Special issue on machine learning in robotics","volume":"27","author":"Bagnell","year":"2008","journal-title":"The International Journal of Robotics Research"},{"issue":"2","key":"10.3233\/AIC-150689_ref4","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/s10703-013-0194-4","article-title":"Preface to the special issue on probabilistic model checking","volume":"43","author":"Baier","year":"2013","journal-title":"Formal Methods in System Design"},{"key":"10.3233\/AIC-150689_ref5","unstructured":"[5]M.\u00a0Bozzano, A.\u00a0Cimatti, M.\u00a0Roveri and A.\u00a0Tchaltsev, A comprehensive approach to on-board autonomy verification and validation, in: Proceedings of the 22nd International Joint Conference on Artificial Intelligence, IJCAI 2011, Barcelona, Catalonia, Spain, 16\u201322 July 2011, 2011, pp.\u00a02398\u20132403."},{"key":"10.3233\/AIC-150689_ref6","doi-asserted-by":"crossref","unstructured":"[6]G.\u00a0Cicala, A.\u00a0Khalili, G.\u00a0Metta, L.\u00a0Natale, S.\u00a0Pathak, L.\u00a0Pulina and A.\u00a0Tacchella, Engineering approaches and methods to verify software in autonomous systems, in: 13th International Conference on Intelligent Autonomous Systems, Advances in Intelligent Systems and Computing, Springer, 2014.","DOI":"10.1007\/978-3-319-08338-4_121"},{"issue":"5","key":"10.3233\/AIC-150689_ref7","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","article-title":"A logic for reasoning about time and reliability","volume":"6","author":"Hansson","year":"1994","journal-title":"Formal Aspects of Computing"},{"key":"10.3233\/AIC-150689_ref8","doi-asserted-by":"crossref","unstructured":"[8]N.\u00a0Jansen, E.\u00a0\u00c1brah\u00e1m, M.\u00a0Volk, R.\u00a0Wimmer, J.-P.\u00a0Katoen and B.\u00a0Becker, The COMICS tool\u00a0\u2013 Computing minimal counterexamples for DTMCs, in: Automated Technology for Verification and Analysis, Springer, 2012, pp.\u00a0349\u2013353.","DOI":"10.1007\/978-3-642-33386-6_27"},{"issue":"2","key":"10.3233\/AIC-150689_ref9","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","article-title":"The ins and outs of the probabilistic model checker MRMC","volume":"68","author":"Katoen","year":"2011","journal-title":"Performance Evaluation"},{"key":"10.3233\/AIC-150689_ref10","doi-asserted-by":"crossref","unstructured":"[10]M.\u00a0Kwiatkowska, G.\u00a0Norman and D.\u00a0Parker, PRISM: Probabilistic symbolic model checker, in: Computer Performance Evaluation: Modelling Techniques and Tools, 2002, pp.\u00a0113\u2013140.","DOI":"10.1007\/3-540-46029-2_13"},{"key":"10.3233\/AIC-150689_ref11","doi-asserted-by":"crossref","unstructured":"[11]M.\u00a0Kwiatkowska, G.\u00a0Norman and D.\u00a0Parker, Stochastic model checking, in: Formal Methods for Performance Evaluation, 2007, pp.\u00a0220\u2013270.","DOI":"10.1007\/978-3-540-72522-0_6"},{"issue":"4","key":"10.3233\/AIC-150689_ref12","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/1364644.1364651","article-title":"Using probabilistic model checking in systems biology","volume":"35","author":"Kwiatkowska","year":"2008","journal-title":"ACM SIGMETRICS Performance Evaluation Review"},{"key":"10.3233\/AIC-150689_ref13","doi-asserted-by":"crossref","unstructured":"[13]M.\u00a0Kwiatkowska, G.\u00a0Norman and D.\u00a0Parker, PRISM 4.0: Verification of probabilistic real-time systems, in: Computer Aided Verification, Springer, 2011, pp.\u00a0585\u2013591.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"10.3233\/AIC-150689_ref14","doi-asserted-by":"crossref","unstructured":"[14]M.\u00a0Kwiatkowska, G.\u00a0Norman and J.\u00a0Sproston, Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol, Springer, 2002.","DOI":"10.1007\/3-540-45605-8_11"},{"issue":"8,9","key":"10.3233\/AIC-150689_ref15","doi-asserted-by":"crossref","first-page":"1125","DOI":"10.1016\/j.neunet.2010.08.010","article-title":"The iCub humanoid robot: An open-systems platform for research in cognitive development","volume":"23","author":"Metta","year":"2010","journal-title":"Neural Networks: The Official Journal of the International Neural Network Society"},{"key":"10.3233\/AIC-150689_ref16","doi-asserted-by":"crossref","unstructured":"[16]S.\u00a0Pathak, E.\u00a0\u00c1brah\u00e1m, N.\u00a0Jansen, A.\u00a0Tacchella and J.-P.\u00a0Katoen, A greedy approach for the efficient repair of stochastic models, in: NASA Formal Methods, Springer International Publishing, 2015, pp.\u00a0295\u2013309.","DOI":"10.1007\/978-3-319-17524-9_21"},{"key":"10.3233\/AIC-150689_ref17","doi-asserted-by":"crossref","unstructured":"[17]S.\u00a0Pathak, L.\u00a0Pulina, G.\u00a0Metta and A.\u00a0Tacchella, Ensuring safety of policies learned by reinforcement: Reaching objects in the presence of obstacles with the iCub, in: IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS) 2013, IEEE, 2013, pp.\u00a0170\u2013175.","DOI":"10.1109\/IROS.2013.6696349"},{"key":"10.3233\/AIC-150689_ref18","doi-asserted-by":"crossref","unstructured":"[18]S.\u00a0Pathak, L.\u00a0Pulina and A.\u00a0Tacchella, Learning, verification and repair for safe human\u2013robot interaction, in: 14th Conference of the Italian Association for Artificial Intelligence (AI*IA 2015), Lecture Notes in Computer Science, Springer, 2015.","DOI":"10.1007\/978-3-319-24309-2_20"},{"key":"10.3233\/AIC-150689_ref19","unstructured":"[19]M.L.\u00a0Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Vol.\u00a0414, John Wiley & Sons, 2009."},{"key":"10.3233\/AIC-150689_ref20","doi-asserted-by":"crossref","unstructured":"[20]R.S.\u00a0Sutton and A.G.\u00a0Barto, Reinforcement Learning\u00a0\u2013 An Introduction, MIT Press, 1998.","DOI":"10.1109\/TNN.1998.712192"},{"key":"10.3233\/AIC-150689_ref21","doi-asserted-by":"crossref","unstructured":"[21]M.Y.\u00a0Vardi, Automatic verification of probabilistic concurrent finite-state programs, in: FOCS, 1985, pp.\u00a0327\u2013338.","DOI":"10.1109\/SFCS.1985.12"},{"issue":"3,4","key":"10.3233\/AIC-150689_ref22","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BF00992698","article-title":"Q-learning","volume":"8","author":"Watkins","year":"1992","journal-title":"Machine Learning"},{"key":"10.3233\/AIC-150689_ref23","doi-asserted-by":"crossref","unstructured":"[23]M.\u00a0Wiering and M.\u00a0Van Otterlo, Reinforcement Learning, Adaptation, Learning, and Optimization, Vol.\u00a012, Springer, 2012.","DOI":"10.1007\/978-3-642-27645-3"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-150689","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T18:27:24Z","timestamp":1777400844000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-150689"}},"subtitle":[],"editor":[{"given":"Toni","family":"Mancini","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"Marco","family":"Maratea","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"Francesco","family":"Ricca","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2016,3,2]]},"references-count":23,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.3233\/aic-150689","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"value":"1875-8452","type":"electronic"},{"value":"0921-7126","type":"print"}],"subject":[],"published":{"date-parts":[[2016,3,2]]}}}