nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Model Checking Pushdown Epistemic Game Structures

verfasst von : Taolue Chen, Fu Song, Zhilin Wu

Erschienen in: Formal Methods and Software Engineering

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

In this paper, we investigate the problem of verifying pushdown multi-agent systems with imperfect information. As the formal model, we introduce pushdown epistemic game structures (PEGSs), an extension of pushdown game structures with epistemic accessibility relations (EARs). For the specification, we consider extensions of alternating-time temporal logics with epistemic modalities: ATEL, ATEL\(^*\) and AEMC. We study the model checking problems for ATEL, ATEL\(^*\) and AEMC over PEGSs under various imperfect information settings. For ATEL and ATEL\(^*\), we show that size-preserving EARs, a common definition of the accessibility relation in the literature of games over pushdown systems with imperfect information, will render the model checking problem undecidable under imperfect information and imperfect recall setting. We then propose regular EARs, and provide automata-theoretic model checking algorithms with matching low bounds, i.e., EXPTIME-complete for ATEL and 2EXPTIME-complete for ATEL\(^*\). In contrast, for AEMC, we show that the model checking problem is EXPTIME-complete even in the presence of size-preserving EARs.

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

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

Vorheriges Kapitel Modularization of Refinement Steps for Agile Formal Methods

Nächstes Kapitel Transforming Timing Requirements into CCSL Constraints to Verify Cyber-Physical Systems

One may notice that, in the definition of PEGSs, \(\varDelta \) is defined as a complete function \(P\times \varGamma \times \mathcal {D}\rightarrow P\times \varGamma ^*\), meaning that all actions are available to each agent. This does not restrict the expressiveness of PEGSs, as we can easily add transitions to some additional sink state to simulate the situation where some actions are unavailable to some agents.

“complete” means that \(\varDelta (q, \gamma )\) is defined for each \((q,\gamma ) \in Q \times \varGamma \).

Since normal PEGS only pops one symbol from the stack at one step, in order to pop m symbols, we need to introduce some additional control states as done in [30].

\(\langle {\emptyset }\rangle \) (resp. \([{\emptyset }]\)) is the universal (resp. existential) path quantification A (resp. E).

Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: FOCS 1997, pp. 100–109 (1997)

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

Aminof, B., Legay, A., Murano, A., Serre, O., Vardi, M.Y.: Pushdown module checking with imperfect information. Inf. Comput. 223, 1–17 (2013)MathSciNetCrossRefMATH

Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). doi:10.1007/3-540-63141-0_10

Bozzelli, L.: Complexity results on branching-time pushdown model checking. Theoret. Comput. Sci. 379(1–2), 286–297 (2007)MathSciNetCrossRefMATH

Brihaye, T., Laroussinie, F., Markey, N., Oreiby, G.: Timed concurrent game structures. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 445–459. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74407-8_30 CrossRef

Bulling, N., Jamroga, W.: Alternating epistemic mu-calculus. In: IJCAI 2011, pp. 109–114 (2011)

Bulling, N., Nguyen, H.N.: Model checking resource bounded systems with shared resources via alternating büchi pushdown systems. In: Chen, Q., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds.) PRIMA 2015. LNCS (LNAI), vol. 9387, pp. 640–649. Springer, Cham (2015). doi:10.1007/978-3-319-25524-8_47 CrossRef

Cermák, Petr: A model checker for strategy logic. Meng individual project, Department of Computing, Imperial College, London (2015)

10.

Cermák, P., Lomuscio, A., Murano, A.: Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In: AAAI 2015, pp. 2038–2044 (2015)

11.

Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61–92 (2013)CrossRefMATH

12.

Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: a model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185–191. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_13 CrossRef

13.

Chen, T., Song, F., Wu, Z.: Global model checking on pushdown multi-agent systems. In: AAAI 2016, pp. 2459–2465 (2016)

14.

Chen, T., Song, F., Wu, Z.: Verifying pushdown multi-agent systems against strategy logics. In: IJCAI 2016, pp. 180–186 (2016)

15.

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)CrossRef

16.

Dima, C., Tiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225 (2011)

17.

Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355–376 (2003)MathSciNetCrossRefMATH

18.

Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)MATH

19.

Jamroga, W.: Some remarks on alternating temporal epistemic logic. In: FAMAS 2003, pp. 133–140 (2003)

20.

Jamroga, W., Dix, J.: Model checking abilities under incomplete information is indeed Delta2-complete. In: EUMAS 2006 (2006)

21.

Kupferman, O., Piterman, N., Vardi, M.Y.: Pushdown specifications. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 262–277. Springer, Heidelberg (2002). doi:10.1007/3-540-36078-6_18 CrossRef

22.

Lomuscio, A., Raimondi, F.: Model checking knowledge, strategies, and games in multi-agent systems. In: AAMAS 2006, pp. 161–168 (2006)

23.

Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: on the model-checking problem. ACM Trans. Comput. Logic 15(4), 34:1–34:47 (2014)MathSciNetCrossRefMATH

24.

Mogavero, F., Murano, A., Sauro, L.: On the boundary of behavioral strategies. In: LICS 2013, pp. 263–272 (2013)

25.

Mogavero, F., Murano, A., Sauro, L.: A behavioral hierarchy of strategy logic. In: Bulling, N., Torre, L., Villata, S., Jamroga, W., Vasconcelos, W. (eds.) CLIMA 2014. LNCS (LNAI), vol. 8624, pp. 148–165. Springer, Cham (2014). doi:10.1007/978-3-319-09764-0_10

26.

Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: FSTTCS 2010, pp. 133–144 (2010)

27.

Murano, A., Perelli, G.: Pushdown multi-agent system verification. In: IJCAI 2015, pp. 1090–1097 (2015)

28.

Pilecki, J., Bednarczyk, M.A., Jamroga, W.: Model checking properties of multi-agent systems with imperfect information and imperfect recall. In: IS 2014, pp. 415–426 (2014)

29.

Schobbens, P.-Y.: Alternating-time logic with imperfect recall. Electron. Notes Theoret. Comput. Sci. 85(2), 82–93 (2004)MathSciNetCrossRefMATH

30.

Schwoon, S.: Model checking pushdown systems. Ph.D. thesis, Technical University Munich, Germany (2002)

31.

Song, F., Touili, T.: Efficient CTL model-checking for pushdown systems. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 434–449. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23217-6_29 CrossRef

32.

Song, F., Touili, T.: Efficient CTL model-checking for pushdown systems. Theoret. Comput. Sci. 549, 127–145 (2014)MathSciNetCrossRefMATH

33.

van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: AAMAS 2002, pp. 1167–1174 (2002)

34.

van der Hoek, W., Wooldridge, M.: Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications. Stud. Logica 75(1), 125–157 (2003)MathSciNetCrossRefMATH

35.

Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FSTTCS 2000. LNCS, vol. 1974, pp. 127–138. Springer, Heidelberg (2000). doi:10.1007/3-540-44450-5_10 CrossRef

36.

Hague, M., Ong, C.-H.L.: A saturation method for the modal \(\mu \)-calculus over pushdown systems. Inf. Comput. 209(5), 799–821 (2011)MathSciNetCrossRefMATH

Titel: Model Checking Pushdown Epistemic Game Structures
verfasst von: Taolue Chen
Fu Song
Zhilin Wu
Verlag: Springer International Publishing
Buch: Formal Methods and Software Engineering
Print ISBN: 978-3-319-68689-9

Electronic ISBN: 978-3-319-68690-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-68690-5_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner