{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T03:40:03Z","timestamp":1750909203153,"version":"3.41.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319686899"},{"type":"electronic","value":"9783319686905"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68690-5_3","type":"book-chapter","created":{"date-parts":[[2017,10,10]],"date-time":"2017-10-10T01:14:51Z","timestamp":1507598091000},"page":"36-53","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking Pushdown Epistemic Game\u00a0Structures"],"prefix":"10.1007","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,11]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: FOCS 1997, pp. 100\u2013109 (1997)","DOI":"10.1109\/SFCS.1997.646098"},{"issue":"5","key":"3_CR2","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"3_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2012.11.005","volume":"223","author":"B Aminof","year":"2013","unstructured":"Aminof, B., Legay, A., Murano, A., Serre, O., Vardi, M.Y.: Pushdown module checking with imperfect information. Inf. Comput. 223, 1\u201317 (2013)","journal-title":"Inf. Comput."},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR 1997: Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"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\u2013150. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63141-0_10"},{"issue":"1\u20132","key":"3_CR5","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1016\/j.tcs.2007.03.049","volume":"379","author":"L Bozzelli","year":"2007","unstructured":"Bozzelli, L.: Complexity results on branching-time pushdown model checking. Theoret. Comput. Sci. 379(1\u20132), 286\u2013297 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-540-74407-8_30","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"T Brihaye","year":"2007","unstructured":"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\u2013459. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74407-8_30"},{"key":"3_CR7","unstructured":"Bulling, N., Jamroga, W.: Alternating epistemic mu-calculus. In: IJCAI 2011, pp. 109\u2013114 (2011)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-319-25524-8_47","volume-title":"PRIMA 2015: Principles and Practice of Multi-Agent Systems","author":"N Bulling","year":"2015","unstructured":"Bulling, N., Nguyen, H.N.: Model checking resource bounded systems with shared resources via alternating b\u00fcchi pushdown systems. In: Chen, Q., Torroni, P., Villata, S., Hsu, J., Omicini, A. (eds.) PRIMA 2015. LNCS (LNAI), vol. 9387, pp. 640\u2013649. Springer, Cham (2015). doi: 10.1007\/978-3-319-25524-8_47"},{"key":"3_CR9","unstructured":"Cerm\u00e1k, Petr: A model checker for strategy logic. Meng individual project, Department of Computing, Imperial College, London (2015)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Cerm\u00e1k, P., Lomuscio, A., Murano, A.: Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In: AAAI 2015, pp. 2038\u20132044 (2015)","DOI":"10.1609\/aaai.v29i1.9444"},{"issue":"1","key":"3_CR11","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43(1), 61\u201392 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-36742-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Chen","year":"2013","unstructured":"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\u2013191. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_13"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Chen, T., Song, F., Wu, Z.: Global model checking on pushdown multi-agent systems. In: AAAI 2016, pp. 2459\u20132465 (2016)","DOI":"10.1609\/aaai.v30i1.10124"},{"key":"3_CR14","unstructured":"Chen, T., Song, F., Wu, Z.: Verifying pushdown multi-agent systems against strategy logics. In: IJCAI 2016, pp. 180\u2013186 (2016)"},{"key":"3_CR15","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"3_CR16","unstructured":"Dima, C., Tiplea, F.L.: Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs\/1102.4225 (2011)"},{"issue":"2","key":"3_CR17","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1016\/S0890-5401(03)00139-1","volume":"186","author":"J Esparza","year":"2003","unstructured":"Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355\u2013376 (2003)","journal-title":"Inf. Comput."},{"key":"3_CR18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning About Knowledge","author":"R Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)"},{"key":"3_CR19","unstructured":"Jamroga, W.: Some remarks on alternating temporal epistemic logic. In: FAMAS 2003, pp. 133\u2013140 (2003)"},{"key":"3_CR20","unstructured":"Jamroga, W., Dix, J.: Model checking abilities under incomplete information is indeed Delta2-complete. In: EUMAS 2006 (2006)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-36078-6_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O Kupferman","year":"2002","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Pushdown specifications. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 262\u2013277. Springer, Heidelberg (2002). doi: 10.1007\/3-540-36078-6_18"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Raimondi, F.: Model checking knowledge, strategies, and games in multi-agent systems. In: AAMAS 2006, pp. 161\u2013168 (2006)","DOI":"10.1145\/1160633.1160660"},{"issue":"4","key":"3_CR23","doi-asserted-by":"crossref","first-page":"34:1","DOI":"10.1145\/2631917","volume":"15","author":"F Mogavero","year":"2014","unstructured":"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\u201334:47 (2014)","journal-title":"ACM Trans. Comput. Logic"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Mogavero, F., Murano, A., Sauro, L.: On the boundary of behavioral strategies. In: LICS 2013, pp. 263\u2013272 (2013)","DOI":"10.1109\/LICS.2013.32"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-09764-0_10","volume-title":"Computational Logic in Multi-Agent Systems","author":"F Mogavero","year":"2014","unstructured":"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\u2013165. Springer, Cham (2014). doi: 10.1007\/978-3-319-09764-0_10"},{"key":"3_CR26","unstructured":"Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: FSTTCS 2010, pp. 133\u2013144 (2010)"},{"key":"3_CR27","unstructured":"Murano, A., Perelli, G.: Pushdown multi-agent system verification. In: IJCAI 2015, pp. 1090\u20131097 (2015)"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"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\u2013426 (2014)","DOI":"10.1007\/978-3-319-11313-5_37"},{"issue":"2","key":"3_CR29","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1016\/S1571-0661(05)82604-0","volume":"85","author":"P-Y Schobbens","year":"2004","unstructured":"Schobbens, P.-Y.: Alternating-time logic with imperfect recall. Electron. Notes Theoret. Comput. Sci. 85(2), 82\u201393 (2004)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"3_CR30","unstructured":"Schwoon, S.: Model checking pushdown systems. Ph.D. thesis, Technical University Munich, Germany (2002)"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-23217-6_29","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"F Song","year":"2011","unstructured":"Song, F., Touili, T.: Efficient CTL model-checking for pushdown systems. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 434\u2013449. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23217-6_29"},{"key":"3_CR32","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/j.tcs.2014.07.001","volume":"549","author":"F Song","year":"2014","unstructured":"Song, F., Touili, T.: Efficient CTL model-checking for pushdown systems. Theoret. Comput. Sci. 549, 127\u2013145 (2014)","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: AAMAS 2002, pp. 1167\u20131174 (2002)","DOI":"10.1145\/545056.545095"},{"issue":"1","key":"3_CR34","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1023\/A:1026185103185","volume":"75","author":"W Hoek van der","year":"2003","unstructured":"van der Hoek, W., Wooldridge, M.: Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications. Stud. Logica 75(1), 125\u2013157 (2003)","journal-title":"Stud. Logica"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-44450-5_10","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science","author":"I Walukiewicz","year":"2000","unstructured":"Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FSTTCS 2000. LNCS, vol. 1974, pp. 127\u2013138. Springer, Heidelberg (2000). doi: 10.1007\/3-540-44450-5_10"},{"issue":"5","key":"3_CR36","doi-asserted-by":"crossref","first-page":"799","DOI":"10.1016\/j.ic.2010.12.004","volume":"209","author":"M Hague","year":"2011","unstructured":"Hague, M., Ong, C.-H.L.: A saturation method for the modal $$\\mu $$ -calculus over pushdown systems. Inf. Comput. 209(5), 799\u2013821 (2011)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68690-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T03:05:24Z","timestamp":1750907124000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68690-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319686899","9783319686905"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68690-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}