Uncertain Agent Verification through Probabilistic Model-Checking

  • Paolo Ballarini
  • Michael Fisher
  • Michael Wooldridge
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4324)


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.


Model Check Reservation Price Acceptance Probability Discrete Time Markov Chain Negotiation Game 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Henzinger, T.: Reactive modules. Formal Methods in System Design 15(1), 7–48 (1999)CrossRefGoogle Scholar
  2. 2.
    Baier, C., Haverkort, B., Hermann, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Software Eng. 29(6), 524–541 (2003)CrossRefGoogle Scholar
  3. 3.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Model checking rational agents. IEEE Intelligent Systems 19(5), 46–52 (2004)CrossRefGoogle Scholar
  4. 4.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. Journal of Autonomous Agents and Multi-Agent Systems 12(2), 239–256 (2006)CrossRefGoogle Scholar
  5. 5.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  6. 6.
    Dix, J., Nanni, M., Subrahmanian, V.S.: Probabilistic agent programs. ACM Trans. Comput. Logic 1(2), 208–246 (2000)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Faratin, P., Sierra, C., Jennings, N.R.: Negotiation decision functions for autonomous agents. Int. Journal of Robotics and Autonomous Systems 24(3-4), 159–182 (1998)CrossRefGoogle Scholar
  8. 8.
    Feller, W.: An introduction to probability theory and its applications. John Wiley and Sons, Chichester (1968)zbMATHGoogle Scholar
  9. 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. 10.
    Holzmann, G.J.: The Spin Model Checker. Addison Wesley, Reading (2003)Google Scholar
  11. 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. 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. 13.
    Parker, D.: Prism web site,
  14. 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
  15. 15.
    Wooldridge, M.: Agent-based software engineering. IEE Proceedings on Software Engineering 144(1), 26–37 (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Paolo Ballarini
    • 1
  • Michael Fisher
    • 2
  • Michael Wooldridge
    • 2
  1. 1.University of GlasgowGlasgowUK
  2. 2.University of LiverpoolLiverpoolUK

Personalised recommendations