EVE: A Tool for Temporal Equilibrium Analysis

  • Julian Gutierrez
  • Muhammad NajibEmail author
  • Giuseppe Perelli
  • Michael Wooldridge
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)


We present EVE (Equilibrium Verification Environment), a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems. In EVE, systems are modelled using the Simple Reactive Module Language (SRML) as a collection of independent system components (players/agents in a game) and players’ goals are expressed using Linear Temporal Logic (LTL) formulae. EVE can be used to automatically check the existence of pure strategy Nash equilibria in such concurrent and multi-agent systems and to verify which temporal logic properties are satisfied in the equilibria.



The authors acknowledge with gratitude the financial support of the ERC Advanced Investigator Grant 291528 (“RACE”) at Oxford. Muhammad Najib is supported by the Indonesian Endowment Fund for Education (LPDP).


  1. 1.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Brenguier, R.: Praline: a tool for computing nash equilibria in concurrent games. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 890–895. Springer, Heidelberg (2013). Scholar
  3. 3.
    Bulychev, P.E., David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Computing nash equilibrium in wireless ad hoc networks: A simulation-based approach. In: Proceedings Second International Workshop on Interactions, Games and Protocols, IWIGP 2012, Tallinn, Estonia, 25th March 2012, pp. 1–14 (2012)CrossRefGoogle Scholar
  4. 4.
    Fischer, M.J., Michael, A.: Sacrificing serializability to attain high availability of data in an unreliable network. In: PODS, pp. 70–75. ACM, New York (1982)Google Scholar
  5. 5.
    Gao, T., Gutierrez, J., Wooldridge, M.: Iterated boolean games for rational verification. In: AAMAS, pp. 705–713. ACM, Sao Paulo, Brazil (2017)Google Scholar
  6. 6.
    Gifford, D.K.: Weighted voting for replicated data. In: Proceedings of the Seventh ACM Symposium on Operating Systems Principles SOSP ’79, pp. 150–162. ACM, New York (1979)Google Scholar
  7. 7.
    Gutierrez, J., Harrenstein, P., Perelli, G., Wooldridge, M.: Nash equilibrium and bisimulation invariance. In: CONCUR. LIPIcs, vol. 85, pp. 17:1–17:16. Schloss Dagstuhl, Berlin, Germany (2017)Google Scholar
  8. 8.
    Gutierrez, J., Harrenstein, P., Wooldridge, M.: Iterated boolean games. Inf. Comput. 242, 53–79 (2015)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Gutierrez, J., Harrenstein, P., Wooldridge, M.: From model checking to equilibrium checking: reactive modules for rational verification. Artif. Intell. 248, 123–157 (2017)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Gutierrez, J., Harrenstein, P., Wooldridge, M.: Reasoning about equilibria in game-like concurrent systems. Ann. Pure Appl. Log. 168(2), 373–403 (2017)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Gutierrez, J., Murano, A., Perelli, G., Rubin, S., Wooldridge, M.: Nash equilibria in concurrent games with lexicographic preferences. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19–25, 2017, pp. 1067–1073 (2017) ( Scholar
  12. 12.
    Gutierrez, J., Perelli, G., Wooldridge, M.: Imperfect information in reactive modules games. Inf. Comput. 261, 650–675 (2018)MathSciNetCrossRefGoogle Scholar
  13. 13.
    van der Hoek, W., Lomuscio, A., Wooldridge, M.: On the complexity of practical ATL model checking. In: Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems AAMAS ’06, pp. 201–208. ACM, New York, NY, USA (2006)Google Scholar
  14. 14.
    Ladin, R., Liskov, B., Shrira, L., Ghemawat, S.: Providing high availability using lazy replication. ACM Trans. Comput. Syst. 10(4), 360–391 (1992)CrossRefGoogle Scholar
  15. 15.
    Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell (1997)CrossRefGoogle Scholar
  16. 16.
    Nisan, N.: Introduction to mechanism design (for computer scientists). In: Nisan, N., Roughgarden, T., Tardos, E., Vazirani, V.V. (eds.) Algorithmic Game Theory, pp. 209–242. Cambridge University Press, Cambridge (2007)Google Scholar
  17. 17.
    Osborne, M.J., Rubinstein, A.: A Course in Game Theory. MIT Press, Cambridge (1994)Google Scholar
  18. 18.
    Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE, Rhode Island, USA (1977)Google Scholar
  19. 19.
    Toumi, A., Gutierrez, J., Wooldridge, M.: A tool for the automated verification of nash equilibria in concurrent games. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 583–594. Springer, Cham (2015). Scholar
  20. 20.
    Čermák, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525–532. Springer, Cham (2014). Scholar
  21. 21.
    Wooldridge, M., Gutierrez, J., Harrenstein, P., Marchioni, E., Perelli, G., Toumi, A.: Rational verification: From model checking to equilibrium checking. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12–17, 2016, Phoenix, Arizona, USA, pp. 4184–4191 (2016)Google Scholar
  22. 22.
    Wuu, G.T., Bernstein, A.J.: Efficient solutions to the replicated log and dictionary problems. In: Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing PODC ’84, pp. 233–242. ACM, New York, USA (1984)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Julian Gutierrez
    • 1
  • Muhammad Najib
    • 1
    Email author
  • Giuseppe Perelli
    • 1
  • Michael Wooldridge
    • 1
  1. 1.Department of Computer ScienceUniversity of OxfordOxfordUK

Personalised recommendations