{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T23:40:26Z","timestamp":1737157226523,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540727323"},{"type":"electronic","value":"9783540727347"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-72734-7_14","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T09:40:50Z","timestamp":1183023650000},"page":"195-211","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking Knowledge and Linear Time: PSPACE Cases"],"prefix":"10.1007","author":[{"given":"Kai","family":"Engelhardt","sequence":"first","affiliation":[]},{"given":"Peter","family":"Gammie","sequence":"additional","affiliation":[]},{"given":"Ron","family":"van der Meyden","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements, common knowledge, and private suspicions. In: TARK \u201998: Proc. 7th Conf. Theoretical Aspects of Rationality and Knowledge, pp. 43\u201356 (1998)"},{"issue":"1","key":"14_CR2","first-page":"114","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J.\u00a0ACM\u00a028(1), 114\u2013133 (1981)","journal-title":"J.\u00a0ACM"},{"key":"14_CR3","unstructured":"Cimatti, A., Pecheur, C., Cavada, R.: Formal verification of diagnosability via symbolic model checking. In: IJCAI, pp. 363\u2013369 (2003)"},{"key":"14_CR4","unstructured":"Cimatti, A., Pecheur, C., Lomuscio, A.: Applications of model checking for multi-agent systems: Verification of diagnosability and recoverability. In: CS&P \u201905: Proc. Int. Work. Concurrency, Specification, and Programming (2005)"},{"key":"14_CR5","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":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-48153-2_29","volume-title":"Correct Hardware Design and Verification Methods","author":"K. Fisler","year":"1999","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 338\u2013342. Springer, Heidelberg (1999)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/978-3-540-27813-9_41","volume-title":"Computer Aided Verification","author":"P. Gammie","year":"2004","unstructured":"Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 479\u2013483. Springer, Heidelberg (2004)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-70881-0_31","volume-title":"Perspectives of Systems Informatics","author":"N.V. Shilov","year":"2007","unstructured":"Shilov, N.V., Garanina, N.O.: Well-structured model checking of multiagent systems. In: Virbitskaite, I., Voronkov, A. (eds.) PSI 2006. LNCS, vol.\u00a04378, pp. 363\u2013376. Springer, Heidelberg (2007)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y., Moses, Y.: Knowledge and Common Knowledge in a Distributed Environment. J.\u00a0ACM\u00a037(3) (1990)","DOI":"10.1145\/79147.79161"},{"key":"14_CR10","first-page":"75","volume-title":"CSFW","author":"J.Y. Halpern","year":"2003","unstructured":"Halpern, J.Y., O\u2019Neill, K.R.: Anonymity and information hiding in multiagent systems. In: CSFW, pp. 75\u201388. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/318593.318622","volume-title":"POPL \u201985: Proc. 12th ACM SIGACT-SIGPLAN Symp. Principles of Programming Languages","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL \u201985: Proc. 12th ACM SIGACT-SIGPLAN Symp. Principles of Programming Languages, pp. 97\u2013107. ACM Press, New York (1985)"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1145\/1160633.1160733","volume-title":"AAMAS","author":"A. Lomuscio","year":"2006","unstructured":"Lomuscio, A., Raimondi, F.: The complexity of model checking concurrent programs against CTLK specifications. In: Nakashima, H., Wellman, M.P., Weiss, G., Stone, P. (eds.) AAMAS, pp. 548\u2013550. ACM Press, New York (2006)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/11691372_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Lomuscio","year":"2006","unstructured":"Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 450\u2013454. Springer, Heidelberg (2006)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D.M.R. Park","year":"1981","unstructured":"Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"issue":"2","key":"14_CR15","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W.J. Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J.\u00a0Comput. Syst. Sci.\u00a04(2), 177\u2013192 (1970)","journal-title":"J.\u00a0Comput. Syst. Sci."},{"key":"14_CR16","unstructured":"Shilov, N.V., Garanina, N.O.: Model checking knowledge and fixpoints. In: \u00c9sik, Z., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FICS, volume NS-02-2 of BRICS Notes Series, pp. 25\u201339. University of Aarhus (2002)"},{"issue":"1\u20133","key":"14_CR17","first-page":"347","volume":"72","author":"N.V. Shilov","year":"2006","unstructured":"Shilov, N.V., Garanina, N.O., Choe, K.-M.: Update and abstraction in model checking of knowledge and branching time. Fundamenta Informaticae\u00a072(1\u20133), 347\u2013361 (2006)","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"14_CR18","first-page":"733","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J.\u00a0ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"J.\u00a0ACM"},{"key":"14_CR19","first-page":"414","volume-title":"ISCA \u201986: Proc. 13th Int. Symp. Computer Architecture","author":"P. Sweazey","year":"1986","unstructured":"Sweazey, P., Smith, A.J.: A class of compatible cache consistency protocols and their support by the IEEE futurebus. In: ISCA \u201986: Proc. 13th Int. Symp. Computer Architecture, pp. 414\u2013423. IEEE Computer Society Press, Los Alamitos (1986)"},{"issue":"3\u20134","key":"14_CR20","doi-asserted-by":"crossref","first-page":"317","DOI":"10.3233\/JCS-1992-13-407","volume":"1","author":"P.F. Syverson","year":"1992","unstructured":"Syverson, P.F.: Knowledge, belief, and semantics in the analysis of cryptographic protocols. J. Computer Security\u00a01(3\u20134), 317\u2013334 (1992)","journal-title":"J. Computer Security"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/3-540-62034-6_55","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"R. Meyden van der","year":"1996","unstructured":"van der Meyden, R.: Finite state implementations of knowledge-based programs. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol.\u00a01180, pp. 262\u2013273. Springer, Heidelberg (1996)"},{"issue":"2","key":"14_CR22","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1006\/inco.1997.2679","volume":"140","author":"R. Meyden van der","year":"1998","unstructured":"van der Meyden, R.: Common knowledge and update in finite environments. Information and Computation\u00a0140(2), 115\u2013157 (1998)","journal-title":"Information and Computation"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/3-540-46691-6_35","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"R. Meyden van der","year":"1999","unstructured":"van der Meyden, R., Shilov, N.V.: Model checking knowledge and time in systems with perfect recall (extended abstract). In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, p. 432. Springer, Heidelberg (1999)"},{"key":"14_CR24","volume-title":"CFSW 2004: Proc. 17th IEEE Computer Security Foundations Workshop","author":"R. Meyden van der","year":"2004","unstructured":"van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: CFSW 2004: Proc. 17th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1007\/11539452_42","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"R. Meyden van der","year":"2005","unstructured":"van der Meyden, R., Wilke, T.: Synthesis of distributed systems from knowledge-based specifications. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 562\u2013576. Springer, Heidelberg (2005)"},{"key":"14_CR26","unstructured":"van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. In: Proceedings Workshop on Views on Designing Complex Systems, Bertinoro, Italy, Sep. 2006. ENTCS, to appear (2006)"},{"key":"14_CR27","unstructured":"van Eijck, J., Orzan, S.: Modelling the epistemics of communication with functional programming. In: van Eekelen, M. (ed.) TFP \u201905: 6th Symp. Trends in Functional Programming, pp. 44\u201359 (2005)"},{"key":"14_CR28","first-page":"15","volume-title":"TARK \u201996: Proc. 6th Conf. Theoretical Aspects of Rationality and Knowledge","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: Implementing knowledge-based programs. In: Shoham, Y. (ed.) TARK \u201996: Proc. 6th Conf. Theoretical Aspects of Rationality and Knowledge, pp. 15\u201330. Morgan Kaufmann, San Francisco (1996)"},{"key":"14_CR29","first-page":"446","volume-title":"STOC","author":"M.Y. Vardi","year":"1984","unstructured":"Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs (extended abstract). In: STOC, pp. 446\u2013456. ACM Press, New York (1984)"},{"key":"14_CR30","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1145\/1082473.1082498","volume-title":"AAMAS \u201905: 4th Int. J. Conf. Autonomous Agents and Multiagent Systems","author":"B. Wozna","year":"2005","unstructured":"Wozna, B., Lomuscio, A., Penczek, W.: Bounded model checking for knowledge and real time. In: AAMAS \u201905: 4th Int. J. Conf. Autonomous Agents and Multiagent Systems, Utrecht, 25\u201329 July 2005, pp. 165\u2013172. ACM Press, New York (2005)"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72734-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T23:03:40Z","timestamp":1737155020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72734-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540727323","9783540727347"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72734-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}