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.
This work was partially supported by NSFC grant (61402179, 61532019, 61662035, 61572478, 61472474, 61100062, and 61272135), UK EPSRC grant (EP/P00430X/1), and European CHIST-ERA project SUCCESS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
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.
- 2.
“complete” means that \(\varDelta (q, \gamma )\) is defined for each \((q,\gamma ) \in Q \times \varGamma \).
- 3.
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].
- 4.
\(\langle {\emptyset }\rangle \) (resp. \([{\emptyset }]\)) is the universal (resp. existential) path quantification A (resp. E).
References
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)
Aminof, B., Legay, A., Murano, A., Serre, O., Vardi, M.Y.: Pushdown module checking with imperfect information. Inf. Comput. 223, 1–17 (2013)
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)
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
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
Cermák, Petr: A model checker for strategy logic. Meng individual project, Department of Computing, Imperial College, London (2015)
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)
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)
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
Chen, T., Song, F., Wu, Z.: Global model checking on pushdown multi-agent systems. In: AAAI 2016, pp. 2459–2465 (2016)
Chen, T., Song, F., Wu, Z.: Verifying pushdown multi-agent systems against strategy logics. In: IJCAI 2016, pp. 180–186 (2016)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)
Dima, C., Tiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225 (2011)
Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355–376 (2003)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Jamroga, W.: Some remarks on alternating temporal epistemic logic. In: FAMAS 2003, pp. 133–140 (2003)
Jamroga, W., Dix, J.: Model checking abilities under incomplete information is indeed Delta2-complete. In: EUMAS 2006 (2006)
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
Lomuscio, A., Raimondi, F.: Model checking knowledge, strategies, and games in multi-agent systems. In: AAMAS 2006, pp. 161–168 (2006)
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)
Mogavero, F., Murano, A., Sauro, L.: On the boundary of behavioral strategies. In: LICS 2013, pp. 263–272 (2013)
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
Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: FSTTCS 2010, pp. 133–144 (2010)
Murano, A., Perelli, G.: Pushdown multi-agent system verification. In: IJCAI 2015, pp. 1090–1097 (2015)
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)
Schobbens, P.-Y.: Alternating-time logic with imperfect recall. Electron. Notes Theoret. Comput. Sci. 85(2), 82–93 (2004)
Schwoon, S.: Model checking pushdown systems. Ph.D. thesis, Technical University Munich, Germany (2002)
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
Song, F., Touili, T.: Efficient CTL model-checking for pushdown systems. Theoret. Comput. Sci. 549, 127–145 (2014)
van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: AAMAS 2002, pp. 1167–1174 (2002)
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)
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
Hague, M., Ong, C.-H.L.: A saturation method for the modal \(\mu \)-calculus over pushdown systems. Inf. Comput. 209(5), 799–821 (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Chen, T., Song, F., Wu, Z. (2017). Model Checking Pushdown Epistemic Game Structures. In: Duan, Z., Ong, L. (eds) Formal Methods and Software Engineering. ICFEM 2017. Lecture Notes in Computer Science(), vol 10610. Springer, Cham. https://doi.org/10.1007/978-3-319-68690-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-68690-5_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68689-9
Online ISBN: 978-3-319-68690-5
eBook Packages: Computer ScienceComputer Science (R0)