Uncertain Agent Verification through Probabilistic Model-Checking
- 394 Downloads
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.
KeywordsModel Check Reservation Price Acceptance Probability Discrete Time Markov Chain Negotiation Game
Unable to display preview. Download preview PDF.
- 5.Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
- 9.Hansson, H.A., Jonsson, B.: A framework for reasoning about time and reliability. In: Proc. 10th IEEE Real -Time Systems Symposium, pp. 102–111. IEEE Computer Society Press, Santa Monica (1989)Google Scholar
- 10.Holzmann, G.J.: The Spin Model Checker. Addison Wesley, Reading (2003)Google Scholar
- 11.Kwiatokowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with prism: A hybrid approach. International Journal on Software Tools for Technology Transfer, STTT (2004)Google Scholar
- 12.Li, C., Giampapa, J., Sycara, K.: Bilateral negotiation decisions with uncertain dynamic outside options. IEEE Transactions on Systems, Man, and Cybernetics 36, Part C: Special Issue on Game-theoretic Analysis and Stochastic Simulation of Negotiation Agents(No. 1) (2006)Google Scholar
- 13.Parker, D.: Prism web site, http://www.cs.bham.ac.uk/~dxp/prism
- 14.Pnueli, A.: The temporal logic of programs. In: Proceedings of the Eighteenth IEEE Symposium on the Foundations of Computer Science, pp. 46–57 (1977)Google Scholar