{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:41Z","timestamp":1755217781747,"version":"3.43.0"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1023\/a:1016043502772","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T20:59:24Z","timestamp":1041109164000},"page":"193-224","source":"Crossref","is-referenced-by-count":8,"title":["Formula-Dependent Equivalence for Compositional CTL Model Checking"],"prefix":"10.1007","volume":"21","author":[{"given":"Adnan","family":"Aziz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Shiple","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vigyan","family":"Singhal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5090227_CR1","doi-asserted-by":"crossref","unstructured":"A. Aziz, T.R. Shiple, V. Singhal, and A.L. Sangiovanni-Vincentelli, \u201cFormula-dependent equivalence for compositional CTL model checking,\u201d in Proc. of the Computer Aided Verification Conf, 1994.","DOI":"10.1007\/3-540-58179-0_65"},{"key":"5090227_CR2","series-title":"Technical Report","volume-title":"Verifying interacting finite state machines","author":"A. Aziz","year":"1993","unstructured":"A. Aziz, V. Singhal, and R.K. Brayton, \u201cVerifying interacting finite state machines,\u201d Technical Report UCB\/ERL M93\/52, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, 1993."},{"key":"5090227_CR3","unstructured":"A. Bouajjani, J. Fernandez, and N. Halbwachs, \u201cMinimal model generation,\u201d in E. Clarke and R. Kurshan (Eds.), Proc. of CAV 1990, Vol. 531 of Lecture Notes in Computer Science, 1990."},{"key":"5090227_CR4","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg, \u201cCharacterizing finite Kripke structures in propositional temporal logic,\u201d Theoretical Computer Science, Vol. 59, pp. 115\u2013131, 1988.","journal-title":"Theoretical Computer Science"},{"key":"5090227_CR5","doi-asserted-by":"crossref","unstructured":"M. Chiodo, T.R. Shiple, and A.L. Sangiovanni-Vincentelli, \u201cAutomatic compositional minimization in CTL model checking,\u201d in Proc. Intl. Conf. on Computer-Aided Design, 1992, pp. 172\u2013178.","DOI":"10.1109\/ICCAD.1992.279379"},{"issue":"2","key":"5090227_CR6","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla, \u201cAutomatic verification of finite-state concurrent systems using temporal logic specifications,\u201d ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, pp. 244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5090227_CR7","unstructured":"E.M. Clarke, D.E. Long, and K.L. McMillan, \u201cCompositional model checking,\u201d in 4th Annual Symposium on Logic in Computer Science. Asilomar, CA, 1989."},{"key":"5090227_CR8","doi-asserted-by":"crossref","unstructured":"D. Dams, O. Gr\u00fcmberg, and R. Gerth, \u201cGeneration of reduced models for fragments of CTL,\u201d in Proc. of the Computer Aided Verification Conf, 1993.","DOI":"10.1007\/3-540-56922-7_39"},{"key":"5090227_CR9","unstructured":"C. Eisner, D. Geist, I. Beer, and R. Gerwitzmann, \u201cIndustrial strength formal verification,\u201d in Computer Aided Verification, Vol. 818 of Lecture Notes in Computer Science, 1994."},{"key":"5090227_CR10","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, \u201cTemporal and modal logic,\u201d in J. van Leeuwen (Ed.), Formal Models and Semantics, Vol. B of Handbook of Theoretical Computer Science. Elsevier Science, 1990, pp. 996\u20131072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"5090227_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C.L. Lei, \u201cModalities for model checking: Branching time strikes back,\u201d in Proc. ACM Symposium on Principles of Programming Languages, 1985, pp. 84\u201396.","DOI":"10.1145\/318593.318620"},{"issue":"3","key":"5090227_CR12","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D. Long, \u201cModel checking and modular verification,\u201d ACM Transactions on Programming Languages and Systems, Vol. 16, No. 3, pp. 843\u2013871, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5090227_CR13","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long, \u201cModel checking and modular verification,\u201d in J.C.M. Baeten and J.F. Groote (Eds.), Proc. ofCONCUR'91: 2nd Inter. Conf. on Concurrency Theory,Vol. 527 of Lecture Notes in Computer Science, 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"5090227_CR14","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner, Communication and Concurrency, New York, Prentice Hall, 1989."},{"key":"5090227_CR15","doi-asserted-by":"crossref","unstructured":"T.R. Shiple, R. Hojati, A.L. Sangiovanni-Vincentelli, and R.K. Brayton, \u201cHeuristic minimization of BDDs using don't cares,\u201d in Proc. of the Design Automation Conf., San Diego, CA, 1994.","DOI":"10.1145\/196244.196360"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016043502772.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1016043502772\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016043502772.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:07:39Z","timestamp":1754420859000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1016043502772"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5090227"],"URL":"https:\/\/doi.org\/10.1023\/a:1016043502772","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}