{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:39:34Z","timestamp":1750307974877,"version":"3.41.0"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2007,9,1]],"date-time":"2007-09-01T00:00:00Z","timestamp":1188604800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGACT News"],"published-print":{"date-parts":[[2007,9]]},"DOI":"10.1145\/1324215.1324231","type":"journal-article","created":{"date-parts":[[2007,12,7]],"date-time":"2007-12-07T19:19:01Z","timestamp":1197055141000},"page":"77-99","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Symbolic model checking for temporal-epistemic logics"],"prefix":"10.1145","volume":"38","author":[{"given":"Alessio","family":"Lomuscio","sequence":"first","affiliation":[{"name":"Imperial College London, London, UK"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland and Podlasie Academy, Siedlce, Poland"}]}],"member":"320","published-online":{"date-parts":[[2007,9]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"MCK : Model checking knowledge. http:\/\/www.cse.unsw.edu.au\/~mck. MCK: Model checking knowledge. http:\/\/www.cse.unsw.edu.au\/~mck."},{"key":"e_1_2_1_2_1","unstructured":"Verics. http:\/\/verics.ipipan.waw.pl. Verics. http:\/\/verics.ipipan.waw.pl."},{"key":"e_1_2_1_3_1","volume-title":"MOCHA user manual. Technical report","author":"Alur R.","year":"2000","unstructured":"R. Alur , L. de Alfaro , T. Henzinger , S. Krishnan , F. Mang , S. Qadeer , S. Rajamani , and S. Tasiran . MOCHA user manual. Technical report , University of California at Berkeley , 2000 . http:\/\/www-cad.eecs.berkeley.edu\/~mocha\/doc\/c-doc\/c-manual.ps.gz. R. Alur, L. de Alfaro, T. Henzinger, S. Krishnan, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA user manual. Technical report, University of California at Berkeley, 2000. http:\/\/www-cad.eecs.berkeley.edu\/~mocha\/doc\/c-doc\/c-manual.ps.gz."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.759192"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/380921.380932"},{"key":"e_1_2_1_8_1","series-title":"Advances in Computers","volume-title":"Highly Dependable Software","author":"Biere A.","year":"2003","unstructured":"A. Biere , A. Cimatti , E. Clarke , O. Strichman , and Y. Zhu . Bounded model checking . In Highly Dependable Software , volume 58 of Advances in Computers . Academic Press , 2003 . Pre-print. A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. In Highly Dependable Software, volume 58 of Advances in Computers. Academic Press, 2003. Pre-print."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_2_1_10_1","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn P.","year":"2001","unstructured":"P. Blackburn , M. de Rijke , and Y. Venema . Modal Logic , volume 53 of Cambridge Tracts in Theoretical Computer Science . Cambridge University Press , 2001 . P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/54235.54239"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733923"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/647762.735503"},{"key":"e_1_2_1_17_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg , and D. Peled . Model Checking . MIT Press , 1999 . E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647763.760719"},{"key":"e_1_2_1_19_1","first-page":"278","volume-title":"Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03)","volume":"2619","author":"Dembi\u0144ski P.","year":"2003","unstructured":"P. Dembi\u0144ski , A. Janowska , P. Janowski , W. Penczek , A. P\u00f3lrola , M. Szreter , B. Wo\u017ana , and A. Zbrzezny . VerICS: A tool for verifying timed automata and Estelle specifications . In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03) , volume 2619 of LNCS, pages 278 -- 283 . Springer-Verlag , 2003 . P. Dembi\u0144ski, A. Janowska, P. Janowski, W. Penczek, A. P\u00f3lrola, M. Szreter, B. Wo\u017ana, and A. Zbrzezny. VerICS: A tool for verifying timed automata and Estelle specifications. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278--283. Springer-Verlag, 2003."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/647762.760716"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625970"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about Knowledge","author":"Fagin R.","year":"1995","unstructured":"R. Fagin , J. Y. Halpern , Y. Moses , and M. Vardi . Reasoning about Knowledge . MIT Press , Cambridge , 1995 . R. Fagin, J. Y. Halpern, Y. Moses, and M. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2778"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/79147.79161"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/132218.132228"},{"key":"e_1_2_1_28_1","volume-title":"An Introduction to the Logic of the Two Notions","author":"Hintikka J.","year":"1962","unstructured":"J. Hintikka . Knowledge and Belief , An Introduction to the Logic of the Two Notions . Cornell University Press , Ithaca (NY) and London, 1962 . J. Hintikka. Knowledge and Belief, An Introduction to the Logic of the Two Notions. Cornell University Press, Ithaca (NY) and London, 1962."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645881.672227"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_31_1","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"Huth M. R. A.","year":"2000","unstructured":"M. R. A. Huth and M. D. Ryan . Logic in Computer Science: Modelling and Reasoning about Systems . Cambridge University Press, Cambridge , England , 2000 . M. R. A. Huth and M. D. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge, England, 2000."},{"key":"e_1_2_1_32_1","volume-title":"Agents that know how to play. Fundamenta Informaticae, 63(2--3):185--219","author":"Jamroga W.","year":"2004","unstructured":"W. Jamroga and W. van der Hoek . Agents that know how to play. Fundamenta Informaticae, 63(2--3):185--219 , 2004 . W. Jamroga and W. van der Hoek. Agents that know how to play. Fundamenta Informaticae, 63(2--3):185--219, 2004."},{"key":"e_1_2_1_33_1","volume-title":"Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol. Fundamenta Informaticae, 63(2, 3):221--240","author":"Kacprzak M.","year":"2006","unstructured":"M. Kacprzak , A. Lomuscio , A. Niewiadomski , W. Penczek , F. Raimondi , and M. Szreter . Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol. Fundamenta Informaticae, 63(2, 3):221--240 , 2006 . M. Kacprzak, A. Lomuscio, A. Niewiadomski, W. Penczek, F. Raimondi, and M. Szreter. Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol. Fundamenta Informaticae, 63(2, 3):221--240, 2006."},{"key":"e_1_2_1_35_1","volume-title":"From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae, 63(2--3):221--240","author":"Kacprzak M.","year":"2004","unstructured":"M. Kacprzak , A. Lomuscio , and W. Penczek . From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae, 63(2--3):221--240 , 2004 . M. Kacprzak, A. Lomuscio, and W. Penczek. From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae, 63(2--3):221--240, 2004."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/229000.226297"},{"key":"e_1_2_1_37_1","series-title":"Acta Philosophica Fennica","volume-title":"Recent work in epistemic logic","author":"Lenzen W.","year":"1978","unstructured":"W. Lenzen . Recent work in epistemic logic , volume 30 of Acta Philosophica Fennica . North-Holland , Amsterdam , 1978 . W. Lenzen. Recent work in epistemic logic, volume 30 of Acta Philosophica Fennica. North-Holland, Amsterdam, 1978."},{"key":"e_1_2_1_38_1","first-page":"1384","volume-title":"Proceedings of the Twentieth International Joint Conference on Artificial Intelligence","author":"Lomuscio A.","year":"2007","unstructured":"A. Lomuscio , C. Pecheur , and F. Raimondi . Automatic verification of knowledge and time with NuSMV . In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence , pages 1384 -- 1389 , Hyderabad, India , January 2007 . AAAI. A. Lomuscio, C. Pecheur, and F. Raimondi. Automatic verification of knowledge and time with NuSMV. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, pages 1384--1389, Hyderabad, India, January 2007. AAAI."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160733"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_31"},{"key":"e_1_2_1_41_1","volume-title":"July","author":"Lomuscio A.","year":"2007","unstructured":"A. Lomuscio , F. Raimondi , and B. Wozna . Verification of the tesla protocol in MCMAS-X. Fundamenta Informaticae, 79(3--4):473--486 , July 2007 . A. Lomuscio, F. Raimondi, and B. Wozna. Verification of the tesla protocol in MCMAS-X. Fundamenta Informaticae, 79(3--4):473--486, July 2007."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026176900459"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160658"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2007.05.005"},{"key":"e_1_2_1_45_1","volume-title":"An approach to the state explosion problem","author":"McMillan K.","year":"1993","unstructured":"K. McMillan . Symbolic model checking : An approach to the state explosion problem . Kluwer Academic Publishers , 1993 . K. McMillan. Symbolic model checking: An approach to the state explosion problem. Kluwer Academic Publishers, 1993."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734421"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/646837.708360"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009683"},{"key":"e_1_2_1_49_1","volume-title":"Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'04)","volume":"99","author":"Nabialek W.","year":"2004","unstructured":"W. Nabialek , A. Niewiadomski , W. Penczek , A. P\u00f3lrola , and M. Szreter . VerICS 2004: A model checker for real time and multi-agent systems . In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'04) , volume 170(1) of Informatik-Berichte, pages 88-- 99 . Humboldt University , 2004 . W. Nabialek, A. Niewiadomski, W. Penczek, A. P\u00f3lrola, and M. Szreter. VerICS 2004: A model checker for real time and multi-agent systems. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'04), volume 170(1) of Informatik-Berichte, pages 88--99. Humboldt University, 2004."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/648065.747610"},{"key":"e_1_2_1_51_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of MoChArt","author":"Pecheur C.","year":"2006","unstructured":"C. Pecheur and F. Raimondi . Symbolic model checking of logics with actions . In Proceedings of MoChArt 2006 , Lecture Notes in Artificial Intelligence . Springer Verlag , August 2006. to appear. C. Pecheur and F. Raimondi. Symbolic model checking of logics with actions. In Proceedings of MoChArt 2006, Lecture Notes in Artificial Intelligence. Springer Verlag, August 2006. to appear."},{"key":"e_1_2_1_52_1","first-page":"409","volume-title":"CAV","author":"Peled D.","year":"1993","unstructured":"D. Peled . All from one, one for all: on model checking using representatives . In CAV , pages 409 -- 423 , 1993 . D. Peled. All from one, one for all: on model checking using representatives. In CAV, pages 409--423, 1993."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370935.2370943"},{"key":"e_1_2_1_54_1","series-title":"Studies in Computational Intelligence","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-32870-4","volume-title":"Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach","author":"Penczek W.","year":"2006","unstructured":"W. Penczek and A. P\u00f3lrola . Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach , volume 20 of Studies in Computational Intelligence . Springer-Verlag , 2006 . W. Penczek and A. P\u00f3lrola. Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach, volume 20 of Studies in Computational Intelligence. Springer-Verlag, 2006."},{"key":"e_1_2_1_55_1","volume-title":"Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1--2):135--156","author":"Penczek W.","year":"2002","unstructured":"W. Penczek , B. Wo\u017ana , and A. Zbrzezny . Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1--2):135--156 , 2002 . W. Penczek, B. Wo\u017ana, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1--2):135--156, 2002."},{"key":"e_1_2_1_57_1","volume-title":"Proc. of the Int. Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'03)","volume":"2003","author":"Raimondi F.","unstructured":"F. Raimondi and A. Lomuscio . A tool for specification and verification of epistemic properties of interpreted systems. In W. van der Hoek, A. Lomuscio, E. de Vink, and M. Wooldridge, editors , Proc. of the Int. Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'03) , volume 85(2) of ENTCS. Elsevier, 2003 . F. Raimondi and A. Lomuscio. A tool for specification and verification of epistemic properties of interpreted systems. In W. van der Hoek, A. Lomuscio, E. de Vink, and M. Wooldridge, editors, Proc. of the Int. Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'03), volume 85(2) of ENTCS. Elsevier, 2003."},{"key":"e_1_2_1_58_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-540-25927-5_15","volume-title":"Proceedings of DEON04, Seventh International Workshop on Deontic Logic in Computer Science","author":"Raimondi F.","year":"2004","unstructured":"F. Raimondi and A. Lomuscio . Symbolic model checking of deontic interpreted systems via OBDDs . In Proceedings of DEON04, Seventh International Workshop on Deontic Logic in Computer Science , volume 3065 of LNCS , pages 228 -- 242 . Springer Verlag , 2004 . F. Raimondi and A. Lomuscio. Symbolic model checking of deontic interpreted systems via OBDDs. In Proceedings of DEON04, Seventh International Workshop on Deontic Logic in Computer Science, volume 3065 of LNCS, pages 228--242. Springer Verlag, 2004."},{"key":"e_1_2_1_59_1","unstructured":"F. Raimondi and A. Lomuscio. http:\/\/www.cs.ucl.ac.uk\/staff\/f.raimondi\/MCMAS 2006. F. Raimondi and A. Lomuscio. http:\/\/www.cs.ucl.ac.uk\/staff\/f.raimondi\/MCMAS 2006."},{"key":"e_1_2_1_60_1","first-page":"5","article-title":"Automatic verification of multi-agent systems by model checking via OBDDs","author":"Raimondi F.","year":"2007","unstructured":"F. Raimondi and A. Lomuscio . Automatic verification of multi-agent systems by model checking via OBDDs . Journal of Applied Logic , 5 , 2007 . F. Raimondi and A. Lomuscio. Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic, 5, 2007.","journal-title":"Journal of Applied Logic"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037076"},{"key":"e_1_2_1_62_1","unstructured":"F. Somenzi. CUDD: CU decision diagram package -- release 2.4.0. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cuddIntro.html 2005. F. Somenzi. CUDD: CU decision diagram package -- release 2.4.0. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cuddIntro.html 2005."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_14"},{"key":"e_1_2_1_64_1","volume-title":"Proc. of the 3rd Int. Workshop on Constraints in Formal Verification (CFV'05)","author":"Szreter M.","year":"2006","unstructured":"M. Szreter . Generalized blocking clauses in unbounded model checking . In Proc. of the 3rd Int. Workshop on Constraints in Formal Verification (CFV'05) , 2006 . To appear in ENTCS. M. Szreter. Generalized blocking clauses in unbounded model checking. In Proc. of the 3rd Int. Workshop on Constraints in Formal Verification (CFV'05), 2006. To appear in ENTCS."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1090-9443(03)00031-0"},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of the Twenty-Second Conference on Artificial Intelligence (AAAI-07)","author":"Wooldridge M.","year":"2007","unstructured":"M. Wooldridge , T. Agotnes , P. E. Dunne , and W. van der Hoek. Logic for automated mechanism design - a progress report . In Proceedings of the Twenty-Second Conference on Artificial Intelligence (AAAI-07) , 2007 . M. Wooldridge, T. Agotnes, P. E. Dunne, and W. van der Hoek. Logic for automated mechanism design - a progress report. In Proceedings of the Twenty-Second Conference on Artificial Intelligence (AAAI-07), 2007."},{"key":"e_1_2_1_67_1","first-page":"93","volume-title":"Proc. of the 2nd Int. Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'04)","volume":"126","author":"Wo\u017ana B.","year":"2005","unstructured":"B. Wo\u017ana , A. Lomuscio , and W. Penczek . Bounded model checking for deontic interpreted systems . In Proc. of the 2nd Int. Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'04) , volume 126 of ENTCS, pages 93 -- 114 . Elsevier , 2005 . B. Wo\u017ana, A. Lomuscio, and W. Penczek. Bounded model checking for deontic interpreted systems. In Proc. of the 2nd Int. Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'04), volume 126 of ENTCS, pages 93--114. Elsevier, 2005."},{"key":"e_1_2_1_68_1","first-page":"249","volume-title":"Proc. of Int. Conf. on Computer-Aided Design (ICCAD'01)","author":"Zhang L.","year":"2001","unstructured":"L. Zhang , C. Madigan , M. Moskewicz , and S. Malik . Efficient conflict driven learning in a Boolean satisfiability solver . In Proc. of Int. Conf. on Computer-Aided Design (ICCAD'01) , pages 249 -- 285 , 2001 . L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. Efficient conflict driven learning in a Boolean satisfiability solver. In Proc. of Int. Conf. on Computer-Aided Design (ICCAD'01), pages 249--285, 2001."}],"container-title":["ACM SIGACT News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1324215.1324231","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1324215.1324231","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:58:25Z","timestamp":1750258705000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1324215.1324231"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9]]},"references-count":65,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,9]]}},"alternative-id":["10.1145\/1324215.1324231"],"URL":"https:\/\/doi.org\/10.1145\/1324215.1324231","relation":{},"ISSN":["0163-5700"],"issn-type":[{"type":"print","value":"0163-5700"}],"subject":[],"published":{"date-parts":[[2007,9]]},"assertion":[{"value":"2007-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}