{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:39Z","timestamp":1760202639804},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_60","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:37:01Z","timestamp":1330259821000},"page":"325-338","source":"Crossref","is-referenced-by-count":9,"title":["Augmenting branching temporal logics with existential quantification over atomic propositions"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli. Methodology and system for practical formal verification of reactive hardware. In Proc. 6th Workshop on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 182\u2013193, Stanford, June 1994.","DOI":"10.1007\/3-540-58179-0_53"},{"issue":"2","key":"26_CR2","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"26_CR4","volume-title":"Lecture Notes in Computer Science","author":"O. Bernholtz","year":"1994","unstructured":"O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Computer Aided Verification, Proc. 6th Int. Workshop, Stanford, California, June 1994. Lecture Notes in Computer Science, Springer-Verlag, full version available from authors."},{"issue":"2","key":"26_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, January 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"26_CR6","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114\u2013133, January 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proc. 4th IEEE Symposium on Logic in Computer Science, pages 353\u2013362, 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"26_CR8","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":"26_CR9","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 84\u201396, New Orleans, January 1985.","DOI":"10.1145\/318593.318620"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. Handbook of theoretical computer science, pages 997\u20131072, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and A. P. Sistla. Deciding branching time logic. In Proceedings of the 16th ACM Symposium on Theory of Computing, Washington, April 1984.","DOI":"10.1145\/800057.808661"},{"key":"26_CR13","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. J. of Computer and Systems Sciences, 18:194\u2013211, 1979.","journal-title":"J. of Computer and Systems Sciences"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. In Proc. 2nd Conferance on Concurrency Theory, volume 527 of Lecture Notes in Computer Science, pages 250\u2013265, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"26_CR15","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0168-0072(94)90084-1","volume":"69","author":"J.Y. Halpern","year":"1994","unstructured":"J.Y. Halpern and B. Kapron. Zero-one laws for modal logic. Annals of Pure and Applied Logic, 69:157\u2013193, 1994.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"26_CR16","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1016\/0022-0000(81)90039-8","volume":"22","author":"N. Immerman","year":"1981","unstructured":"N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, 22(3):384\u2013406, 1981.","journal-title":"Journal of Computer and System Sciences"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"O. Kupferman and A. Pnueli. Once and for all. In Proc. 10th IEEE Symposium on Logic in Computer Science, San Diego, June 1995. To appear.","DOI":"10.1109\/LICS.1995.523241"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"L. Lamport. Sometimes is sometimes \u201cnot never\u201d \u2014 on the temporal logic of programs. In Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pages 174\u2013185, January 1980.","DOI":"10.1145\/567446.567463"},{"key":"26_CR19","volume-title":"PhD thesis","author":"D.E. Long","year":"1993","unstructured":"D.E. Long. Model checking, abstraction and compositional verification. PhD thesis, Carnegie-Mellon University, Pittsburgh, 1993."},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97\u2013107, New Orleans, January 1985.","DOI":"10.1145\/318593.318622"},{"key":"26_CR21","doi-asserted-by":"publisher","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":"26_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the Sixteenth ACM Symposium on Principles of Programming Languages, Austin, Januery 1989.","DOI":"10.1145\/75277.75293"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"S. Pinter and P. Wolper. A temporal logic for reasoning about partially ordered computations. In Proc. 3rd ACM Symposium on Principles of Distributed Computing, pages 28\u201337, Vancouver, August 1984.","DOI":"10.1145\/800222.806733"},{"key":"26_CR24","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":"26_CR25","volume-title":"PhD thesis","author":"A.P. Sistla","year":"1983","unstructured":"A.P. Sistla. Theoretical issues in the design of distributed and concurrent systems. PhD thesis, Harward University, Cambridge, MA, 1983."},{"key":"26_CR26","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic. Theoretical Computer Science, 49:217\u2013237, 1987.","journal-title":"Theoretical Computer Science"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th ACM Symp. on Theory of Computing, pages 240\u2013251, 1985.","DOI":"10.1145\/22145.22173"},{"issue":"2","key":"26_CR28","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\u201321, April 1986.","journal-title":"Journal of Computer and System Science"},{"key":"26_CR29","first-page":"233","volume-title":"volume 715 of Lecture Notes in Computer Science","author":"P. Wolper","year":"1993","unstructured":"P. Wolper and P. Godefroid, Partial-order methods for temporal verification. In Proc. 4th Conferance on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 233\u2013246, Hildesheim, August 1993. Springer-Verlag."},{"issue":"1\u20132","key":"26_CR30","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1\u20132):72\u201399, 1983.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_60.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:28:56Z","timestamp":1605630536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}