{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:46:43Z","timestamp":1725486403690},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540429579"},{"type":"electronic","value":"9783540456537"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45653-8_2","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T00:57:30Z","timestamp":1181350650000},"page":"24-38","source":"Crossref","is-referenced-by-count":17,"title":["On Bounded Specifications"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"MosheY.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,11,20]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F.B. Schneider. Defining liveness. IPL, 21:181\u2013185, 1985.","journal-title":"IPL"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"B. Alpern and F.B. Schneider. Recognizing safety and liveness. Distributed computing, 2:117\u2013126, 1987.","journal-title":"Distributed computing"},{"key":"2_CR3","unstructured":"J. Benthem and J. Bergstra. Logic of transition systems. Technical Report P9308, Programing research group, University of Amsterdam, 1993."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. 36th DAC, pp. 317\u2013320, 1999.","DOI":"10.1145\/309847.309942"},{"key":"2_CR5","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS, LNCS 1579, 1999."},{"key":"2_CR6","series-title":"Lect Notes Comput Sci","first-page":"172","volume-title":"Proc. 11th CAV","author":"A. Biere","year":"1999","unstructured":"A. Biere, E.M. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC[tm] microprocessor using symbolic model checking without BDDs. In Proc. 11th CAV, LNCS 1633, pp. 172\u2013183, 1999."},{"key":"2_CR7","unstructured":"J. Benthem. Languages in actions: categories, lambdas and dynamic logic. Studies in Logic, 130, 1991."},{"key":"2_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-54233-7_126","volume-title":"Proc. 18th ICALP","author":"A. Bouajjani","year":"1991","unstructured":"A. Bouajjani, J.-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching semantics. In Proc. 18th ICALP, LNCS, pp. 76\u201392, 1991."},{"key":"2_CR9","series-title":"Lect Notes Comput Sci","first-page":"37","volume-title":"FMCAD","author":"R. Bloem","year":"2000","unstructured":"R. Bloem, H.N. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in n log n symbolic steps. In FMCAD, LNCS 1954, pp. 37\u201354, 2000."},{"issue":"3","key":"2_CR10","doi-asserted-by":"publisher","first-page":"521","DOI":"10.2307\/2273529","volume":"43","author":"J. Barwise","year":"1978","unstructured":"J. Barwise and Y.N. Moschovakis. Global inductive definability. Journal of Symbolic Logic, 43(3):521\u2013534, 1978.","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"2_CR11","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(97)00217-X","volume":"195","author":"J.C. Bradfield","year":"1998","unstructured":"J.C. Bradfield. The modal \u03bc-calculus alternation hierarchy is strict. Theoretical Computer Science, 195(2):133\u2013153, March 1998.","journal-title":"Theoretical Computer Science"},{"key":"2_CR12","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. JACM, 33(1):151\u2013178, 1986.","journal-title":"JACM"},{"key":"2_CR14","unstructured":"E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional \u03bc-calculus. In Proc. 1st LICS, pp. 267\u2013278, 1986."},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"E.A. Emerson","year":"1983","unstructured":"E.A. Emerson. Alternative semantics for temporal logics. Theoretical Computer Science, 26:121\u2013130, 1983.","journal-title":"Theoretical Computer Science"},{"key":"2_CR16","volume-title":"Computers and Intractability: A Guide to the Theory of NP-completeness","author":"M. Garey","year":"1979","unstructured":"M. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-completeness. W. Freeman and Co., San Francisco, 1979."},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0020-0190(93)90074-J","volume":"47","author":"H.P. Gumm","year":"1993","unstructured":"H.P. Gumm. Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions. IPL, 47:291\u2013294, 1993.","journal-title":"IPL"},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-63166-6_27","volume-title":"Proc. 9th CAV","author":"R.H. Hardin","year":"1997","unstructured":"R.H. Hardin, R.P. Kurshan, S.K. Shukla, and M.Y. Vardi. A new heuristic for bad cycle detection using BDDs. In Proc. 9th CAV, LNCS 1254, pp. 268\u2013278, 1997."},{"key":"2_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/BFb0027043","volume-title":"Proc. Advanced School on Current Trends in Concurrency","author":"H.J. Hoogeboom","year":"1986","unstructured":"H.J. Hoogeboom and G. Rozenberg. Infinitary languages: basic theory and applications to concurrent systems. In Proc. Advanced School on Current Trends in Concurrency, LNCS 224, pp. 266\u2013342, 1986."},{"key":"2_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1007\/3-540-60246-1_160","volume-title":"Proc. 20th MFCS","author":"D. Janin","year":"1995","unstructured":"D. Janin and I. Walukiewicz. Automata for the modal \u03bc-calculus and related results. In Proc. 20th MFCS, LNCS, pp. 552\u2013562, 1995."},{"key":"2_CR21","first-page":"268","volume":"53","author":"E. Kindler","year":"1994","unstructured":"E. Kindler. Safety and liveness properties: A survey. EATCS, 53:268\u2013272, 1994.","journal-title":"EATCS"},{"key":"2_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. TCS, 27:333\u2013354, 1983.","journal-title":"TCS"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"2_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Proc. 11th CAV","author":"O. Kupferman","year":"1999","unstructured":"O. Kupferman and M.Y. Vardi. Model checking of safety properties. In Proc. 11th CAV, LNCS 1633, pp. 172\u2013183, 1999."},{"issue":"2","key":"2_CR25","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. JACM, 47(2):312\u2013360, March 2000.","journal-title":"JACM"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"L. Lamport. Sometimes is sometimes \u201cnot never\u201d-on the temporal logic of programs. In Proc. 7th POPL, pp. 174\u2013185, 1980.","DOI":"10.1145\/567446.567463"},{"key":"2_CR27","series-title":"Lect Notes Comput Sci","first-page":"190","volume-title":"Distributed systems-methods and tools for specification","author":"L. Lamport","year":"1985","unstructured":"L. Lamport. Logical foundation. In Distributed systems-methods and tools for specification, LNCS 190, 1985."},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"L.H. Landweber","year":"1969","unstructured":"L.H. Landweber. Decision problems for\u03c9-automata. Mathematical Systems Theory, 3:376\u2013384, 1969.","journal-title":"Mathematical Systems Theory"},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"S. Miyano and T. Hayashi. Alternating finite automata on \u03c9-words. Theoretical Computer Science, 32:321\u2013330, 1984.","journal-title":"Theoretical Computer Science"},{"key":"2_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/BFb0013024","volume-title":"Linear time, branching time, and partial order in logics and models for concurrency","author":"Z. Manna","year":"1989","unstructured":"Z. Manna and A. Pnueli. The anchored version of the temporal framework. In Linear time, branching time, and partial order in logics and models for concurrency, LNCS 345, pp. 201\u2013284, 1989."},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification., Berlin, January 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"P. Manolios and R. Trefler. Safety and liveness in branching time. In Proc. 16th LICS, 2001.","DOI":"10.1109\/LICS.2001.932512"},{"key":"2_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/3-540-16761-7_96","volume-title":"Proc. 13th ICALP","author":"D. Niwi\u0144ski","year":"1986","unstructured":"D. Niwi\u0144ski. On fixed point clones. In Proc. 13th ICALP, LNCS 226, pp. 464\u2013473, 1986."},{"key":"2_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/3-540-49116-3_50","volume-title":"Proc. 16th STACS","author":"M. Otto","year":"1999","unstructured":"M. Otto. Eliminating recursion in the \u03bc-calculus. In Proc. 16th STACS, LNCS 1563, pp. 531\u2013540, 1999."},{"key":"2_CR35","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1147\/rd.32.0114","volume":"3","author":"M.O. Rabin","year":"1959","unstructured":"M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115\u2013125, 1959.","journal-title":"IBM Journal of Research and Development"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.J.H. Seger","year":"1995","unstructured":"C.J.H. Seger and R.E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6:147\u2013189, 1995.","journal-title":"Formal Methods in System Design"},{"key":"2_CR37","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"A.P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6:495\u2013511, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"L. Staiger. \u03c9-languages. Handbook of Formal Languages, pp. 339\u2013388, 1997.","DOI":"10.1007\/978-3-642-59126-6_6"},{"key":"2_CR39","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":"2_CR40","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M.Y. Vardi","year":"1996","unstructured":"M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pp. 238\u2013266, 1996."},{"issue":"2","key":"2_CR41","doi-asserted-by":"publisher","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"},{"issue":"1","key":"2_CR42","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, November 1994.","journal-title":"Information and Computation"},{"key":"2_CR43","first-page":"110","volume":"1738","author":"T. Wilke","year":"1999","unstructured":"T. Wilke. CTL+ is exponentially more succinct than CTL. In Proc. 19th FST&TCS, 1738, pp. 110\u2013121, 1999.","journal-title":"Proc. 19th FST&TCS"},{"key":"2_CR44","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/3-540-49116-3_3","volume-title":"Proc. 16th STACS","author":"T. Wilke","year":"1999","unstructured":"T. Wilke. Classifying discrete temporal properties In Proc. 16th STACS, LNCS 1563, pp. 32\u201346, 1999."},{"key":"2_CR45","unstructured":"J. Yang. A theory for generalized symbolic trajectory evaluation. In Symposium on Symbolic Trajectory Evaluation, Chicago, July 2000."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45653-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:21:43Z","timestamp":1556479303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45653-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429579","9783540456537"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/3-540-45653-8_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}