{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T06:25:07Z","timestamp":1794378307970,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540405245","type":"print"},{"value":"9783540450696","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45069-6_29","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T17:11:46Z","timestamp":1277226706000},"page":"288-300","source":"Crossref","is-referenced-by-count":16,"title":["Abstraction for Branching Time Properties"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, p. 23. Springer, Heidelberg (1998); Journal version in JACM","DOI":"10.1007\/3-540-49213-5_2"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 158. Springer, Heidelberg (2002)"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 260. Springer, Heidelberg (2001)"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: InVeST: A tool for the verification of invariants. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification","author":"A. Bouajjani","year":"1990","unstructured":"Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model generation. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531. Springer, Heidelberg (1990)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"I.A. Browne","year":"1995","unstructured":"Browne, I.A., Manna, Z., Sipma, H.B.: Generalized temporal verification diagrams. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026. Springer, Heidelberg (1995)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-44618-4_14","volume-title":"CONCUR 2000 - Concurrency Theory","author":"G. Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, p. 168. Springer, Heidelberg (2000)"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. TOPLAS\u00a016(5) (1994)","DOI":"10.1145\/186025.186051"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"R. Cleaveland","year":"1995","unstructured":"Cleaveland, R., Iyer, S.P., Yankelevich, D.: Optimality in abstractions of model checking. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983. Springer, Heidelberg (1995)"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE (2001)","DOI":"10.1145\/337180.337234"},{"key":"29_CR12","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1997)"},{"key":"29_CR13","unstructured":"Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology (1996)"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. TOPLAS\u00a019(2) (1997)","DOI":"10.1145\/244795.244800"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal derivation of programs. CACM\u00a018(8) (1975)","DOI":"10.1145\/360933.360975"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1993","unstructured":"Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of \u03bc-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)"},{"key":"29_CR17","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: FOCS (1991)"},{"key":"29_CR18","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, p. 426. Springer, Heidelberg (2001)"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Technical Journal\u00a05(2) (2000)","DOI":"10.1002\/bltj.2223"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation\u00a0163(1) (2000)","DOI":"10.1006\/inco.2000.3000"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A., Vardi, M.: Verification by augmented abstraction: The automata-theoretic view. JCSS 62(4) (2001)","DOI":"10.1006\/jcss.2000.1744"},{"key":"29_CR24","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the propositional mu-calculus. In: ICALP (1982)","DOI":"10.7146\/dpb.v11i146.7420"},{"key":"29_CR25","doi-asserted-by":"crossref","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems. In: STOC (1992)","DOI":"10.1145\/129712.129738"},{"key":"29_CR26","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: 2nd IJCAI (1971)"},{"key":"29_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 2. Springer, Heidelberg (2001)"},{"key":"29_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-36384-X_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.S. Namjoshi","year":"2002","unstructured":"Namjoshi, K.S.: Lifting temporal proofs through abstractions. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 174\u2013188. Springer, Heidelberg (2002)"},{"key":"29_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"29_CR30","doi-asserted-by":"crossref","unstructured":"Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. Formal Methods in System Design\u00a015(1) (1999)","DOI":"10.1023\/A:1008791913551"},{"key":"29_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages, and Programming","author":"R.S. Streett","year":"1984","unstructured":"Streett, R.S., Emerson, E.A.: The propositional mu-calculus is elementary. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol.\u00a0172, Springer, Heidelberg (1984); Full version in Inf. and Comp. 81(3), 249-264 (1989)"},{"key":"29_CR32","unstructured":"Uribe, T.E.: Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Stanford University (1999)"},{"key":"29_CR33","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: ICSE (2000)","DOI":"10.1109\/ASE.2000.873645"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45069-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,29]],"date-time":"2021-10-29T20:14:49Z","timestamp":1635538489000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45069-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405245","9783540450696"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45069-6_29","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/b11831","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}