{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:29:39Z","timestamp":1743085779492,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642206733"},{"type":"electronic","value":"9783642206740"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-20674-0_8","type":"book-chapter","created":{"date-parts":[[2011,4,20]],"date-time":"2011-04-20T06:06:05Z","timestamp":1303279565000},"page":"112-129","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Model Checking the Knowledge in Herbivore Protocol"],"prefix":"10.1007","author":[{"given":"Xiangyu","family":"Luo","sequence":"first","affiliation":[]},{"given":"Kaile","family":"Su","sequence":"additional","affiliation":[]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[]},{"given":"Lijun","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Jinji","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Goel, S., Robson, M., Polte, M., Sirer, E.G.: Herbivore: A Scalable and Efficient Protocol for Anonymous Communication. Technical Report TR2003-1890, Cornell Univeristy Computing and Information Science (2003)"},{"key":"#cr-split#-8_CR2.1","doi-asserted-by":"crossref","unstructured":"Halpern, J., Vardi, M.Y.: Model Checking vs. Theorem Proving: A Manifesto. Technical Report, IBM Almaden Research Center(1991);","DOI":"10.1016\/B978-0-12-450010-5.50015-3"},{"key":"#cr-split#-8_CR2.2","unstructured":"An extended version of a paper in Proc. 2nd Int. Conf. on Principles of Knowledge Representation and Reasoning (1991)"},{"issue":"2","key":"8_CR3","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":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"8_CR5","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. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 450\u2013454. Springer, Heidelberg (2006)"},{"key":"8_CR6","unstructured":"Su, K.: Model Checking Temporal Logics of Knowledge in Distributed Systems. In: Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, pp. 98\u2013103. AAAI Press \/ The MIT Press (2004)"},{"issue":"4","key":"8_CR7","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1093\/comjnl\/bxm009","volume":"50","author":"K. Su","year":"2007","unstructured":"Su, K., Sattar, A., Luo, X.: Model Checking Temporal Logics of Knowledge Via OBDDs. The Computer Journal\u00a050(4), 403\u2013420 (2007)","journal-title":"The Computer Journal"},{"key":"8_CR8","first-page":"29","volume-title":"TARK 1998: Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge","author":"K. Engelhardt","year":"1998","unstructured":"Engelhardt, K., van der Meyden, R., Moses, Y.: Knowledge and the Logic of Local Propositions. In: TARK 1998: Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge, pp. 29\u201341. Morgan Kaufmann Publishers Inc., San Francisco (1998)"},{"key":"8_CR9","unstructured":"Luo, X.: Symbolic Model Checking Multi-Agent Systems. Phd Thesis, School of Information Science and Technology, Sun Yat-sen University (2006) (in Chinese)"},{"issue":"8","key":"8_CR10","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"8_CR11","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., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT Press, Cambridge (1995)"},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"issue":"5","key":"8_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The Model Checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"8_CR15","first-page":"97","volume-title":"POPL 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on 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 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 97\u2013107. ACM Press, New York (1985)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 415\u2013427. Springer, Heidelberg (1994)"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D. Chaum","year":"1988","unstructured":"Chaum, D.: The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability. Journal of Cryptology\u00a01, 65\u201375 (1988)","journal-title":"Journal of Cryptology"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20674-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T04:48:40Z","timestamp":1741150120000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20674-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642206733","9783642206740"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20674-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}