{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:51:06Z","timestamp":1725490266725},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540749141"},{"type":"electronic","value":"9783540749158"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74915-8_5","type":"book-chapter","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T05:13:35Z","timestamp":1187932415000},"page":"7-22","source":"Crossref","is-referenced-by-count":4,"title":["Tightening the Exchange Rates Between Automata"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. IPL\u00a021, 181\u2013185 (1985)","journal-title":"IPL"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/11901914_12","volume-title":"Automated Technology for Verification and Analysis","author":"B. Aminof","year":"2006","unstructured":"Aminof, B., Kupferman, O.: On the succinctness of nondeterminizm. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 125\u2013140. Springer, Heidelberg (2006)"},{"key":"5_CR3","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pp. 1\u201312. Stanford University Press (1962)"},{"issue":"2","key":"5_CR4","first-page":"142","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. I&C\u00a098(2), 142\u2013170 (1992)","journal-title":"I&C"},{"key":"5_CR5","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"5_CR6","first-page":"275","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. FMSD\u00a01, 275\u2013288 (1992)","journal-title":"FMSD"},{"key":"5_CR7","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)"},{"issue":"3","key":"5_CR8","first-page":"175","volume":"61","author":"A.E. Emerson","year":"1984","unstructured":"Emerson, A.E., Sistla, A.P.: Deciding full branching time logics. I&C\u00a061(3), 175\u2013201 (1984)","journal-title":"I&C"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"E.A. Emerson","year":"1983","unstructured":"Emerson, E.A.: Alternative semantics for temporal logics. TCS\u00a026, 121\u2013130 (1983)","journal-title":"TCS"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. 29th FOCS, pp. 328\u2013337 (1988)","DOI":"10.1109\/SFCS.1988.21949"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-540-30476-0_10","volume-title":"Automated Technology for Verification and Analysis","author":"E. Friedgut","year":"2004","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.Y.: B\u00fcchi complementation made tighter. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 64\u201378. Springer, Heidelberg (2004)"},{"key":"5_CR12","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman & Hall, Sydney, Australia (1995)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-58325-4_202","volume-title":"Algorithms and Computation","author":"S.C. Krishnan","year":"1994","unstructured":"Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic \u03c9-automata vis-a-vis deterministic B\u00fcchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol.\u00a0834, pp. 378\u2013386. Springer, Heidelberg (1994)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11901914_11","volume-title":"Automated Technology for Verification and Analysis","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Lampert, R.: On the construction of fine automata for safety properties. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 110\u2013124. Springer, Heidelberg (2006)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/978-3-540-30476-0_27","volume-title":"Automated Technology for Verification and Analysis","author":"O. Kupferman","year":"2004","unstructured":"Kupferman, O., Morgenstern, G., Murano, A.: Typeness for \u03c9-regular automata. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 324\u2013338. Springer, Heidelberg (2004)"},{"issue":"3","key":"5_CR16","first-page":"291","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. FMSD\u00a019(3), 291\u2013314 (2001)","journal-title":"FMSD"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/1055686.1055689","volume":"6","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: From linear time to branching time. ACM TOCL\u00a06(2), 273\u2013294 (2005)","journal-title":"ACM TOCL"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th FOCS, pp. 531\u2013540 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"5_CR19","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Distributed systems - methods and tools for specification","author":"L. Lamport","year":"1985","unstructured":"Lamport, L.: Logical foundation. In: Alford, M.W., Hommel, G., Schneider, F.B., Ansart, J.P., Lamport, L., Mullery, G.P., Liskov, B. (eds.) Distributed Systems. LNCS, vol.\u00a0190, Springer, Heidelberg (1985)"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"L.H. Landweber","year":"1969","unstructured":"Landweber, L.H.: Decision problems for \u03c9\u2013automata. Mathematical Systems Theory\u00a03, 376\u2013384 (1969)","journal-title":"Mathematical Systems Theory"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th POPL, pp. 97\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"key":"5_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)"},{"key":"5_CR24","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer, Heidelberg (1995)"},{"key":"5_CR25","first-page":"521","volume":"9","author":"R. McNaughton","year":"1966","unstructured":"McNaughton, R.: Testing and generating infinite sequences by a finite automaton. I&C\u00a09, 521\u2013530 (1966)","journal-title":"I&C"},{"key":"5_CR26","series-title":"LNM 453","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/BFb0064872","volume-title":"Proc. Logic Colloquium","author":"A.R. Meyer","year":"1975","unstructured":"Meyer, A.R.: Weak monadic second order theory of successor is not elementary recursive. In: AUSCRYPT 1990. LNM 453, pp. 132\u2013154. Springer, Heidelberg (1975)"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Fischer, M.J.: Economy of description by automata, grammars, and formal systems. In: Proc. 12th SWAT, pp. 188\u2013191 (1971)","DOI":"10.1109\/SWAT.1971.11"},{"key":"5_CR28","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)"},{"key":"5_CR29","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. TCS\u00a013, 45\u201360 (1981)","journal-title":"TCS"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"5_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS\u00a0141, 1\u201335 (1969)","journal-title":"Transaction of the AMS"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-40922-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Ravi","year":"2000","unstructured":"Ravi, K., Bloem, R., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 143\u2013160. Springer, Heidelberg (2000)"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proc. 29th FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"5_CR34","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing\u00a06, 495\u2013511 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"5_CR35","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. JACM\u00a032, 733\u2013749 (1985)","journal-title":"JACM"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/BFb0015772","volume-title":"Automata, Languages and Programming","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. In: Brauer, W. (ed.) Automata, Languages and Programming. LNCS, vol.\u00a0194, pp. 465\u2013474. Springer, Heidelberg (1985)"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-13345-3_43","volume-title":"Automata, Languages, and Programming","author":"R.S. Street","year":"1984","unstructured":"Street, R.S., Emerson, E.A.: An elementary decision procedure for the \u03bc-calculus. In: Paredaens, J. (ed.) Automata, Languages, and Programming. LNCS, vol.\u00a0172, pp. 465\u2013472. Springer, Heidelberg (1984)"},{"issue":"1","key":"5_CR38","first-page":"101","volume":"118","author":"H.J. Touati","year":"1995","unstructured":"Touati, H.J., Brayton, R.K., Kurshan, R.: Testing language containment for \u03c9-automata using BDD\u2019s. I&C\u00a0118(1), 101\u2013109 (1995)","journal-title":"I&C"},{"key":"5_CR39","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st LICS, pp. 332\u2013344 (1986)"},{"issue":"2","key":"5_CR40","first-page":"182","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. JCSS\u00a032(2), 182\u2013221 (1986)","journal-title":"JCSS"},{"issue":"1","key":"5_CR41","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C\u00a0115(1), 1\u201337 (1994)","journal-title":"I&C"},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-46691-6_9","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Wilke","year":"1999","unstructured":"Wilke, T.: CTL\u2009+\u2009 is exponentially more succinct than CTL. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a01738, pp. 110\u2013121. Springer, Heidelberg (1999)"},{"key":"5_CR43","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th FOCS, pp. 185\u2013194 (1983)","DOI":"10.1109\/SFCS.1983.51"},{"key":"5_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11787006_50","volume-title":"Automata, Languages and Programming","author":"Q. Yan","year":"2006","unstructured":"Yan, Q.: Lower bounds for complementation of \u03c9-automata via the full automata technique. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 589\u2013600. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74915-8_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:45:57Z","timestamp":1619520357000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74915-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540749141","9783540749158"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74915-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}