{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T15:58:46Z","timestamp":1769788726564,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705826","type":"print"},{"value":"9783540705833","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70583-3_30","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"361-372","source":"Crossref","is-referenced-by-count":14,"title":["Open Implication"],"prefix":"10.1007","author":[{"given":"Karin","family":"Greimel","sequence":"first","affiliation":[]},{"given":"Roderick","family":"Bloem","sequence":"additional","affiliation":[]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[]},{"given":"Moshe","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Bloem, R., Gabow, H., Somenzi, F.: An algorithm for strongly connected component analysis in nlogn symbolic steps. Formal Methods in System Design (2006)","DOI":"10.1007\/s10703-006-4341-z"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: A case study. In: DATE (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification, pp. 3\u201316 (2007)","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"1999","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633. Springer, Heidelberg (1999)"},{"key":"30_CR5","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: International Congress on Logic, Methodology, and Philosophy of Science (1962)"},{"key":"30_CR6","volume-title":"A Practical Introduction to PSL","author":"C. Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Heidelberg (2006)"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs (extended abstract). In: Proc.\u00a0Foundations of Computer Science (1988)","DOI":"10.1109\/SFCS.1988.21949"},{"key":"30_CR8","unstructured":"Greimel, K.: Open implication. Master\u2019s thesis, Graz University of Technology (2007)"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Logics and Models of Concurrent Systems, pp. 477\u2013498 (1985)","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: 6th Conference on Formal Methods in Computer Aided Design (FMCAD 2006), pp. 117\u2013124 (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Computer Aided Verification, pp. 258\u2013262 (2007)","DOI":"10.1007\/978-3-540-73368-3_29"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"King, V., Kupferman, O., Vardi, M.Y.: On the complexity of parity word automata. In: Foundations of Software Science and Computation Structures (2001)","DOI":"10.1007\/3-540-45315-6_18"},{"key":"30_CR13","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 31\u201344. Springer, Heidelberg (2006)"},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Relating linear and branching model checking. In: IFIP Working Conference on Programming Concepts and Methods (1998)","DOI":"10.1007\/978-0-387-35358-6_21"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Symposium on Foundations of Computer Science (FOCS 2005), pp. 531\u2013542 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"30_CR17","unstructured":"McIsaac, A.: Personal Communication (November 2006)"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: Logic in Computer Science (LICS 2006), pp. 255\u2013264 (2006)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"30_CR19","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Proc.\u00a0Verification, Model Checking and Abstract Interpretation, pp. 364\u2013380 (2006)","DOI":"10.1007\/11609773_24"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: IEEE Symposium on Foundations of Computer Science, Providence, RI, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. Symposium on Principles of Programming Languages (POPL 1989), pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"30_CR22","volume-title":"Regional Conference Series in Mathematics","author":"M.O. Rabin","year":"1972","unstructured":"Rabin, M.O.: Automata on Infinite Objects and Church\u2019s Problem. In: Regional Conference Series in Mathematics. American Mathematical Society, Providence (1972)"},{"key":"30_CR23","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)"},{"issue":"2","key":"30_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":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences\u00a04(2), 177\u2013192 (1970)","journal-title":"Journal of Computer and System Sciences"},{"key":"30_CR25","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"3","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal of the ACM\u00a03, 733\u2013749 (1985)","journal-title":"Journal of the ACM"},{"key":"30_CR26","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. Theoretical Computer Science (1987)"},{"key":"30_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115, 1\u201337 (1994)","journal-title":"Information and Computation"},{"issue":"2","key":"30_CR28","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Sciences\u00a032(2), 182\u2013221 (1986)","journal-title":"Journal of Computer and System Sciences"},{"key":"30_CR29","doi-asserted-by":"crossref","unstructured":"Yoshiura, N.: Finding the causes of unrealizability of reactive system formal specifications. In: Proc. Software Engineering and Formal Methods (SEFM 2004) (2004)","DOI":"10.1109\/SEFM.2004.1347501"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70583-3_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:07:59Z","timestamp":1605744479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70583-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705826","9783540705833"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70583-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}