{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T05:27:30Z","timestamp":1740806850992,"version":"3.38.0"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,12,1]],"date-time":"2010-12-01T00:00:00Z","timestamp":1291161600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci. China"],"published-print":{"date-parts":[[2011,3]]},"DOI":"10.1007\/s11704-010-0358-y","type":"journal-article","created":{"date-parts":[[2010,12,1]],"date-time":"2010-12-01T07:44:14Z","timestamp":1291189454000},"page":"14-25","source":"Crossref","is-referenced-by-count":4,"title":["Abstraction for model checking multi-agent systems"],"prefix":"10.1007","volume":"5","author":[{"given":"Conghua","family":"Zhou","sequence":"first","affiliation":[]},{"given":"Bo","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Zhifeng","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,12,1]]},"reference":[{"key":"358_CR1","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke E, Grumberg O, Peled D. Model Checking. Cambridge: MIT Press, 2000"},{"key":"358_CR2","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/B978-0-12-450010-5.50015-3","volume-title":"Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy","author":"J. Y. Halpern","year":"1991","unstructured":"Halpern J Y, Vardi M. Model checking vs. theorem proving: a manifesto. In: McCarthy J, Lifschitz V, eds. Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy. San Diego: Academic Press, 1991, 151\u2013176"},{"key":"358_CR3","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. Cambridge: MIT Press, 1995"},{"key":"358_CR4","doi-asserted-by":"crossref","unstructured":"van der Hoek W, Wooldridge M. Model checking knowledge and time. In: Proceedings of 9th International SPIN Workshop on Model Checking of Software. 2002, 95\u2013111","DOI":"10.1007\/3-540-46017-9_9"},{"issue":"4","key":"358_CR5","doi-asserted-by":"crossref","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. Computer Journal, 2007, 50(4): 403\u2013420","journal-title":"Computer Journal"},{"key":"358_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan K. Symbolic Model Checking. Norwell: Kluwer Academic Publishers, 1993"},{"issue":"02","key":"358_CR7","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3724\/SP.J.1016.2008.00245","volume":"31","author":"L. Wu","year":"2008","unstructured":"Wu L, Su J, S K. Symbolic model checking knowledge and time in multi-agent system via extended mu-calculus. Chinese Journal of Computers, 2008, 31(02): 245\u2013252 (in Chinese)","journal-title":"Chinese Journal of Computers"},{"issue":"12","key":"358_CR8","doi-asserted-by":"crossref","first-page":"2485","DOI":"10.1360\/jos172485","volume":"17","author":"X. Luo","year":"2006","unstructured":"Luo X, Su K, Yang J. Bounded model checking for temporal epistemic logic in synchronous multi-agent systems. Journal of Software, 2006, 17(12): 2485\u20132498 (in Chinese)","journal-title":"Journal of Software"},{"key":"358_CR9","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y. Symbolic model checking without BDDs. In: Proceedings of 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems. 1999, 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"issue":"2","key":"358_CR10","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0304-3975(94)90009-4","volume":"126","author":"D. Peled","year":"1994","unstructured":"Peled D, Pnueli A. Proving partial order properties. Theoretical Computer Science, 1994, 126(2): 143\u2013182","journal-title":"Theoretical Computer Science"},{"issue":"1\u20132","key":"358_CR11","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E. Emerson","year":"1996","unstructured":"Emerson E, Sistla A. Symmetry and model checking. Formal Methods in System Design, 1996, 9(1\u20132): 105\u2013131","journal-title":"Formal Methods in System Design"},{"issue":"8","key":"358_CR12","doi-asserted-by":"crossref","first-page":"1417","DOI":"10.1360\/crad20060816","volume":"43","author":"L. J. Wu","year":"2006","unstructured":"Wu L J, Su J S, Chen Q, Yang Z. Algorithm research on \u201con the fly\u201d model checking temporal logics of knowledge in multi-agent systems. Journal of Computer Research and Development, 2006, 43(8): 1417\u20131424","journal-title":"Journal of Computer Research and Development"},{"issue":"5","key":"358_CR13","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 1994, 16(5): 1512\u20131542","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"358_CR14","first-page":"167","volume":"55","author":"W. Penczek","year":"2003","unstructured":"Penczek W, Lomuscio A. Verifying epistemic properties of multi-Agent systems via bounded model checking. Fundamenta Informaticae, 2003, 55(2): 167\u2013185","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"358_CR15","doi-asserted-by":"crossref","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, 1988, 1(1): 65\u201375","journal-title":"Journal of Cryptology"},{"key":"358_CR16","doi-asserted-by":"crossref","unstructured":"Enea C, Dima C. Abstractions of multi-agent systems. In: Proceedings of 5th international Central and Eastern European conference on Multi-Agent Systems and Applications. 2007, 11\u201321","DOI":"10.1007\/978-3-540-75254-7_2"},{"key":"358_CR17","unstructured":"Cohen M, Dam M, Lomuscio A, Russo F. Abstraction in model checking multi-agent systems. In: Proceeding of 8th International Conference on Autonomous Agents and Multiagent Systems. 2009, 945\u2013952"},{"key":"358_CR18","doi-asserted-by":"crossref","unstructured":"Clarke E M, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement. In: Proceedings of 12th International Conference on Computer Aided Verification. 2000, 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"358_CR19","doi-asserted-by":"crossref","unstructured":"Clarke E M, Jha S, Lu Y, Veith H. Tree-like counterexamples in model checking. In: Proceeding of 17th IEEE Symposium on Logic in Computer Science. 2002, 19\u201329","DOI":"10.1109\/LICS.2002.1029814"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-010-0358-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-010-0358-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-010-0358-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T09:56:29Z","timestamp":1740736589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-010-0358-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,1]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,3]]}},"alternative-id":["358"],"URL":"https:\/\/doi.org\/10.1007\/s11704-010-0358-y","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"type":"print","value":"1673-7350"},{"type":"electronic","value":"1673-7466"}],"subject":[],"published":{"date-parts":[[2010,12,1]]}}}