{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T18:08:54Z","timestamp":1729620534267,"version":"3.28.0"},"reference-count":53,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008,11]]},"DOI":"10.1109\/fmcad.2008.ecp.16","type":"proceedings-article","created":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T16:36:21Z","timestamp":1228149381000},"page":"1-8","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking Nash Equilibria in MAD Distributed Systems"],"prefix":"10.1109","author":[{"given":"Federico","family":"Mari","sequence":"first","affiliation":[]},{"given":"Igor","family":"Melatti","sequence":"additional","affiliation":[]},{"given":"Ivano","family":"Salvo","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[]},{"given":"Lorenzo","family":"Alvisi","sequence":"additional","affiliation":[]},{"given":"Allen","family":"Clement","sequence":"additional","affiliation":[]},{"given":"Harry","family":"Li","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"35","first-page":"77","article-title":"model checking games for the alternation free -calculus and alternating automata","volume":"1705","author":"leucker","year":"1999","journal-title":"LNAI"},{"key":"36","article-title":"bar gossip","author":"li","year":"2006","journal-title":"Proceedings of OSDI'06"},{"key":"33","article-title":"verification of multi-agent systems via unbounded model checking","author":"kacprzak","year":"2004","journal-title":"Proc AAMAS 04"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"39","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1093\/logcom\/12.4.623","article-title":"model checking games for branching time logics","volume":"12","author":"stirling","year":"2002","journal-title":"Journal of Logic and Computation"},{"key":"37","first-page":"29","article-title":"a cooperative internet backup scheme","author":"lillibridge","year":"2003","journal-title":"Proc ATEC'03"},{"key":"38","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160660"},{"key":"43","first-page":"141","article-title":"automated analysis of cryptographic protocols using murphi","author":"mitchell","year":"1997","journal-title":"Proc SPIE 97"},{"year":"0","key":"42"},{"key":"41","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945451"},{"key":"40","first-page":"231","article-title":"sustaining cooperation in multi-hop wireless networks","author":"mahajan","year":"2005","journal-title":"Proc of NSDI'05"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"year":"0","key":"23"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007445"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/1011767.1011770"},{"journal-title":"Game Theory","year":"1991","author":"fudenberg","key":"26"},{"year":"0","key":"27"},{"year":"0","key":"28"},{"journal-title":"Gear web page","year":"0","key":"29"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/TAP.1968.1139250"},{"key":"2","first-page":"156","article-title":"realizability and synthesis of reactive modules","author":"anuchitanukul","year":"1994","journal-title":"Proc CAV 94"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095816"},{"key":"7","first-page":"519","article-title":"model checking security protocols using a logic of belief","author":"benerecetti","year":"2000","journal-title":"Proc of TACAS'00"},{"key":"30","article-title":"automata, logics, and infinite games: a guide to current research [outcome of a dagstuhl seminar, february 2001]","volume":"2500","year":"2002","journal-title":"LNCS"},{"key":"6","article-title":"pstore: a secure peer-to-peer backup system","author":"batten","year":"2002","journal-title":"Technical Memo MI-TLCS-TM-632 Massachusetts Institute of Technology Laboratory for Computer Science"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.07.030"},{"key":"32","first-page":"62","article-title":"pushdown processes: games and model checking","volume":"1102","author":"walukiewicz","year":"1996","journal-title":"Proc CAV 96"},{"year":"0","key":"4"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055082"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_10"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35533-7_25"},{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/1250910.1250962"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945458"},{"journal-title":"CUDD Web Page","year":"2004","key":"18"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2008.4630097"},{"key":"16","article-title":"incentives build robustness in bittorrent","author":"cohen","year":"2003","journal-title":"Proc of IPTPS'03"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1016\/j.geb.2009.05.004"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"14"},{"year":"0","key":"11"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-44641-7_7"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1111\/1467-937X.t01-1-00023"},{"year":"0","key":"20"},{"key":"49","doi-asserted-by":"publisher","DOI":"10.1145\/1011767.1011781"},{"journal-title":"What good are models and what models are good","year":"1993","author":"schneider","key":"48"},{"key":"45","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/301250.301287","article-title":"algorithmic mechanism design (extended abstract)","author":"nisan","year":"1999","journal-title":"Proc STOC 99"},{"key":"44","first-page":"201","article-title":"finite-state analysis of ssl 3.0","author":"mitchell","year":"1998","journal-title":"Seventh USENIX Security Symposium"},{"key":"47","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"journal-title":"NuSMV Web Page","year":"2006","key":"46"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"51","first-page":"58","article-title":"infinite games and verification (extended abstract of a tutorial)","author":"thomas","year":"2002","journal-title":"Proc of CAV'02"},{"key":"52","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.1996.572981"},{"key":"53","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.1998.730577"},{"key":"50","first-page":"1","article-title":"on the synthesis of strategies in infinite games","author":"thomas","year":"1995","journal-title":"Symposium on Theoretical Aspects of Computer Science"}],"event":{"name":"2008 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2008,11,17]]},"location":"Portland, OR, USA","end":{"date-parts":[[2008,11,20]]}},"container-title":["2008 Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4689158\/4689159\/04689175.pdf?arnumber=4689175","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,18]],"date-time":"2017-06-18T10:13:47Z","timestamp":1497780827000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4689175\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11]]},"references-count":53,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2008.ecp.16","relation":{},"subject":[],"published":{"date-parts":[[2008,11]]}}}