{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:40:57Z","timestamp":1725493257654},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_31","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T06:37:12Z","timestamp":1192862232000},"page":"483-500","source":"Crossref","is-referenced-by-count":4,"title":["Model Checking on Product Structures"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Schneider","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"31_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In D. Kozen, editor, Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52\u201371, Yorktown Heights, New York, May 1981. Springer-Verlag."},{"key":"31_CR2","first-page":"46","volume":"18","author":"A. Pnueli","year":"1977","unstructured":"A. Pnueli. The temporal logic of programs. In Symposium on Foundations of Computer Science, volume 18, pages 46\u201357, New York, 1977. IEEE.","journal-title":"Symposium on Foundations of Computer Science"},{"issue":"1","key":"31_CR3","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern. \u201csometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151\u2013178, January 1986.","journal-title":"Journal of the ACM"},{"key":"31_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993."},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"A. Aziz, F. Balarin, S.-T. Cheng, R. Hojati, T. Kam, S.C. Krishnan, R.K. Ranjan, T.R. Shiple, V. Singhal, S. Tasiran, H.-Y. Wang, R.K. Brayton, and A.L. Sangiovanni-Vincentelli. HSIS: A BDD-Based Environment for Formal Verification. In ACM\/IEEE Design Automation Conference (DAC), San Diego, CA, June 1994. San Diego Convention Center.","DOI":"10.1145\/196244.196467"},{"key":"31_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-60045-0_40","volume-title":"Conference on Computer Aided Verification (CAV)","author":"J. Dingel","year":"1995","unstructured":"J. Dingel and T. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In P. Wolper, editor, Conference on Computer Aided Verification (CAV), volume 939 of Lecture Notes in Computer Science, pages 54\u201369, Liege, Belgium, July 1995. Springer Verlag."},{"issue":"2","key":"31_CR7","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. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"31_CR8","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logics. Journal of Assoc. Comput. Mach., 32(3):733\u2013749, July 1985.","journal-title":"Journal of Assoc. Comput. Mach."},{"key":"31_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Conference on Computer Aided Verification (CAV)","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In David L. Dill, editor, Conference on Computer Aided Verification (CAV), volume 818 of Lecture Notes in Computer Science, pages 415\u2013427, Standford, California, USA, June 1994. Springer-Verlag."},{"key":"31_CR10","first-page":"119","volume":"28","author":"P. Wolper","year":"1985","unstructured":"P. Wolper. The tableau method for temporal logic: An overview. Logique et Analyse, 28:119\u2013136, 1985.","journal-title":"Logique et Analyse"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Temporal Logic in Specification, pages 75\u2013123, Altrincham, UK, 1987. Springer-Verlag.","DOI":"10.1007\/3-540-51803-7_23"},{"key":"31_CR12","first-page":"332","volume-title":"IEEE Symposium on Logic in Computer Science (LICS)","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verifi-cation. In IEEE Symposium on Logic in Computer Science (LICS), pages 332\u2013344. IEEE Computer Society Press, D.C., June 1986."},{"key":"31_CR13","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":"31_CR14","doi-asserted-by":"crossref","unstructured":"A. Valmari. A Stubborn Attack on the State Explosion Problem. In P. Kurshan and.M. larkes editor Workshop on Computer Aided Verification (CAV), June 1990.","DOI":"10.1090\/dimacs\/003\/04"},{"issue":"2","key":"31_CR15","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01383879","volume":"2","author":"P. Godefroid","year":"1993","unstructured":"P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149\u2013164, April 1993.","journal-title":"Formal Methods in System Design"},{"key":"31_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Conference on Computer Aided Verification (CAV)","author":"D. Peled","year":"1994","unstructured":"D. Peled. Combining partial order reductions with on-the-fly model-checking. In David L.Dill, editor, Conference on Computer Aided Verification (CAV), volume 818 of Lecture Notes in Computer Science, pages 377\u2013390, Standford, California, USA, June 1994. Springer-Verlag."},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"K. Schneider. CTL and equivalent sublanguages of CTL*. In C. Delgado Kloos, editor, IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL), pages 40\u201359, Toledo,Spain, April 1997. IFIP, Chapman and Hall.","DOI":"10.1007\/978-0-387-35064-6_4"},{"key":"31_CR18","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall International, London, 1989."},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science, 59(1\u20132), July 1988.","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"A. Aziz, V. Singhal, F. Balarin, R.K. Brayton, and A.L. Sangiovanni-Vincentelli. Equivalences for fair kripke structures. In International Colloquium on Automata, Languages and Programming (ICALP), Jerusalem, Israel, July 1994.","DOI":"10.1007\/3-540-58201-0_82"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back. In ACM Symposium on Principles of Programming Languages (POPL), pages 84\u201396, New York, January 1985. ACM.","DOI":"10.1145\/318593.318620"},{"key":"31_CR22","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back. Science of Computer Programming, 8:275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"issue":"5","key":"31_CR23","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM Transactions on Programming Languages and systems"},{"key":"31_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0028174","volume-title":"A Decade of Concurrency-Reflections and Perspectives","author":"E. Clarke","year":"1993","unstructured":"E. Clarke, O. Grumberg, and D. Long. Verification Tools for Finite State Concurrent Systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency-Reflections and Perspectives, volume 803 of Lecture Notes in Computer Science, pages 124\u2013175, Noordwijkerhout, Netherlands, June 1993. REX School\/Symposium, Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,25]],"date-time":"2021-08-25T20:17:26Z","timestamp":1629922646000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_31","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}