{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:11:46Z","timestamp":1761487906512},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540747819"},{"type":"electronic","value":"9783540747826"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74782-6_6","type":"book-chapter","created":{"date-parts":[[2007,8,25]],"date-time":"2007-08-25T14:51:49Z","timestamp":1188053509000},"page":"48-59","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking and Preprocessing"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Ferrara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Liberatore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Schaerf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/3-540-58179-0_53","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1994","unstructured":"Beer, I., Ben David, S., Geist, D., Gewirtzman, R., Yoeli, M.: Methodology and system for pratical formal verification of reactive hardware. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 182\u2013193. Springer, Heidelberg (1994)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1998","unstructured":"Beer, I., Ben David, S., Landver, A.: On the fly model checking for rctl formulas. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 184\u2013194. Springer, Heidelberg (1998)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R.K. Brayton","year":"1996","unstructured":"Brayton, R.K., Hachtel, G.D., Vincetelli, A.S., Somenzi, F., Aziz, A., Cheng, S.T., Edwards, S., Khatri, S., Kukimoto, T., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: a system for verification and syntesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","first-page":"274","volume-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence","author":"T. Bylander","year":"1991","unstructured":"Bylander, T.: Complexity results for planning. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence. LNCS, pp. 274\u2013279. Morgan Kaufmann, San Mateo, CA (1991)"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0004-3702(99)00074-0","volume":"13","author":"M. Cadoli","year":"1999","unstructured":"Cadoli, M., Donini, F.M., Liberatore, P., Schaerf, M.: Space efficency of propositional knowledge representation formalisms. Journal of Artificial Intelligence Research\u00a013, 25\u201364 (1999)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0004-3702(00)00010-2","volume":"115","author":"M. Cadoli","year":"2000","unstructured":"Cadoli, M., Donini, F.M., Liberatore, P., Schaerf, M.: The size of a revised knowledge base. Artificial Intelligence\u00a0115, 1\u201331 (2000)","journal-title":"Artificial Intelligence"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1006\/inco.2001.3043","volume":"176","author":"M. Cadoli","year":"2002","unstructured":"Cadoli, M., Donini, F.M., Liberatore, P., Schaerf, M.: Preprocessing of intractable problems. Information and Computation\u00a0176, 89\u2013120 (2002)","journal-title":"Information and Computation"},{"unstructured":"Cavada, R., Cimatti, A., Jochim, C.A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV 2.4 User\u2019s Manual. IRST (2005), \n                    \n                      http:\/\/nusmv.irst.itc.it","key":"6_CR8"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2002)"},{"key":"6_CR10","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"R. Fikes","year":"1971","unstructured":"Fikes, R., Nilson, N.: Strips: a new approach to the application of theorem proving to problem solving. Artificial Intelligence\u00a02, 189\u2013209 (1971)","journal-title":"Artificial Intelligence"},{"key":"6_CR12","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, San Francisco (1979)"},{"key":"6_CR13","series-title":"CSLI Lecture Notes","volume-title":"Logics of Time and Computation","author":"R. Goldblatt","year":"1987","unstructured":"Goldblatt, R.: Logics of Time and Computation. CSLI Lecture Notes, vol.\u00a07. Center for the Study of Language and Information, Stanford (1987)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019el, Z., Kurshan, R.P.: Cospan. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 423\u2013427. Springer, Heidelberg (1996)"},{"issue":"5","key":"6_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"IBM Haifa, RuleBase User\u2019s Manual (2006), \n                    \n                      http:\/\/www.haifa.ibm.com\/projects\/verification\/Formal_Methods-Home\/index.html","key":"6_CR16"},{"issue":"2","key":"6_CR17","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata theoretic approach to branching-time model checking. Journal of ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"Journal of ACM"},{"issue":"6","key":"6_CR18","doi-asserted-by":"publisher","first-page":"1091","DOI":"10.1145\/504794.504795","volume":"48","author":"P. Liberatore","year":"2001","unstructured":"Liberatore, P.: Monotonic reductions, representative equivalence, and compilation of intractable problems. Journal of ACM\u00a048(6), 1091\u20131125 (2001)","journal-title":"Journal of ACM"},{"key":"6_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems - Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, Heidelberg (1995)"},{"key":"6_CR20","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, Boston (1993)"},{"key":"6_CR21","first-page":"46","volume-title":"FOCS 1977","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977. Proceeding of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society Press, Los Alamitos (1977)"},{"key":"6_CR22","first-page":"1","volume-title":"AiML 2002","author":"P.. Schnoebelen","year":"2002","unstructured":"Schnoebelen, P.: The complexity of temporal logic model checking. In: AiML 2002. Proceedings of the 4th Internationa Workshop in Advances in Modal Logic, vol.\u00a04, pp. 1\u201344. World Scientific Publishing, San Mateo, CA (2002)"},{"issue":"3","key":"6_CR23","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"Journal of ACM"},{"key":"6_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L.J. Stockmeyer","year":"1976","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theoretical Computer Science\u00a03, 1\u201322 (1976)","journal-title":"Theoretical Computer Science"},{"unstructured":"Villa, T., Swarny, G., Shiple, T.: VIS User\u2019s Manual. VIS Group (2004), \n                    \n                      http:\/\/vlsi.colorado.edu\/~vis\/","key":"6_CR25"}],"container-title":["Lecture Notes in Computer Science","AI*IA 2007: Artificial Intelligence and Human-Oriented Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74782-6_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:38:46Z","timestamp":1619519926000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74782-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540747819","9783540747826"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74782-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}