<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>8343</REFNUM><AUTHORS><AUTHOR>Ballarini,P.</AUTHOR><AUTHOR>Fisher,M.D.</AUTHOR><AUTHOR>Wooldrige,M.</AUTHOR></AUTHORS><YEAR>2006</YEAR><TITLE>Uncertain Agent Verification through Probabilistic Model-Checking</TITLE><PLACE_PUBLISHED>to appear on LNAI hot topic volume</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><LABEL>Ballarini:2006:8343</LABEL><KEYWORDS><KEYWORD>agent-oriented software engineering</KEYWORD></KEYWORDS<ABSTRACT>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.</ABSTRACT></RECORD></RECORDS></XML>