{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T16:41:33Z","timestamp":1777135293796,"version":"3.51.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2023,6,12]],"date-time":"2023-06-12T00:00:00Z","timestamp":1686528000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,6,12]],"date-time":"2023-06-12T00:00:00Z","timestamp":1686528000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"SUPSI - University of Applied Sciences and Arts of Southern Switzerland"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["SN COMPUT. SCI."],"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Standard techniques for model checking stochastic multi-agent systems usually assume the transition probabilities describing the system dynamics to be <jats:italic>stationary<\/jats:italic> and <jats:italic>completely specified<\/jats:italic>. As a consequence, neither non-stationary systems nor systems whose stochastic behaviour is partially unknown can be treated. So far, most of the approaches proposed to overcome this limitation suffer from complexity issues making them poorly efficient in the case of large state spaces. A fruitful but poorly explored way out is offered by the formalism of <jats:italic>imprecise probabilities<\/jats:italic> and the related <jats:italic>imprecise Markov models<\/jats:italic>. The aim of this paper is to show how imprecise probabilities can be fruitfully involved to model-check multi-agent systems characterised by non-stationary behaviours. Specifically, the paper introduces a new class of multi-agent models called <jats:italic>Imprecise Probabilistic Interpreted Systems<\/jats:italic> and their relative extensions with rewards. It also introduces a proper logical language to specify properties of such models and corresponding model checking algorithms based on iterative procedures to compute probabilistic and epistemic inferences over imprecise Markov models.<\/jats:p>","DOI":"10.1007\/s42979-023-01817-x","type":"journal-article","created":{"date-parts":[[2023,6,12]],"date-time":"2023-06-12T16:01:55Z","timestamp":1686585715000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Imprecise Probabilistic Model Checking for Stochastic Multi-agent Systems"],"prefix":"10.1007","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5993-0948","authenticated-orcid":false,"given":"Alberto","family":"Termine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Antonucci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Primiero","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Facchini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,6,12]]},"reference":[{"key":"1817_CR1","doi-asserted-by":"publisher","DOI":"10.1201\/9781315273600","volume-title":"Introduction to stochastic processes","author":"GF Lawler","year":"2018","unstructured":"Lawler GF. Introduction to stochastic processes. London: Chapman and Hall\/CRC; 2018."},{"key":"1817_CR2","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP. Principles of model checking. Cambridge: MIT Press; 2008."},{"key":"1817_CR3","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.05.004","author":"M Huang","year":"2019","unstructured":"Huang M, Fu H, Katoen J. Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems. Inf Comput. 2019. https:\/\/doi.org\/10.1016\/j.ic.2019.05.004.","journal-title":"Inf Comput"},{"key":"1817_CR4","unstructured":"Hillston J. A compositional approach to performance modelling. PhD thesis, University of Edinburgh, UK, Edinburgh, UK. 1994. https:\/\/hdl.handle.net\/1842\/15027. Accessed 01 Mar 2016."},{"key":"1817_CR5","doi-asserted-by":"publisher","unstructured":"Hillston J, Marin A, Rossi S, Piazza C. Contextual lumpability. In: Horv\u00e1th A, Buchholz P, Cortellessa V, Muscariello L, Squillante MS. editors. 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools \u201913, Torino, Italy, December 10-12, 2013; pp. 194\u2013203. ICST\/ACM, New York, USA (2013). https:\/\/doi.org\/10.4108\/icst.valuetools.2013.254408.","DOI":"10.4108\/icst.valuetools.2013.254408"},{"issue":"5","key":"1817_CR6","doi-asserted-by":"publisher","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 Comput. 1994;6(5):512\u201335.","journal-title":"Formal Aspects Comput"},{"key":"1817_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and software verification","author":"B B\u00e9rard","year":"2001","unstructured":"B\u00e9rard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P, McKenzie P. Systems and software verification. Cham: Model-Checking Techniques and Tools. Springer; 2001."},{"key":"1817_CR8","doi-asserted-by":"publisher","unstructured":"Bentahar J, Moulin B, Meyer JC. A new model checking approach for verifying agent communication protocols. In: Proceedings of the Canadian Conference on Electrical and Computer Engineering, CCECE 2006, May 7\u201310, 2006, Ottawa Congress Centre, Ottawa, Canada, 2006; pp. 1586\u20131590. IEEE, Ottawa. https:\/\/doi.org\/10.1109\/CCECE.2006.277640.","DOI":"10.1109\/CCECE.2006.277640"},{"key":"1817_CR9","doi-asserted-by":"publisher","unstructured":"Gallina L, Hamadou S, Marin A, Rossi S. A probabilistic energy-aware model for mobile ad-hoc networks. In: Al-Begain K, Balsamo S, Fiems D, Marin A. editors. Analytical and stochastic modeling techniques and applications\u201418th International Conference, ASMTA 2011, Venice, Italy, June 20-22, 2011. Proceedings. Lecture Notes in Computer Science, 2011; vol. 6751, pp. 316\u2013330. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-642-21713-5_23.","DOI":"10.1007\/978-3-642-21713-5_23"},{"issue":"2","key":"1817_CR10","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s11235-015-0122-6","volume":"63","author":"L Gallina","year":"2016","unstructured":"Gallina L, Marin A, Rossi S. Connectivity and energy-aware preorders for mobile ad-hoc networks. Telecommun Syst. 2016;63(2):307\u201333. https:\/\/doi.org\/10.1007\/s11235-015-0122-6.","journal-title":"Telecommun Syst"},{"key":"1817_CR11","doi-asserted-by":"publisher","unstructured":"Rossi, S. Model checking adaptive multilevel service compositions. In: Barbosa LS, Lumpe M. editors. Formal Aspects of Component Software\u20147th International Workshop, FACS 2010, Guimar\u00e3es, Portugal, October 14-16, 2010, Revised Selected Papers. Lecture Notes in Computer Science, 2010; vol. 6921, pp. 106\u2013124. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-642-27269-1_7.","DOI":"10.1007\/978-3-642-27269-1_7"},{"key":"1817_CR12","doi-asserted-by":"publisher","unstructured":"Bernardi G, Bugliesi M, Macedonio D, Rossi S. A theory of adaptable contract-based service composition. In: Negru V, Jebelean T, Petcu D, Zaharie D. editors. SYNASC 2008, 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, 26\u201329 September 2008, pp. 327\u2013334. IEEE Computer Society, New York, USA, 2008. https:\/\/doi.org\/10.1109\/SYNASC.2008.38.","DOI":"10.1109\/SYNASC.2008.38"},{"key":"1817_CR13","doi-asserted-by":"publisher","unstructured":"Bugliesi M, Macedonio D, Pino L, Rossi S. Compliance preorders for web services. In: Laneve C, Su J. editors. Web Services and Formal Methods, 6th International Workshop, WS-FM 2009, Bologna, Italy, September 4\u20135, 2009, Revised Selected Papers. Lecture Notes in Computer Science, 2009; vol. 6194, pp. 76\u201391. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-642-14458-5_5.","DOI":"10.1007\/978-3-642-14458-5_5"},{"key":"1817_CR14","doi-asserted-by":"crossref","unstructured":"Brim L, Ceska M, Safr\u00e1nek D. Model checking of biological systems. In: Bernardo M, de Vink EP, Pierro AD, Wiklicky H. editors. Formal methods for dynamical systems\u201413th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2013, Bertinoro, Italy, June 17\u201322, 2013. Advanced Lectures. Lecture Notes in Computer Science, 2013; vol. 7938, pp. 63\u2013112. Springer, Cham.","DOI":"10.1007\/978-3-642-38874-3_3"},{"key":"1817_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-17297-8_1","volume-title":"Automated reasoning for systems biology and medicine. Computational biology","author":"N Benes","year":"2019","unstructured":"Benes N, Brim L, Pastva S, Safr\u00e1nek D. Model checking approach to the analysis of biological systems. In: Li\u00f2 P, Zuliani P, editors. Automated reasoning for systems biology and medicine. Computational biology, vol. 30. Cham: Springer; 2019. p. 3\u201335."},{"key":"1817_CR16","volume-title":"Handbook of epistemic logic","year":"2015","unstructured":"van Ditmarsch H, van der Hoek W, Halpern J, Kooi B, editors. Handbook of epistemic logic. London: College Publications; 2015."},{"issue":"4","key":"1817_CR17","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/s11225-015-9621-4","volume":"104","author":"T Chen","year":"2016","unstructured":"Chen T, Primiero G, Raimondi F, Rungta N. A computationally grounded, weighted doxastic logic. Stud Log. 2016;104(4):679\u2013703.","journal-title":"Stud Log"},{"key":"1817_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/j.knosys.2013.06.017","volume":"50","author":"W Wan","year":"2013","unstructured":"Wan W, Bentahar J, Hamza AB. Model checking epistemic-probabilistic logic using probabilistic interpreted systems. Knowl Based Syst. 2013;50:279\u201395. https:\/\/doi.org\/10.1016\/j.knosys.2013.06.017.","journal-title":"Knowl Based Syst"},{"key":"1817_CR19","unstructured":"Daws C. Symbolic and parametric model checking of discrete-time Markov chains. In: Zhiming L, Araki K, editors. Theoretical aspects of computing\u2014ICTAC 2004, First International Colloquium, Guiyang, China, September 20\u201324, 2004, Revised Selected Papers, vol. 3407. Lecture Notes in Computer Science. Cham: Springer; 2004. p. 280\u201394."},{"key":"1817_CR20","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.104504","volume":"272","author":"C Baier","year":"2020","unstructured":"Baier C, Hensel C, Hutschenreiter L, Junges S, Katoen JP, Klein J. Parametric Markov chains: PCTL complexity and fraction-free gaussian elimination. Inf Comput. 2020;272: 104504. https:\/\/doi.org\/10.1016\/j.ic.2019.104504.","journal-title":"Inf Comput"},{"key":"1817_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-3472-7","volume-title":"Statistical reasoning with imprecise probabilities","author":"P Walley","year":"1991","unstructured":"Walley P. Statistical reasoning with imprecise probabilities. New York: Chapman and Hall; 1991."},{"key":"1817_CR22","unstructured":"Troffaes MCM, Skulj D. Model checking for imprecise markov chains. In: Cozman F, Denoeux T, Destercke S, Seidenfeld T. editors. ISIPTA \u201913 : Proceedings of the Eighth International Symposium on Imprecise Probability : Theories and Applications July 2\u20135 2013, Compi\u00e8gne, France., pp. 337\u2013344. Society for Imprecise Probability: Theories and Applications (SIPTA), Compi\u00e8gne. 2013."},{"key":"1817_CR23","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1016\/j.artint.2015.09.005","volume":"230","author":"KV Delgado","year":"2016","unstructured":"Delgado KV, De Barros LN, Dias DB, Sanner S. Real-time dynamic programming for Markov decision processes with imprecise probabilities. Artif Intell. 2016;230:192\u2013223.","journal-title":"Artif Intell"},{"key":"1817_CR24","unstructured":"Krak TE, T\u2019Joens N, Bock JD. Hitting times and probabilities for imprecise markov chains. In: Bock JD, de Campos CP, de Cooman G, Quaeghebeur E, Wheeler GR, editors. International Symposium on Imprecise Probabilities: Theories and Applications, ISIPTA 2019, 3\u20136 July 2019, Thagaste, Ghent, Belgium, vol. 103. Proceedings of Machine Learning Research. Ghent: PMLR; 2019. p. 265\u201375."},{"key":"1817_CR25","unstructured":"Termine A, Antonucci A, Facchini A, Primiero G. Robust model checking with imprecise Markov reward models. In: International Symposium on imprecise probabilities: theories and applications, ISIPTA 2021, July 6\u20139 2021, Granada, Spain. Proceedings of Machine Learning Research. PMLR, Granada; 2021."},{"key":"1817_CR26","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1016\/j.ijar.2016.04.009","volume":"76","author":"G De Cooman","year":"2016","unstructured":"De Cooman G, De Bock J, Lopatatzidis S. Imprecise stochastic processes in discrete time: global models, imprecise Markov chains and ergodic theorems. Int J Approx Reason. 2016;76:18\u201346.","journal-title":"Int J Approx Reason"},{"key":"1817_CR27","doi-asserted-by":"crossref","unstructured":"T\u2019Joens N, Krak TE, De Bock J, De Cooman G. A recursive algorithm for computing inferences in imprecise markov chains. In: Kern-Isberner G, Ognjanovic Z, editors. Symbolic and Quantitative Approaches to Reasoning with Uncertainty, 15th European Conference, ECSQARU 2019, Belgrade, Serbia, September 18\u201320, 2019, Proceedings, vol. 11726. Lecture Notes in Computer Science. Cham: Springer; 2019. p. 455\u201365.","DOI":"10.1007\/978-3-030-29765-7_38"},{"key":"1817_CR28","doi-asserted-by":"crossref","unstructured":"Termine A, Antonucci A, Primiero G, Facchini A. Logic and model checking by imprecise probabilistic interpreted systems. In: European Conference on multi-agent systems, 2021; pp. 211\u2013227. Springer.","DOI":"10.1007\/978-3-030-82254-5_13"},{"key":"1817_CR29","volume-title":"Markov chains","author":"JR Norris","year":"1998","unstructured":"Norris JR. Markov chains, vol. 2. Cambridge University Press; 1998."},{"key":"1817_CR30","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1613\/jair.4355","volume":"50","author":"DD Mau\u00e1","year":"2014","unstructured":"Mau\u00e1 DD, de Campos CP, Benavoli A, Antonucci A. Probabilistic inference in Credal networks: New complexity results. J Artif Intell Res. 2014;50:603\u201337.","journal-title":"J Artif Intell Res"},{"key":"1817_CR31","volume-title":"Probability and finance: it\u2019s only a game!","author":"G Shafer","year":"2005","unstructured":"Shafer G, Vovk V. Probability and finance: it\u2019s only a game!, vol. 491. London: Wiley; 2005."},{"key":"1817_CR32","unstructured":"T\u2019Joens N, De\u00a0Bock J. Global upper expectations for discrete-time stochastic processes: in practice, they are all the same! In: International Symposium on imprecise probability: theories and applications, 2021; p. 310\u2013319. PMLR."},{"issue":"4","key":"1817_CR33","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1017\/S0269964809990039","volume":"23","author":"G De Cooman","year":"2009","unstructured":"De Cooman G, Hermans F, Quaeghebeur E. Imprecise Markov chains and their limit behavior. Probab Eng Inf Sci. 2009;23(4):597\u2013635.","journal-title":"Probab Eng Inf Sci"},{"issue":"11","key":"1817_CR34","doi-asserted-by":"publisher","first-page":"1400","DOI":"10.1016\/j.artint.2008.03.001","volume":"172","author":"G De Cooman","year":"2008","unstructured":"De Cooman G, Hermans F. Imprecise probability trees: bridging two theories of imprecise probability. Artif Intell. 2008;172(11):1400\u201327.","journal-title":"Artif Intell"},{"key":"1817_CR35","doi-asserted-by":"crossref","unstructured":"Destercke S, Cooman Gd. Relating epistemic irrelevance to event trees. In: Soft methods for handling variability and imprecision. Cham: Springer, Cham; 2008, , p. 66\u201373.","DOI":"10.1007\/978-3-540-85027-4_9"},{"key":"1817_CR36","doi-asserted-by":"crossref","unstructured":"Hermans F, \u0160kulj D. Stochastic processes. In: Augustin T., Coolen FPA, De Cooman G, and Troffaes MCM, editors. Introduction to imprecise probabilities. London: Wiley, 2014; p. 258\u201378.","DOI":"10.1002\/9781118763117.ch11"},{"key":"1817_CR37","doi-asserted-by":"crossref","unstructured":"Miranda E, De Cooman G. Structural judgements. In: Augustin T., Coolen F.P.A., De Cooman G., and Troffaes M.C.M. Introduction to imprecise probabilities. London: Wiley, Introduction to imprecise probabilities, 2014; p. 56\u201378.","DOI":"10.1002\/9781118763117.ch3"},{"key":"1817_CR38","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1016\/j.ijar.2017.06.012","volume":"88","author":"T Krak","year":"2017","unstructured":"Krak T, De Bock J, Siebes A. Imprecise continuous-time Markov chains. Int J Approx Reason. 2017;88:452\u2013528.","journal-title":"Int J Approx Reason"},{"key":"1817_CR39","unstructured":"Antonucci A, Huber D, Zaffalon M, Luginb\u00fchl P, Chapman I, Ladouceur R. Credo: a military decision-support system based on Credal networks. In: Proceedings of the 16th Conference on Information Fusion (FUSION 2013), Istanbul, Turkey; 2013."},{"key":"1817_CR40","doi-asserted-by":"crossref","unstructured":"Lomuscio A, Raimondi F. MCMAS: a model checker for multi-agent systems. In: Hermanns H, Palsberg J, editors. Tools and algorithms for the construction and analysis of systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25\u2013April 2, 2006, Proceedings, vol. 3920. Lecture Notes in Computer Science. Cham: Springer; 2006. p. 450\u20134.","DOI":"10.1007\/11691372_31"},{"issue":"10","key":"1817_CR41","doi-asserted-by":"publisher","first-page":"1021","DOI":"10.1057\/palgrave.jors.2600619","volume":"49","author":"SI McClean","year":"1998","unstructured":"McClean SI, McAlea B, Millard PH. Using a Markov reward model to estimate spend-down costs for a geriatric department. J Oper Res Soc. 1998;49(10):1021\u20135.","journal-title":"J Oper Res Soc"},{"key":"1817_CR42","doi-asserted-by":"crossref","unstructured":"Cardelli L, Grosu R, Larsen KG, Tribastone M, Tschaikowski M, Vandin A. Lumpability for uncertain continuous-time markov chains. In: International Conference on quantitative evaluation of systems, Cham, 2021; p. 391\u2013409. Springer.","DOI":"10.1007\/978-3-030-85172-9_21"},{"key":"1817_CR43","volume-title":"Reinforcement learning\u2014an introduction. Adaptive computation and machine learning","author":"RS Sutton","year":"1998","unstructured":"Sutton RS, Barto AG. Reinforcement learning\u2014an introduction. Adaptive computation and machine learning. Cambridge: MIT Press; 1998."}],"container-title":["SN Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-023-01817-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s42979-023-01817-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-023-01817-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,12]],"date-time":"2023-06-12T16:29:42Z","timestamp":1686587382000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s42979-023-01817-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,12]]},"references-count":43,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2023,9]]}},"alternative-id":["1817"],"URL":"https:\/\/doi.org\/10.1007\/s42979-023-01817-x","relation":{},"ISSN":["2661-8907"],"issn-type":[{"value":"2661-8907","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,12]]},"assertion":[{"value":"4 February 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 March 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 June 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"On behalf of all the authors, the corresponding author states that there is no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"443"}}