Skip to main content
SpringerLink
Log in

EVE: A Tool for Temporal Equilibrium Analysis

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11138))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We refer to [9, 21] for the formal characterisation of NE.

  2. 2.

    The core of the protocol involves (at least) pairwise interactions periodically.

  3. 3.

    We assume arithmetic modulo \( (|\text {N}|+1) \) in this example.

  4. 4.

    The tool to automatically convert EVE’s input (SRML code) into MCMAS’s input (ISPL code) is available online from https://github.com/eve-mas/sevia.

  5. 5.

    To carry out a fairer comparison (since PRALINE accepts Büchi objectives), we added to PRALINE’s running time, the time needed to convert LTL games into its input. Translating parity games to PRALINE’s input is possible in our particular examples since in those cases we can map the colours/priorities directly into Büchi condition.

References

  1. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-39799-8_63

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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. 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. 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. 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. Gutierrez, J., Harrenstein, P., Wooldridge, M.: Iterated boolean games. Inf. Comput. 242, 53–79 (2015)

    Article  MathSciNet  Google Scholar 

  9. Gutierrez, J., Harrenstein, P., Wooldridge, M.: From model checking to equilibrium checking: reactive modules for rational verification. Artif. Intell. 248, 123–157 (2017)

    Article  MathSciNet  Google Scholar 

  10. Gutierrez, J., Harrenstein, P., Wooldridge, M.: Reasoning about equilibria in game-like concurrent systems. Ann. Pure Appl. Log. 168(2), 373–403 (2017)

    Article  MathSciNet  Google Scholar 

  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) (ijcai.org)

    Google Scholar 

  12. Gutierrez, J., Perelli, G., Wooldridge, M.: Imperfect information in reactive modules games. Inf. Comput. 261, 650–675 (2018)

    Article  MathSciNet  Google Scholar 

  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. Ladin, R., Liskov, B., Shrira, L., Ghemawat, S.: Providing high availability using lazy replication. ACM Trans. Comput. Syst. 10(4), 360–391 (1992)

    Article  Google Scholar 

  15. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell (1997)

    Article  Google Scholar 

  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. Osborne, M.J., Rubinstein, A.: A Course in Game Theory. MIT Press, Cambridge (1994)

    Google Scholar 

  18. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE, Rhode Island, USA (1977)

    Google Scholar 

  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). https://doi.org/10.1007/978-3-319-25150-9_34

    Chapter  MATH  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-08867-9_34

    Chapter  Google Scholar 

  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. 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 

Download references

Acknowledgements

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).

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, UK

    Julian Gutierrez, Muhammad Najib, Giuseppe Perelli & Michael Wooldridge

Authors
  1. Julian Gutierrez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Muhammad Najib
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Giuseppe Perelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Michael Wooldridge
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Muhammad Najib .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Shuvendu K. Lahiri

  2. University of Southern California, Los Angeles, CA, USA

    Chao Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Gutierrez, J., Najib, M., Perelli, G., Wooldridge, M. (2018). EVE: A Tool for Temporal Equilibrium Analysis. In: Lahiri, S., Wang, C. (eds) Automated Technology for Verification and Analysis. ATVA 2018. Lecture Notes in Computer Science(), vol 11138. Springer, Cham. https://doi.org/10.1007/978-3-030-01090-4_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-01090-4_35

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-01089-8

  • Online ISBN: 978-3-030-01090-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation