{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T04:13:44Z","timestamp":1758946424388},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631668"},{"type":"electronic","value":"9783540691952"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_7","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:14:43Z","timestamp":1330298083000},"page":"36-47","source":"Crossref","is-referenced-by-count":26,"title":["Module checking revisited"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Proc. 6th CAV, LNCS 818, pp. 142\u2013155, June 1994.","DOI":"10.1007\/3-540-58179-0_50"},{"key":"7_CR2","first-page":"52","volume":"131","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 Proc. LP, LNCS 131, pp. 52\u201371, 1981.","journal-title":"Proc. LP, LNCS"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and M.C. Browne. Reasoning about networks with many identical finite-state processes. In Proc. 5th PODC, pp. 240\u2013248, August 1986.","DOI":"10.1145\/10590.10611"},{"issue":"2","key":"7_CR4","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 TPLS, 8(2):244\u2013263, 1986.","journal-title":"ACM TPLS"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th FOCS, pp. 368\u2013377, October 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"7_CR6","unstructured":"E.A. Emerson and C.-L. Lei. Temporal model checking under generalized fairness constraints. In Proc. 18th Hawaii International Conference on System Sciences, Hawaii, 1985."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Automata, tableaux, and temporal logics. In Proc. LP, LNCS 193, pp. 79\u201387, 1985.","DOI":"10.1007\/3-540-15648-8_7"},{"key":"7_CR8","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-50302-1_11","volume":"331","author":"M.J. Fischer","year":"1988","unstructured":"M.J. Fischer and L.D. Zuck. Reasoning about uncertainty in fault-tolerant distributed systems. In Proc. Formal Techniques in Real-Time and Fault-Tolerant Sys., LNCS 331, pp. 142\u2013158, 1988.","journal-title":"Proc. Formal Techniques in Real-Time and Fault-Tolerant Sys., LNCS"},{"issue":"3","key":"7_CR9","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"D. Harel and A. Pnueli. On the development of reactive systems. In Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pp. 477\u2013498, 1985.","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"7_CR12","unstructured":"C.B. Jones. Specification and design of (parallel) programs. In Proc. 9th IFIP, pp. 321\u2013332, North-Holland, 1983."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th CONCUR, LNCS 962, pp. 408\u2013422, August 1995.","DOI":"10.1007\/3-540-60218-6_31"},{"key":"7_CR14","first-page":"75","volume":"1102","author":"O. Kupferman","year":"1996","unstructured":"O. Kupferman and M.Y. Vardi. Module checking. In Proc. 8th CAV, LNCS 1102, pp. 75\u201386, August 1996.","journal-title":"Proc. 8th CAV, LNCS"},{"key":"7_CR15","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM Trans. on Programming Languages and Systenms, 5:190\u2013222, 1983.","journal-title":"ACM Trans. on Programming Languages and Systenms"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th POPL, pp. 97\u2013107, January 1985.","DOI":"10.1145\/318593.318622"},{"key":"7_CR17","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd IJCAI, British Computer Society, pp. 481\u2013489, September 1971."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal specification and verification of reactive modules. 1992.","DOI":"10.1007\/978-1-4612-0931-7_3"},{"key":"7_CR19","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"D.E. Muller and P.E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54,:267\u2013276, 1987.","journal-title":"Theoretical Computer Science"},{"key":"7_CR20","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"D.E. Muller and P.E. Schupp. Simulating aternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141:69\u2013107, 1995.","journal-title":"Theoretical Computer Science"},{"key":"7_CR21","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"7_CR22","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1007\/BFb0027047","volume":"224","author":"A. Pnueli","year":"1985","unstructured":"A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Proc. Advanced School on Current Trends in Concurrency, LNCS 224, pp. 510\u2013584, 1985.","journal-title":"Proc. Advanced School on Current Trends in Concurrency, LNCS"},{"key":"7_CR23","first-page":"337","volume":"137","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, LNCS 137, pp. 337\u2013351, 1981.","journal-title":"Proc. 5th International Symp. on Programming, LNCS"},{"key":"7_CR24","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1016\/0022-0000(84)90034-5","volume":"29","author":"J.H. Reif","year":"1984","unstructured":"J.H. Reif. The complexity of two-player games of incomplete information. J. on Computer and System Sciences, 29:274\u2013301, 1984.","journal-title":"J. on Computer and System Sciences"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. On the complexity of modular model checking. In Proc. 10th LICS, June 1995.","DOI":"10.1109\/LICS.1995.523248"},{"issue":"2","key":"7_CR26","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2): 182\u2013221, April 1986.","journal-title":"Journal of Computer and System Science"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T11:39:01Z","timestamp":1640950741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}