乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:32Z","timestamp":1725540512435},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_16","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"306-325","source":"Crossref","is-referenced-by-count":8,"title":["Graded-CTL: Satisfiability and Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Ferrante","sequence":"first","affiliation":[]},{"given":"Margherita","family":"Napoli","sequence":"additional","affiliation":[]},{"given":"Mimmo","family":"Parente","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1109\/LICS.1990.113767","volume-title":"Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990), pp. 428\u2013439. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"2\/3","key":"16_CR2","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"R.I. Bahar","year":"1997","unstructured":"Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Formal Methods in System Design\u00a010(2\/3), 171\u2013206 (1997)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"16_CR3","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10703-006-4341-z","volume":"28","author":"R. Bloem","year":"2006","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. Formal Methods in System Design\u00a028(1), 37\u201356 (2006)","journal-title":"Formal Methods in System Design"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bianco, A., Mogavero, F., Murano, A.: Graded computation tree logic. In: LICS 2009 (2009)","DOI":"10.1109\/LICS.2009.28"},{"issue":"3","key":"16_CR5","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An openSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"issue":"3","key":"16_CR7","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1006\/jcss.1999.1636","volume":"59","author":"F. Corradini","year":"1999","unstructured":"Corradini, F., De Nicola, R., Labella, A.: Models of nondeterministic regular expressions. J. Comput. Syst. Sci.\u00a059(3), 412\u2013449 (1999)","journal-title":"J. Comput. Syst. Sci."},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"16_CR9","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Usig branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming\u00a02, 241\u2013266 (1982)","journal-title":"Science of Computer Programming"},{"issue":"5","key":"16_CR10","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s10009-007-0047-9","volume":"9","author":"M. Chechik","year":"2007","unstructured":"Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. International Journal on Software Tools for Technololy Transfer\u00a09(5), 429\u2013445 (2007)","journal-title":"International Journal on Software Tools for Technololy Transfer"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-44798-9_23","volume-title":"Correct Hardware Design and Verification Methods","author":"F. Copty","year":"2001","unstructured":"Copty, F., Irron, A., Weissberg, O., Kropp, N.P., Kamhi, G.: Efficient debugging in a formal verification environment. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 275\u2013292. Springer, Heidelberg (2001)"},{"key":"16_CR12","unstructured":"Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model checking and evidence exploration. In: Workshop on Model Based Development: Features, Components and Architectures (ECBS 2003), pp. 214\u2013223 (2003)"},{"issue":"4","key":"16_CR13","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E.A. Emerson","year":"1992","unstructured":"Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. Real-Time Systems\u00a04(4), 331\u2013352 (1992)","journal-title":"Real-Time Systems"},{"issue":"4","key":"16_CR14","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1305\/ndjfl\/1093890715","volume":"13","author":"K. Fine","year":"1972","unstructured":"Fine, K.: In so many possible worlds. Notre Dame Journal of Formal Logic\u00a013(4), 516\u2013520 (1972)","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-88387-6_4","volume-title":"Automated Technology for Verification and Analysis","author":"A. Ferrante","year":"2008","unstructured":"Ferrante, A., Napoli, M., Parente, M.: CTL model-checking with graded quantifiers. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 18\u201332. Springer, Heidelberg (2008)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Ferrante, A., Napoli, M., Parente, M.: Model checking for graded CTL. Fundamenta Informaticae (to appear, 2010); Journal version of [FNP 2008]","DOI":"10.3233\/FI-2009-181"},{"issue":"2","key":"16_CR17","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1006\/inco.1998.2778","volume":"150","author":"R. Gerth","year":"1999","unstructured":"Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. Information and Computation\u00a0150(2), 132\u2013152 (1999)","journal-title":"Information and Computation"},{"key":"16_CR18","unstructured":"Ganzinger, H., Meyer, C., Veanes, M.: The two\u2013variable guarded fragment with transitive relations. In: LICS, pp. 24\u201334 (1999)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BFb0023731","volume-title":"Computer-Aided Verification","author":"P. Godefroid","year":"1991","unstructured":"Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 176\u2013185. Springer, Heidelberg (1991)"},{"key":"16_CR20","unstructured":"Gr\u00e4del, E., Otto, M., Rosen, E.: Two\u2013variable logic with counting is decidable. In: LICS, pp. 306\u2013317 (1997)"},{"issue":"1","key":"16_CR21","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/s00453-007-9079-5","volume":"50","author":"R. Gentilini","year":"2007","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Symbolic graphs: Linear solutions to connectivity related problems. Algorithmica\u00a050(1), 120\u2013158 (2007)","journal-title":"Algorithmica"},{"key":"16_CR22","unstructured":"Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: KR, pp. 335\u2013346 (1991)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/11817963_28","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2006","unstructured":"Kahlon, V., Gupta, A., Sinha, N.: Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 286\u2013299. Springer, Heidelberg (2006)"},{"key":"16_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-45620-1_34","volume-title":"Automated Deduction - CADE-18","author":"O. Kupferman","year":"2002","unstructured":"Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded \u03bc\u2013calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 423\u2013437. Springer, Heidelberg (2002)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-3-540-31980-1_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W. Marrero","year":"2005","unstructured":"Marrero, W.: Using bdds to decide ctl. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 222\u2013236. Springer, Heidelberg (2005)"},{"key":"16_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"issue":"4","key":"16_CR27","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1137\/S0097539797323005","volume":"29","author":"L. Pacholski","year":"2000","unstructured":"Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first\u2013order two\u2013variable logic with counting. SIAM Journal of Computing\u00a029(4), 1083\u20131117 (2000)","journal-title":"SIAM Journal of Computing"},{"key":"16_CR28","unstructured":"Pan, G., Sattler, U., Vardi, M.Y.: Bdd-based decision procedures for the modal logic k. Journal of Applied Non-classical Logics\u00a049 (2005)"},{"key":"16_CR29","unstructured":"Somenzi, F.: Cudd: Cu decision diagram package, release 2.4.1 (2005), http:\/\/vlsi.colorado.edu\/~fabio\/CUDD"},{"issue":"1","key":"16_CR30","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1093\/logcom\/11.1.85","volume":"11","author":"S. Tobies","year":"2001","unstructured":"Tobies, S.: PSPACE reasoning for graded modal logics. Journal Log. Comput.\u00a011(1), 85\u2013106 (2001)","journal-title":"Journal Log. Comput."},{"issue":"2","key":"16_CR31","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. of Computer and System Sciences\u00a032(2), 183\u2013221 (1986)","journal-title":"J. of Computer and System Sciences"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:54:52Z","timestamp":1606186492000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}