{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T20:19:59Z","timestamp":1729628399554,"version":"3.28.0"},"reference-count":30,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/memcod.2005.1487911","type":"proceedings-article","created":{"date-parts":[[2005,7,27]],"date-time":"2005-07-27T13:52:28Z","timestamp":1122472348000},"page":"166-175","source":"Crossref","is-referenced-by-count":0,"title":["Refinemant verification of fair transition systems can contribute to PLTL model checking"],"prefix":"10.1109","author":[{"given":"F.","family":"Bellegarde","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Chouali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Julliand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"journal-title":"Design and Validation of Computer Protocols","year":"1991","author":"holzmann","key":"19"},{"key":"17","first-page":"273","article-title":"Fair simulation","volume":"1243","author":"henzinger","year":"1997","journal-title":"LNCS"},{"key":"18","first-page":"396","article-title":"Efficient omega-regular language containement","author":"hojati","year":"1992","journal-title":"CAV'92"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"16","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1023\/A:1008727508722","article-title":"A new heuristic for bad cycle detection using BDDs","volume":"18","author":"hardin","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"13","first-page":"2","article-title":"Simple on-the-fly automatic verification of linear temporal logic","author":"gerth","year":"1995","journal-title":"Proc If IP- WG6 1 Symposium on Protocols Specification Testing and Verification (PSTV95)"},{"key":"14","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1145\/318774.319268","article-title":"Checking progress with action priority: Is it fair?","author":"giannakopoulou","year":"1999","journal-title":"ESEC \/ SIGSOFT FSE"},{"key":"11","first-page":"420","article-title":"Is there a best symbolic cycle-detection algorithm?","author":"fisler","year":"2001","journal-title":"TAC AS"},{"key":"12","first-page":"53","article-title":"Fast LTL to Bu?chi automata translation","volume":"2102","author":"gastin","year":"2001","journal-title":"LNCS"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-4342-y"},{"key":"20","first-page":"1","article-title":"Algorithmic verification of linear temporal logic specifications","volume":"1443","author":"kesten","year":"1998","journal-title":"LNCS"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_84"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020383505582"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"27","first-page":"39","article-title":"Improving automata generation for linear temporal logic by considering the automaton hierarchy","author":"schneider","year":"2001","journal-title":"LPAR"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"journal-title":"Contribution du Raffinement A? la Ve?rification de Syste?mes Sous Hypothe?ses D'e?quite?","year":"2003","author":"chouali","key":"3"},{"key":"2","first-page":"83","article-title":"Introducing dynamic constraints in B","volume":"1393","author":"abrial","year":"1998","journal-title":"LNCS"},{"key":"10","article-title":"European standard - Identification cards - Integrated circuit(s) card with contacts - Electronic signal and transmission protocols","volume":"iso cei 7816 3","author":"europe?en de normalisation","year":"1992","journal-title":"Technical Report"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"30","first-page":"332","article-title":"An automata-theoric approach to automatic program verification","author":"vardi","year":"1986","journal-title":"1 St IEEE Symp LICS'86"},{"key":"7","first-page":"255","article-title":"Checking for language inclusion using simulation relation","volume":"575","author":"dill","year":"1991","journal-title":"LNCS"},{"key":"6","first-page":"249","article-title":"Improved automata generation for linear temporal logic","author":"daniele","year":"1999","journal-title":"CA 99"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"4","article-title":"PLTL partioned model checking for reactive systems under fairness assumptions","author":"chouali","year":"2004","journal-title":"Int Journal ACM TECS"},{"key":"9","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","article-title":"Optimizing Biichi automata","author":"etessami","year":"2000","journal-title":"CONCUR'2000"},{"key":"8","first-page":"267","article-title":"Efficient model checking in fragments of the prepositional mu-calculus (extended abstract)","author":"emerson","year":"1986","journal-title":"LICS"}],"event":{"name":"Third ACM & amp; IEEE International Conference on Formal Methods and Models for Co-Design","acronym":"MEMCOD-05","location":"Verona, Italy"},"container-title":["Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9956\/32009\/01487911.pdf?arnumber=1487911","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T17:36:15Z","timestamp":1497634575000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1487911\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/memcod.2005.1487911","relation":{},"subject":[]}}