{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:27:57Z","timestamp":1761596877177,"version":"3.28.0"},"reference-count":44,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1109\/lics.2004.1319628","type":"proceedings-article","created":{"date-parts":[[2004,11,13]],"date-time":"2004-11-13T00:14:14Z","timestamp":1100304854000},"page":"335-344","source":"Crossref","is-referenced-by-count":29,"title":["The existence of finite abstractions for branching time model checking"],"prefix":"10.1109","author":[{"given":"D.","family":"Dams","sequence":"first","affiliation":[]},{"given":"K.S.","family":"Namjoshi","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","article-title":"Branching time and abstraction in bisimulation semantics","volume":"89","author":"glabbeek","year":"1989","journal-title":"Information Processing"},{"key":"35","article-title":"An algebraic definition of simulation between programs","author":"milner","year":"1971","journal-title":"IJCAI III"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90036-0"},{"key":"36","article-title":"Certifying model checkers","volume":"2102","author":"namjoshi","year":"2001","journal-title":"CAV Vol 2102 of LNCS"},{"key":"18","article-title":"On model-checking for fragments of ?-calculus","volume":"697","author":"emerson","year":"1993","journal-title":"CAV Vol 697 of LNCS"},{"key":"33","article-title":"A compositional theory of refinement for branching time","author":"manolios","year":"2003","journal-title":"CHARME"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932512"},{"key":"16","article-title":"Efficient model checking in fragments of the propositional mu-calculus","author":"emerson","year":"1986","journal-title":"LICS"},{"key":"39","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"13","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-15648-8_7","article-title":"Automata, tableaux and temporal logics","volume":"193","author":"emerson","year":"1985","journal-title":"Logic of Programs Vol 193 of LNCS"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_29"},{"journal-title":"Abstract Interpretation and Partition Refinement for Model Checking","year":"1996","author":"dams","key":"11"},{"key":"38","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017309"},{"key":"12","article-title":"Three-valued abstractions of games: Uncertainty, but with precision","author":"de alfaro","year":"0","journal-title":"LICS'04"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"20","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36384-X_18","article-title":"On the expressiveness of 3-valued models","volume":"2575","author":"godefroid","year":"2003","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"43","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3550-5","author":"stirling","year":"2001","journal-title":"Modal and Temporal Properties of Processes"},{"key":"42","article-title":"Monotonic abstraction-refinement for CTL","volume":"2988","author":"shoham","year":"2004","journal-title":"TACAS Volume 2988 of LNCS"},{"key":"41","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"40","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-11494-7_22","article-title":"Specification and verification of concurrent systems in CESAR","volume":"137","author":"queille","year":"1982","journal-title":"Proc of the 5th International Symposium on Programming Vol 137 of LNCS"},{"journal-title":"Abstraction-based Deductive-algorithmic Verification of Reactive Systems","year":"1999","author":"uribe","key":"44"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1972.28"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004268"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.3000"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1744"},{"key":"27","article-title":"Modular model checking","volume":"1536","author":"kupferman","year":"1997","journal-title":"COMPOS Vol 1536 of LNCS"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5119"},{"volume":"49","journal-title":"J ACM","year":"2002","key":"3"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1997.646098"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"1","article-title":"Alternating refinement relations","volume":"1466","author":"alur","year":"1998","journal-title":"CONCUR Vol 1466 of LNCS"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113738"},{"key":"7","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"clarke","year":"1981","journal-title":"Workshop on Logics of Programs Vol 131 of LNCS"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932516"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567082"},{"key":"5","article-title":"Model checking partial state spaces with 3-valued temporal logics","volume":"1633","author":"bruns","year":"1999","journal-title":"CAV Vol 1633 of LNCS"},{"key":"31","article-title":"The common fragment of CTL and LTL","author":"maidl","year":"2000","journal-title":"FOCS"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"8","article-title":"Optimally in abstractions of model checking","volume":"983","author":"cleaveland","year":"1995","journal-title":"SAS Vol 983 of LNCS"}],"event":{"name":"Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.","start":{"date-parts":[[2004,7,17]]},"location":"Turku, Finland","end":{"date-parts":[[2004,7,17]]}},"container-title":["Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9221\/29239\/01319628.pdf?arnumber=1319628","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T11:53:02Z","timestamp":1497613982000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1319628\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"references-count":44,"URL":"https:\/\/doi.org\/10.1109\/lics.2004.1319628","relation":{},"subject":[],"published":{"date-parts":[[2004]]}}}