{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:24:07Z","timestamp":1725891847949},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_25","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"322-336","source":"Crossref","is-referenced-by-count":11,"title":["Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise"],"prefix":"10.1007","author":[{"given":"Harald","family":"Fecher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Huth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"5","key":"25_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, Th.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM\u00a049(5), 672\u2013713 (2002)","journal-title":"Journal of the ACM"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T.. Ball","year":"2001","unstructured":"Ball, Th., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G. Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 274\u2013287. Springer, Heidelberg (1999)"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 244\u2013263. Springer, Heidelberg (1982)"},{"issue":"5","key":"25_CR5","doi-asserted-by":"publisher","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 TOPLAS\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM TOPLAS"},{"key":"25_CR6","first-page":"238","volume-title":"Proc. of POPL 1977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs. In: Proc. of POPL 1977, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"25_CR7","unstructured":"Dams, D.: Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands (1996)"},{"issue":"2","key":"25_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM TOPLAS\u00a019(2), 253\u2013291 (1997)","journal-title":"ACM TOPLAS"},{"key":"25_CR9","unstructured":"Dams, D., Gerth, R., Grumberg, O.: A Heuristic for the Automatic Generation of Ranking Functions. In: Proc. of the Workshop on Advances in Verification, Chicago (July 2000)"},{"key":"25_CR10","first-page":"335","volume-title":"Proc. of LICS 2004","author":"D. Dams","year":"2004","unstructured":"Dams, D., Namjoshi, K.: The Existence of Finite Abstractions for Branching Time Model Checking. In: Proc. of LICS 2004, pp. 335\u2013344. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-30579-8_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Dams","year":"2005","unstructured":"Dams, D., Namjoshi, K.S.: Automata as Abstractions. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 216\u2013232. Springer, Heidelberg (2005)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-540-24730-2_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Fang","year":"2004","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with Incomprehensible Ranking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 482\u2013496. Springer, Heidelberg (2004)"},{"key":"25_CR13","unstructured":"Fecher, H., Huth, M.: Complete abstractions through extensions of disjunctive modal transition systems. Technical Report No.\u00a00604, Institut f\u00fcr Informatik und Praktische Mathematik der Christian-Albrechts-Universit\u00e4t zu Kiel, 31 pages (March 2006)"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based Model Checking using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001 and ETAPS 2001. LNCS, vol.\u00a02028, pp. 155\u2013169. Springer, Heidelberg (2001)"},{"issue":"1","key":"25_CR17","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by Augmented Finitary Abstraction. Inf.\u00a0Comput.\u00a0163(1), 203\u2013243 (2000)","journal-title":"Inf.\u00a0Comput."},{"key":"25_CR18","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-31980-1_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: Complementation Constructions for Nondeterministic Automata on Infinite Words. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 206\u2013221. Springer, Heidelberg (2005)"},{"key":"25_CR20","first-page":"203","volume-title":"Proc. of LICS 1988","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: Proc. of LICS 1988, pp. 203\u2013210. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"25_CR21","first-page":"108","volume-title":"Proc. of LICS 1990","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G., Xinxin, L.: Equation Solving Using Modal Transition Systems. In: Proc. of LICS 1990, pp. 108\u2013117. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-45069-6_29","volume-title":"Computer Aided Verification","author":"K. Namjoshi","year":"2003","unstructured":"Namjoshi, K.: Abstraction for Branching Time Properties. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 288\u2013300. Springer, Heidelberg (2003)"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D.M.R. Park","year":"1981","unstructured":"Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proc. of the 5th International Symposium on Programming (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"issue":"2","key":"25_CR25","doi-asserted-by":"crossref","first-page":"359","DOI":"10.36045\/bbms\/1102714178","volume":"8","author":"T.. Wilke","year":"2001","unstructured":"Wilke, Th.: Alternating tree automata, parity games, and modal \u03bc-calculus. Bull. Soc. Math. Belg.\u00a08(2), 359\u2013391 (2001)","journal-title":"Bull. Soc. Math. Belg."}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,9]],"date-time":"2023-05-09T07:48:42Z","timestamp":1683618522000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11901914_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}