{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:33:25Z","timestamp":1754483605591,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602187"},{"type":"electronic","value":"9783540447382"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"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":[[1995]]},"DOI":"10.1007\/3-540-60218-6_31","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:51:15Z","timestamp":1330278675000},"page":"408-422","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["On the complexity of branching modular model checking"],"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,3]]},"reference":[{"issue":"1","key":"31_CR1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems. 15(1):73\u2013132, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th LICS. pp. 428\u2013439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"31_CR3","first-page":"142","volume":"818","author":"O. Bernholtz","year":"1994","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, 1994. Full version available from authors.","journal-title":"Proc. 6th CAV, LNCS"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and I.A. Draghicescu. Expressibility results for linear-time and branching-time logics. In Proc. Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency, pp. 428\u2013437. LNCS, Springer-Verlag, 1988.","DOI":"10.1007\/BFb0013029"},{"issue":"2","key":"31_CR5","doi-asserted-by":"publisher","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, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1146\/annurev.cs.02.060187.001413","volume":"2","author":"E.M. Clarke","year":"1987","unstructured":"E.M. Clarke and O. Grumberg. Research on automatic verification of finite-state concurrent systems. In Annual Review of Computer Science, vol. 2, pp. 269\u2013290, 1987.","journal-title":"In Annual Review of Computer Science"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"E.M. 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, eds., Decade of Concurrency \u2014 Reflections and Perspectives (Proc. of REX School), LNCS, pp. 124\u2013175. Springer-Verlag, 1993. g.","DOI":"10.1007\/3-540-58043-3_19"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proc. 4th LICS, pp. 353\u2013362, 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"31_CR9","first-page":"180","volume":"430","author":"W. Damm","year":"1989","unstructured":"W. Damm, G. D\u00f6hmen, V. Gerstner, and B. Josko. Modular verification of Petri nets: the temporal logic approach. In Proc. REX Workshop, LNCS 430, pp. 180\u2013207, 1989.","journal-title":"Proc. REX Workshop, LNCS"},{"key":"31_CR10","first-page":"479","volume":"697","author":"D. Dams","year":"1993","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Generation of reduced models for checking fragments of CTL. In Proc. 5th CAV, LNCS 697, pp. 479\u2013490, 1993.","journal-title":"Proc. 5th CAV, LNCS"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. of the 29th FOCS, 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"31_CR12","unstructured":"E.A. Emerson and C.-L. Lei. Temporal model checking under generalized fairness constraints. In Proc. 18th Hawaii International Conference on System Sciences, 1985."},{"key":"31_CR13","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 logic strikes back. Science of Computer Programming, 8:275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. Handbook of theoretical computer science, pp. 997\u20131072, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"3","key":"31_CR15","doi-asserted-by":"publisher","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":"31_CR16","unstructured":"C.B. Jones. Specification and design of (parallel) programs. In R.E.A. Mason, ed., Information Processing 83: Proc. IFIP 9th World Congress, pp. 321\u2013332, North-Holland, 1983."},{"key":"31_CR17","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/3-540-51803-7_25","volume":"398","author":"B. Josko","year":"1987","unstructured":"B. Josko. MCTL \u2014 an extension of CTL for modular verification of concurrent systems. In Temporal Logic in Specification. LNCS 398, pp. 165\u2013187, 1987.","journal-title":"Temporal Logic in Specification. LNCS"},{"key":"31_CR18","first-page":"280","volume":"267","author":"B. Josko","year":"1987","unstructured":"B. Josko. Model checking of CTL formulae under liveness assumptions. In Proc. 14th ICALP, LNCS 267. pp. 280\u2013289, 1987.","journal-title":"Proc. 14th ICALP, LNCS"},{"key":"31_CR19","first-page":"386","volume":"430","author":"B. Josko","year":"1989","unstructured":"B. Josko. Verifying the correctness of AADL modules using model chekcing. In Proc. REX workshop, LNCS 430. pp. 386\u2013400, 1989.","journal-title":"Proc. REX workshop, LNCS"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"L. Lamport. Sometimes is sometimes \u201cnot never\u201d \u2014 on the temporal logic of programs. In Proc. 7th POPL, pp. 174\u2013185, 1980.","DOI":"10.1145\/567446.567463"},{"key":"31_CR21","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":"31_CR22","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 20th POPL. pp. 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"31_CR23","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/322033.322037","volume":"24","author":"N. Lynch","year":"1977","unstructured":"N. Lynch. Log space recognition and translation of parenthesis languages. J. ACM, 24:583\u2013590, 1977.","journal-title":"J. ACM"},{"key":"31_CR24","doi-asserted-by":"publisher","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":"31_CR25","doi-asserted-by":"crossref","unstructured":"D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th ICALP, 1986.","DOI":"10.1007\/3-540-16761-7_77"},{"key":"31_CR26","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. 18th FOCS, pp. 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"31_CR27","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, vol. F-13 of NATO Advanced Summer Institutes, pp. 123\u2013144, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"31_CR28","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 Symp. on Programming, LNCS 137, pp. 337\u2013351, 1981.","journal-title":"Proc. 5th Symp. on Programming, LNCS"},{"key":"31_CR29","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1\u201335, 1969.","journal-title":"Transaction of the AMS"},{"key":"31_CR30","volume-title":"PhD thesis","author":"S. Safra","year":"1989","unstructured":"S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Institute of Science, Rehovot. Israel, 1989."},{"key":"31_CR31","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W.J. Savitch","year":"1970","unstructured":"W.J. Savitch. Relationship between nondeterministic and deterministic tape complexities. J. on Computer and System Sciences, 4:177\u2013192, 1970.","journal-title":"J. on Computer and System Sciences"},{"key":"31_CR32","doi-asserted-by":"publisher","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 logic. J. ACM, 32:733\u2013749, 1985.","journal-title":"J. ACM"},{"key":"31_CR33","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. Handbook of theoretical computer science, pp. 165\u2013191, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"31_CR34","unstructured":"M.Y. Vardi. On the complexity of modular model checking. In Proc. 10th LICS, 1995."},{"key":"31_CR35","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th STOC, pp. 240\u2013251, 1985.","DOI":"10.1145\/22145.22173"},{"issue":"1","key":"31_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, 1994.","journal-title":"Information and Computation"},{"key":"31_CR37","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-51803-7_23","volume":"398","author":"P. Wolper","year":"1989","unstructured":"P. Wolper. On the relation of programs and computations to models of temporal logic. In Proc. Temporal Logic in Specification, LNCS 398, pp. 75\u2013123, 1989.","journal-title":"Proc. Temporal Logic in Specification, LNCS"}],"container-title":["Lecture Notes in Computer Science","CONCUR '95: Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60218-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:55:42Z","timestamp":1742597742000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60218-6_31"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602187","9783540447382"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-60218-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"3 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}