Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks Read chapter Read first chapter

2018 | OriginalPaper | Chapter

EVE: A Tool for Temporal Equilibrium Analysis

Authors : Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Owl: A Library for -Words, Automata, and LTL
Footnotes
1
We refer to [9, 21] for the formal characterisation of NE.
 
2
The core of the protocol involves (at least) pairwise interactions periodically.
 
3
We assume arithmetic modulo \( (|\text {N}|+1) \) in this example.
 
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
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.
 
Literature
1.
2.
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)CrossRef
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)
5.
Gao, T., Gutierrez, J., Wooldridge, M.: Iterated boolean games for rational verification. In: AAMAS, pp. 705–713. ACM, Sao Paulo, Brazil (2017)
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)
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)
8.
9.
Gutierrez, J., Harrenstein, P., Wooldridge, M.: From model checking to equilibrium checking: reactive modules for rational verification. Artif. Intell. 248, 123–157 (2017)MathSciNetCrossRef
10.
Gutierrez, J., Harrenstein, P., Wooldridge, M.: Reasoning about equilibria in game-like concurrent systems. Ann. Pure Appl. Log. 168(2), 373–403 (2017)MathSciNetCrossRef
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)
12.
Gutierrez, J., Perelli, G., Wooldridge, M.: Imperfect information in reactive modules games. Inf. Comput. 261, 650–675 (2018)MathSciNetCrossRef
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)
14.
Ladin, R., Liskov, B., Shrira, L., Ghemawat, S.: Providing high availability using lazy replication. ACM Trans. Comput. Syst. 10(4), 360–391 (1992)CrossRef
15.
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)
17.
Osborne, M.J., Rubinstein, A.: A Course in Game Theory. MIT Press, Cambridge (1994)
18.
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE, Rhode Island, USA (1977)
19.
20.
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)
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)
Metadata
Title
EVE: A Tool for Temporal Equilibrium Analysis
Authors
Julian Gutierrez
Muhammad Najib
Giuseppe Perelli
Michael Wooldridge
Copyright Year
2018
Book
Automated Technology for Verification and Analysis

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

Electronic ISBN: 978-3-030-01090-4

Copyright Year: 2018

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

Premium Partner

    Image Credits