{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:10:27Z","timestamp":1742389827792},"publisher-location":"Berlin, Heidelberg","reference-count":38,"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_3","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T00:57:30Z","timestamp":1181350650000},"page":"39-54","source":"Crossref","is-referenced-by-count":21,"title":["Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy"],"prefix":"10.1007","author":[{"given":"K.","family":"Schneider","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,11,20]]},"reference":[{"key":"3_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-40922-X_4","volume-title":"International Conference on Formal Methods in Computer Aided Design (FMCAD)","author":"R. Bloem","year":"2000","unstructured":"R. Bloem, H. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in n log(n) symbolic steps. In International Conference on Formal Methods in Computer Aided Design (FMCAD), LNCS 1954, pp. 37\u201354. Springer Verlag, 2000."},{"key":"3_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Conference on Computer Aided Verification (CAV)","author":"R. Bloem","year":"1999","unstructured":"R. Bloem, K. Ravi, and F. Somenzi. Efficient decision procedures for model checking of linear time logic properties. In Conference on Computer Aided Verification (CAV), LNCS 1633, Trento, Italy, 1999. Springer-Verlag."},{"issue":"2","key":"3_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. Burch","year":"1992","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computing, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computing"},{"key":"3_CR4","series-title":"3","first-page":"495","volume-title":"Conference on Computer AidedVerification (CAV)","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV:Anewsymbolic model verifier. In Conference on Computer AidedVerification (CAV), 3 1633, pp. 495\u2013499, Trento, Italy, 1999. Springer-Verlag."},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Workshop on Logics of Programs","author":"E. Clarke","year":"1981","unstructured":"E. Clarke and E. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In Workshop on Logics of Programs, LNCS 131, pp. 52\u201371, Yorktown Heights, NewYork, May 1981. Springer-Verlag."},{"key":"3_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Conference on Computer Aided Verification (CAV)","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In Conference on Computer Aided Verification (CAV), LNCS 818, pp. 415\u2013427, lStandford, California, USA, June 1994. Springer-Verlag."},{"issue":"2","key":"3_CR7","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland and B. Steffen. A linear-time model checking algorithm for the alternation-free \u03bc-calculus. Formal Methods in System Design, 2(2):121\u2013147, April 1993.","journal-title":"Formal Methods in System Design"},{"key":"3_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999-Formal Methods","author":"J.-M. Couvreur","year":"1999","unstructured":"J.-M. Couvreur. On-the-fly verification of linear temporal logic. In FM\u201999-Formal Methods, LNCS 1708, pp. 233\u2013252, Toulouse, France, 1999. Springer Verlag."},{"key":"3_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Conference on Computer Aided Verification (CAV)","author":"M. Daniele","year":"1999","unstructured":"M. Daniele, F. Giunchiglia, and M. Vardi. Improved automata generation for linear temporal logic. In Conference on Computer Aided Verification (CAV), LNCS 1633, Trento, Italy, 1999. Springer-Verlag."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"E. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pp. 996\u20131072, Amsterdam, 1990. Elsevier Science Publishers.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"1","key":"3_CR11","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. Emerson","year":"1986","unstructured":"E. Emerson and J. Halpern. \u201csometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151\u2013178, January 1986.","journal-title":"Journal of the ACM"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"E. Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back. In ACM Symposium on Principles of Programming Languages, pp. 84\u201396, NewYork, 1985.","DOI":"10.1145\/318593.318620"},{"key":"3_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"International Conference on Concurrency Theory","author":"K. Etessami","year":"2000","unstructured":"K. Etessami and G. Holzmann. Optimizing B\u00fcchi automata. In International Conference on Concurrency Theory, LNCS 1877, pp. 153\u2013168. Springer Verlag, 2000."},{"key":"3_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Conference on Computer Aided Verification (CAV)","author":"P. Gastin","year":"2001","unstructured":"P. Gastin and D. Oddoux. Fast LTL to B\u00fcchi automata translation. In Conference on Computer Aided Verification (CAV), LNCS 2102, pp. 53\u201365, Paris, France, 2001. Springer Verlag."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing, and Verification (PSTV), Warsaw, June 1995. North-Holland.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"3_CR16","unstructured":"M. Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"3_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-540-48654-1","volume-title":"International Conference on Theorem Provers in Circuit Design (TPCD)","author":"S. Johnson","year":"1994","unstructured":"S. Johnson, P. Miner, and A. Camilleri. Studies of the single pulser in various reasoning systems. In International Conference on Theorem Provers in Circuit Design (TPCD), LNCS 901, pp. 126\u2013145, Bad Herrenalb, Germany, September 1994. Springer-Verlag."},{"key":"3_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055036","volume-title":"Automata, Languages and Programming (ICALP)","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. In Automata, Languages and Programming (ICALP), LNCS 1443, Aalborg, Denmark, 1998. Springer Verlag."},{"key":"3_CR19","first-page":"97","volume-title":"ACM Symposium on Principles of Programming Languages (POPL)","author":"O. Lichtenstein","year":"1985","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In ACM Symposium on Principles of Programming Languages (POPL), pp. 97\u2013107, NewYork, January 1985. ACM."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Ahierarchy of temporal properties. In ACM Symposium on Principles of Distributed Computing, pp. 377\u2013408, 1990.","DOI":"10.1145\/93385.93442"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"3_CR22","unstructured":"K. McMillan. Cadence SMV, http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil , 2000."},{"issue":"1","key":"3_CR23","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":"3_CR24","first-page":"46","volume-title":"Symposium on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"A. Pnueli. The temporal logic of programs. In Symposium on Foundations of Computer Science, volume 18, pp. 46\u201357, NewYork, 1977. IEEE."},{"key":"3_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_10","volume-title":"International Conference on Formal Methods in Computer Aided Design (FMCAD)","author":"K. Ravi","year":"2000","unstructured":"K. Ravi, R. Bloem, and F. Somenzi. A comparative study of symbolic algorithms for the computation of fair cycles. In International Conference on Formal Methods in Computer Aided Design (FMCAD), LNCS 1954. Springer Verlag, 2000."},{"key":"3_CR26","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-0-387-35064-6_4","volume-title":"IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL)","author":"K. Schneider","year":"1997","unstructured":"K. Schneider. CTL and equivalent sublanguages of CTL*. In IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL), pp. 40\u201359, Toledo, Spain, April 1997. IFIP, Chapman and Hall."},{"key":"3_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-49519-3_31","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Schneider","year":"1998","unstructured":"K. Schneider. Model checking on product structures. In Formal Methods in Computer-Aided Design, LNCS 1522, pp. 483\u2013500, Palo Alto, USA, November 1998. Springer Verlag."},{"key":"3_CR28","unstructured":"K. Schneider. Exploiting Hierarchies in Temporal Logics, Finite Automata, Arithmetics, and \u03bc-Calculus for Efficiently Verifying Reactive Systems. Habilitation Thesis. University of Karlsruhe, 2001."},{"key":"3_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-48256-3_17","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"K. Schneider","year":"1999","unstructured":"K. Schneider and D. Hoffmann. A HOL conversion for translating linear time temporal logic to \u03c9-automata. In Higher Order Logic Theorem Proving and its Applications, LNCS 1690, pp. 255\u2013272, Nice, France, September 1999. Springer Verlag."},{"key":"3_CR30","series-title":"Lect Notes Comput Sci","first-page":"445","volume-title":"Andrei Ershov Third International Conference Perspectives of Systems Informatics","author":"K. Schneider","year":"1999","unstructured":"K. Schneider and V. Sabelfeld. Introducing mutual exclusion in Esterel. In Andrei Ershov Third International Conference Perspectives of Systems Informatics, LNCS 1755, pp. 445\u2013459, Akademgorodok, Novosibirsk, Russia, July 1999. Springer Verlag."},{"key":"3_CR31","series-title":"Lect Notes Comput Sci","first-page":"247","volume-title":"Conference on Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"F. Somenzi and R. Bloem. Efficient B\u00fcchi automata from LTL formulae. In Conference on Computer Aided Verification, LNCS 1633, pp. 247\u2013263, Trento, Italy, 2000. Springer-Verlag."},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, pp. 133\u2013191, Amsterdam, 1990. Elsevier Science Publishers.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"3_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Vardi","year":"2001","unstructured":"M. Vardi. Branching vs. linear time: Final showdown. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2031, pp. 1\u201322, Genova, Italy, 2001. Springer Verlag."},{"key":"3_CR34","unstructured":"M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In IEEE Symposium on Logic in Computer Science, pp. 332\u2013344. IEEE Computer Society Press, June 1986."},{"key":"3_CR35","volume-title":"Conference on Correct Hardware Design and Verification Methods","author":"W. Visser","year":"1997","unstructured":"W. Visser, H. Barringer, D. Fellows, G. Gough, and A. Williams. Efficient CTL* model hecking for analysis of rainbow designs. In Conference on Correct Hardware Design and Verification Methods, Montreal, Canada, October 1997. IFIP WG 10.5, Chapman and Hall."},{"key":"3_CR36","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/S0019-9958(79)90653-3","volume":"43","author":"K. Wagner","year":"1979","unstructured":"K. Wagner. On \u03c9-regular sets. Information and control, 43:123\u2013177, 1979.","journal-title":"Information and control"},{"key":"3_CR37","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:72\u201399, 1983.","journal-title":"Information and Control"},{"key":"3_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/3-540-44667-2_7","volume-title":"Summer School on Formal Methods in Performance Analysis","author":"P. Wolper","year":"2001","unstructured":"P. Wolper. Constructing automata from temporal logic formulas: A tutorial. In Summer School on Formal Methods in Performance Analysis, LNCS 2090, pp. 261\u2013277. Springer Verlag, 2001."}],"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_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:20:39Z","timestamp":1556479239000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45653-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429579","9783540456537"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-45653-8_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}