In many situations an agent's behaviour can sensibly be described only in terms of a distribution of probability over a set of possibilities. In such case (agents') decision-making becomes probabilistic too. In this work we consider a probabilistic variant of a well-known (two-players) Negotiation game and we show, first, how it can be encoded into a Markovian model, and then how a probabilistic model-checker such as PRISM can be used as a tool for its (automated) analysis. This paper is meant to exemplify that verification through model-checking can be fruitfully applied also to uncertain multi-agent systems. This, in our view, is the first step towards the characterisation of an automated verification method for probabilistic agents. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Ballarini, P., Fisher, M., & Wooldridge, M. (2009). Uncertain agent verification through probabilistic model-checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4324 LNAI, pp. 162–174). https://doi.org/10.1007/978-3-642-04879-1_12
Mendeley helps you to discover research relevant for your work.