Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Acta Informatica
Erschienen in: Acta Informatica 7/2017

16.08.2016 | Original Article

Model-checking iterated games

verfasst von: Chung-Hao Huang, Sven Schewe, Farn Wang

Erschienen in: Acta Informatica | Ausgabe 7/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We propose a logic for the definition of the collaborative power of groups of agents to enforce different temporal objectives. The resulting temporal cooperation logic (TCL) extends ATL by allowing for successive definition of strategies for agents and agencies. Different to previous logics with similar aims, our extension cuts a fine line between extending the power and maintaining a low complexity: model checking TCL sentences is EXPTIME complete in the logic, and NL complete in the model. This advancement over nonelementary logics is bought by disallowing a too close entanglement between the cooperation and competition. We show how allowing such an entanglement immediately leads to a nonelementary complexity. We have implemented a model checker for the logic and shown the feasibility of model checking on a few benchmarks.
Nächster Artikel Safraless LTL synthesis considering maximal realizability

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
A strategy is forgiving if it does not always punish betrayal in the previous round.
 
2
A game is determined if a player knows whether she/he has a winning strategy even before the game is played.
 
3
If immediate acceptance is possible, a \(Q \cup \{\)accept,reject\(\}\) labeled tree. In this case, the complete subtrees rooted in a state labeled with ‘accept’ (resp. ‘reject’) are also labeled with ‘accept’ (resp. ‘reject’), where ‘accept’ is assigned an even and ‘reject’ an odd priority.
 
4
This is in contrast to the original concurrent game structure and also to its unraveling, where the number of strategies a state/node can refer to is unbounded.
 
5
Narrowing is a standard operation, where all atoms \(\big (q,(x,y)\big )\) are replaced by (q, x). The narrowing operation thus turns an automaton \(\mathcal B\) that recognizes a labeled \(\varSigma \times \Pi \) trees into an automaton \(\mathcal A\) that recognize those labeled \(\varSigma \) trees, whose \(\Pi \) widenings are accepted by \(\mathcal B\).
 
6
Recall that we use an enriched model, where all TCL formulas that start with an SQ have a truth assignment and can therefore be treated as a primitive TCL formula.
 
