{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T03:46:34Z","timestamp":1743047194535,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614746"},{"type":"electronic","value":"9783540685999"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_61","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:43:02Z","timestamp":1330274582000},"page":"99-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["HORNSAT, model checking, verification and games"],"prefix":"10.1007","author":[{"given":"Sandeep K.","family":"Shukla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"suffix":"Jr","given":"Harry B.","family":"Hunt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel J.","family":"Rosenkrantz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H. R. Andersen","year":"1994","unstructured":"H. R. Andersen. Model checking and boolean graphs. Theoretical Computer Science, 126(1):3\u201330, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"9_CR2","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/2157.322404","volume":"30","author":"G. Ausiello","year":"1983","unstructured":"G. Ausiello, A. D'Atri, and D. Sacca. Graph algorithms for functional dependency manipulation. Journal of Association for Computing Machinery, 30(4):752\u2013766, Oct 1983.","journal-title":"Journal of Association for Computing Machinery"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0743-1066(91)90006-B","volume":"10","author":"G. Ausiello","year":"1991","unstructured":"G. Ausiello and G. F. Italiano. On-line algorithms for polynomially solvable satisfiability problems. Journal of Logic Programming, 10:69\u201390, 1991.","journal-title":"Journal of Logic Programming"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1145\/320613.320614","volume":"5","author":"C. Beeri","year":"1980","unstructured":"C. Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Transactions on Database Systems, 5:241\u2013259, 1980.","journal-title":"ACM Transactions on Database Systems"},{"key":"9_CR5","unstructured":"G. Bhat, R. Cleaveland, and O. Grumberg. Efficient on-the-fly model checking for ctl. In Proceedings of IEEE Symposium on Logic In Computer Science' 95, 1995."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"J. C. Bradfield. Verifying Temporal Properties of Systems. Birkhauser, 1992.","DOI":"10.1007\/978-1-4684-6819-9"},{"key":"9_CR7","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1007\/3-540-56496-9_29","volume":"663","author":"U. Celikkan","year":"1992","unstructured":"U. Celikkan and R. Cleaveland. Generating diagnostic information for behavioral preorders. In Proceedings of Computer Aided Verification: 1992, Lecture Notes in Computer Science 663, pages 370\u2013383, 1992.","journal-title":"Lecture Notes in Computer Science"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27:725\u2013747, 1990.","journal-title":"Acta Informatica"},{"key":"9_CR9","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/3-540-56496-9_32","volume":"663","author":"R. Cleaveland","year":"1992","unstructured":"R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for modal mucalculus. In Proceedings of Computer Aided Verification: 1992, Lecture Notes in Computer Science 663, pages 410\u2013422, 1992.","journal-title":"Lecture Notes in Computer Science"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"R. Cleaveland and B. Steffen. Computing behavioural relations, logically. In ICALP, pages 127\u2013138, 1991.","DOI":"10.1007\/3-540-54233-7_129"},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"3","author":"W.F. Dowling","year":"1984","unstructured":"W.F. Dowling and J.H. Gallier. Linear time algorithm for testing the satisfiability of propositional horn formulae. Journal of Logic Programming, 3:267\u2013284, 1984.","journal-title":"Journal of Logic Programming"},{"key":"9_CR13","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/3-540-55179-4_18","volume":"575","author":"J. C. Fernandez","year":"1991","unstructured":"J. C. Fernandez and L. Mounier. On the fly verification of behavioral equivalences and preorders. In The 3rd International Workshop on Computer Aided Verification 1991, Lecture Notes in Computer Science 575, pages 181\u2013191, 1991.","journal-title":"Lecture Notes in Computer Science"},{"key":"9_CR14","unstructured":"J. F. Groote. Private communications. 1996."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"9_CR16","unstructured":"O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching time model checking. Draft, 1995."},{"key":"9_CR17","unstructured":"K. G. Larsen. Proof systems for hennessy milner logic with recursion. In CAAP'88 Lecture Notes in Computer Science 299, 1988."},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"K. G. Larsen","year":"1990","unstructured":"K. G. Larsen. Proof systems for satisfiability in hennessy-milner logic with recursion. Theoretical Computer Science, 72:265\u2013288, 1990.","journal-title":"Theoretical Computer Science"},{"key":"9_CR19","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-56496-9_4","volume":"663","author":"K. G. Larsen","year":"1992","unstructured":"K. G. Larsen. Efficient local correctness checking. In CAV 92, Lecture Notes in Computer Science 663, pages 30\u201343, 1992.","journal-title":"CAV 92, Lecture Notes in Computer Science"},{"key":"9_CR20","volume-title":"Technical report","author":"X. Liu","year":"1992","unstructured":"X. Liu. Specification and decomposition in concurrency. Technical report, Department of Mathematics and Computer Science, Aalborg University, Denmark, 1992."},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Thomas J. Schaefer. The complexity of satisfiability problems. In Tenth Annual Symposium on Theory of Computing, 1978.","DOI":"10.1145\/800133.804350"},{"key":"9_CR22","volume-title":"Research Report TR-95-8","author":"S. K. Shukla","year":"1995","unstructured":"S. K. Shukla, H. B. Hunt III, and D. J. Rosenkrantz. Hornsat, model checking, verification, and games. Research Report TR-95-8, Department of Computer Science, SUNY Albany, 1995."},{"key":"9_CR23","unstructured":"S. K. Shukla, D. J. Rosenkrantz, H. B. Hunt III, and R. E. Stearns. A hornsat based approach to the polynomial time decidability of simulation relations for finite state processes. DIMACS workshop on Satisfiability Problem: Theory and Practice, 1996."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"O. Sokolsky and S. A. Smolka. Incremental model checking in the modal mucakulus. In Proceedings of CAV'94, 1994.","DOI":"10.1007\/3-540-58179-0_67"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C. Stirling","year":"1991","unstructured":"C. Stirling and D. Walker. Local model checking in the modal mil-calculus. Theoretical Computer Science, 89:161\u2013177, 1991.","journal-title":"Theoretical Computer Science"},{"key":"9_CR26","unstructured":"Colin Stirling. Modal and temporal logics for processes. In Notes for Summer School in Logic Methods in Concurrency, pages Department of Computer Science, Aarhus University, 1993."},{"key":"9_CR27","volume-title":"Technical Report CS-R9029","author":"R.J. Glabbeek van","year":"1990","unstructured":"R.J. van Glabbeek. The linear time \u2014 branching time spectrum. Technical Report CS-R9029, Computer Science Department, CWI, Centre for Mathematics and Computer Science, Netherlands, 1990."},{"key":"9_CR28","unstructured":"M. Vardi and P. Wolper. An automata theoretic approach to automatic program verification. In Proceedings of LICS 1986, pages 332\u2013344, 1986."},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"S. Zhang, O. Sokolsky, and S. A. Smolka. On the parallel complexity of model checking in the modal mu-calculus. In Proceedings of LICS 1994, 1994.","DOI":"10.1007\/3-540-58179-0_67"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_61","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T09:03:58Z","timestamp":1580288638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_61"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_61","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"3 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}