Literatur
1.
Alechina, N., Logan, B., Nguyen, H.N., Raimondi, F.: Symbolic model checking for one-resource rbÂśatl. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI) (2015)
2.
3.
Alur, R., Henzinger, T.A., Mang, F., Qadeer, S., Rajamani, S.K., Tasiran, S.: Mocha: modularity in model checking. In: Proceedings of the Tenth International Conference on Computer-Aided Verification (CAV 1998), Volume Lecture Notes in Computer Science (LNCS) 1427, pp. 521–525. Springer (1998)
4.
Axelrod, R.: Effective choice in the prisoner’s dilemma. J. Confl. Resolut. 24(1), 3–25 (1980)CrossRef
5.
Baier, C., Brázdil, T., Gröser, M., Kucera, A.: Stochastic game logic. In: QEST, pp. 227–236. IEEE Computer Society (2007)
6.
Brihaye, T., Lopes, A.D.C., Laroussinie, F., Markey, N.: ATL with strategy contexts and bounded memory. In LFCS, Volume LNCS 5407, pp. 92–106. Springer (2009)
7.
Büchi, J., Landweber, L.: Definability in the monadic second-order theory of successor. J. Symbol. Log. 34(2), 166–170 (1969)MathSciNetCrossRefMATH
8.
9.
Cermak, P., Lomuscio, A., Mogavero, F., Murano, A.: Mcmas-slk: a model checker for the verification of strategy logic specifications. In: International Conference on Computer-Aided Verification (CAV), volume LNCS 8559. Springer (2014)
10.
Chatterjee, K., Henzinger, T.A.: A survey of stochastic \(\omega \)-regular games. J. Comput. Syst. Sci. 78(2), 394–413 (2012)MathSciNetCrossRefMATH
11.
12.
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Workshop on Logic of Programs. volume LNCS 131. Springer (1981)
13.
Emerson, E., Jutla, C.: Tree automata, mu-calculus and determinacy. In: 32nd IEEE FOCS, pp. 368–377 (1991)
14.
Finkbeiner, B., Schewe, S.: Coordination logic. In: CSL, pp. 305–319 (2010)
15.
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
16.
17.
18.
Kupfermant, O., Vardit, M.Y.: Synthesis with incomplete information. In: Barringer, H., Fisher, M., Gabbay, D., Gough, G. (eds.) Advances in Temporal Logic. Applied Logic Series, vol. 16, pp. 109–127. Springer, Netherlands (2000)
19.
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)MathSciNetCrossRefMATH
20.
Laroussinie, F., Markey, N.: Satisfiability of ATL with strategy contexts. In: Workshop on Games, Automata, Logics and Formal Verification (GANDALF), volume EPTCS 119, pp. 208–223 (2013)
21.
Lopes, A.D.C., Laroussinie, F., Markey, N.: ATL with strategy contexts: expressiveness and model checking. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 120–132. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2010)
22.
Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: What makes ATL\(^*\) decidable? A decidable fragment of strategy logic. In: Concurrency theory (CONCUR 2012), volume LNCS 7454, pp. 193–208. Springer (2012)
23.
Mogavero, F., Murano, A., Sauro, L.: On the boundary of behavioral strategies. In: ACM/IEEE LICS (2013)
24.
Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 133–144. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2010)
25.
Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: new results and new proofs of the theorems of Rabin, McNaughton and Safra. Theor. Comput. Sci. 141(1–2), 69–107 (1995)MathSciNetCrossRefMATH
26.
Pinchinat, S.: A generic constructive solution for concurrent games with expressive constraints on strategies. In: Automated Technology for Verification and Analysis (ATVA), volume LNCS 4762, pp. 253–267. Springer (2007)
27.
Pnueli, A.: The temporal logic of programs. In: 18th Annual IEEE-CS Symposium on Foundations of Computer Science, pp. 45–57 (1977)
28.
Schewe, S.: Solving parity games in big steps. In: Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2007), 12–14 December, New Delhi, India, volume 4805 of Lecture Notes in Computer Science, pp. 449–460. Springer (2007)
29.
Schewe, S.: ATL* satisfiability is 2ExpTime-complete. In: Proceedings of the 35th International Colloquium on Automata, Languages and Programming, Part II (ICALP 2008), 6–13 July, Reykjavik, Iceland, volume 5126 of Lecture Notes in Computer Science, pp. 373–385. Springer (2008)
30.
31.
Stoica, F., Stoica, L.F.: Implementing an atl model checker tool using relational algebra concepts. In: 22nd International Conference on Software, Telecommunications and Computer Networks (SoftCOM), pp. 361–366. IEEE (2014)
32.
Stoica, L., Stoica, F., Boian, F.: Verification of JADE agents using ATL model checking. Int. J. Comput. Commun. Control 10(5), 718–731 (2015)CrossRef
33.
Vardi, M.Y., Stockmeyer, L.J.: Improved upper and lower bounds for modal logics of programs: preliminary report. In: Sedgewick, R. (eds.) Proceedings of the 17th Annual ACM Symposium on Theory of Computing (STOC), pp. 240–251 (1985)
34.
Walther, D., van der Hoek, W., Wooldridge, M.: Alternating-time temporal logic with explicit strategies. In: Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK), pp. 269–278 (2007)
35.
Wang, F., Schewe, S., Huang, C.-H.: An extension of ATL with strategy interaction. ACM Trans. Program. Lang. Syst. (TOPLAS), 37(3), 9 (2015) (A preliminary version is in the proceedings of CONCUR 2011, LNCS 6901, Springer-Verlag)
36.
Wilke, T.: Alternating tree automata, parity games, and modal \(\mu \)-calculus. Bull. Belg. Math. Soc. 8(2), 359–391 (2001)
Metadaten
Titel
Model-checking iterated games
verfasst von
Chung-Hao Huang
Sven Schewe
Farn Wang
Publikationsdatum
16.08.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
Acta Informatica / Ausgabe 7/2017
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-016-0277-y