{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T13:52:19Z","timestamp":1766065939190,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_5","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T19:39:50Z","timestamp":1265917190000},"page":"38-52","source":"Crossref","is-referenced-by-count":10,"title":["Efficient Model Checking Via B\u00fcchi Tableau Automata?"],"prefix":"10.1007","author":[{"given":"Girish S.","family":"Bhat","sequence":"first","affiliation":[]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Groce","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"5_CR1","unstructured":"LICS\u2019 86, Cambridge, Massachusetts, June 1986. IEEE Computer Society Press."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In LICS\u2019 90, pages 414\u2013425, Philadelphia, Jun. 1990. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1990.113766"},{"issue":"1","key":"5_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H.R. Andersen","year":"1994","unstructured":"H.R. Andersen. Model checking and boolean graphs. TCS, 126(1):3\u201330, Apr. 1994.","journal-title":"TCS"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"H.R. Andersen. Partial model checking. In LICS\u2019 95, pages 398\u2013407, San Diego, Jul. 1995. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1995.523274"},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-61042-1_41","volume-title":"TACAS\u2019 96","author":"G. Bhat","year":"1996","unstructured":"G. Bhat and R. Cleaveland. Efficient local model checking for fragments of the modal \u00b5-calculus. In T. Margaria and B. Steffen, eds., TACAS\u2019 96, LNCS 1055:107\u2013126, Passau, Mar. 1996. Springer-Verlag."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"G. Bhat and R. Cleaveland. Efficient model checking via the equational \u00b5-calculus. In LICS\u2019 96, pages 304\u2013312, New Brunswick, Jul. 1996. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1996.561358"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1023\/A:1018982020561","volume":"7","author":"G. Bhat","year":"1999","unstructured":"G. Bhat, R. Cleaveland, and G. Luettgen. A practical approach to implementing real-time semantics. Annals of Software Engineering, 7:127\u2013155, Oct. 1999.","journal-title":"Annals of Software Engineering"},{"issue":"2","key":"5_CR8","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, Jun. 1992.","journal-title":"Information and Computation"},{"issue":"2","key":"5_CR9","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 TOPLAS, 8(2):244\u2013263, Apr. 1986.","journal-title":"ACM TOPLAS"},{"issue":"4","key":"5_CR10","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"E.M. Clarke and J.M. Wing. Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626\u2013643, Dec. 1996.","journal-title":"ACM Computing Surveys"},{"issue":"2","key":"5_CR11","first-page":"50","volume":"17","author":"R. Cleaveland","year":"1996","unstructured":"R. Cleaveland, G. Luettgen, V. Natarajan, and S. Sims. Modeling and verifying distributed systems using priorities: A case study. Software Concepts and Tools, 17(2):50\u201362, 1996.","journal-title":"Software Concepts and Tools"},{"key":"5_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"CAV\u2019 96","author":"R. Cleaveland","year":"1996","unstructured":"R. Cleaveland and S. Sims. The NCSU Concurrency Workbench. In R. Alur and T. Henzinger, eds., CAV\u2019 96, LNCS 1102:394\u2013397, New Brunswick, Jul. 1996. Springer-Verlag."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"R. Cleaveland and S. Sims. Generic tools for verifying concurrent systems. Science of Computer Programming, to appear.","DOI":"10.1016\/S0167-6423(01)00033-8"},{"key":"5_CR14","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 alternationfree modal mu-calculus. Formal Methods in System Design, 2:121\u2013147, 1993.","journal-title":"Formal Methods in System Design"},{"key":"5_CR15","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 verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"5_CR16","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"M. Dam. CTL** and ECTL** as fragments of the modal mu-calculus. TCS, 126(1):77\u201396, Apr. 1994.","journal-title":"TCS"},{"key":"5_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"CAV\u2019 93","author":"E.A. Emerson","year":"1993","unstructured":"E.A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of \u00b5-calculus. In C. Courcoubetis, ed., CAV\u2019 93, LNCS 697:385\u2013396, Elounda, Jul. 1993. Springer-Verlag."},{"key":"5_CR18","unstructured":"E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In [1], pages 267\u2013278."},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000","author":"K. Etessami","year":"2000","unstructured":"K. Etessami and G. Holzmann. Optimizing buechi automata. In C. Palamidessi, ed., CONCUR 2000, LNCS 1877:153\u2013169, State College, Aug. 2000. Springer-Verlag."},{"key":"5_CR20","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 PSTV\u2019 95, pages 3\u201318, Warsaw, Jun. 1995. Chapman and Hall.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"5_CR21","unstructured":"G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991."},{"issue":"3","key":"5_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 \u00b5-calculus. TCS, 27(3):333\u2013354, Dec. 1983.","journal-title":"TCS"},{"issue":"2","key":"5_CR23","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, Mar. 2000.","journal-title":"JACM"},{"issue":"1+2","key":"5_CR24","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. Larsen","year":"1997","unstructured":"K. Larsen, P. Pettersson, and W. Yi. UPPAAL in a nutshell. Software Tools for Technology Transfer, 1(1+2):134\u2013152, Oct. 1997.","journal-title":"Software Tools for Technology Transfer"},{"key":"5_CR25","unstructured":"R. Mateescu and H. Garavel. XTL: A meta-language and tool for temporal logic model-checking. In T. Margaria and B. Steffen, eds., STTT\u201998, Aalborg, Jul. 1998."},{"key":"5_CR26","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, London, 1989."},{"key":"5_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Specification and verification of concurrent systems in CESAR","author":"J.P. Queille","year":"1982","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In M. Dezani-Ciancaglini and U. Montanari, eds., Proc. Int. Symp. in Programming, LNCS 137: 337\u2013351, Turin, Apr. 1982. Springer-Verlag."},{"key":"5_CR28","series-title":"Lect Notes Comput Sci","first-page":"247","volume-title":"CAV 2000","author":"F. Somenzi","year":"2000","unstructured":"F. Somenzi and R. Bloem. Efficient B\u00fcchi automata from LTL formulae. In E.A. Emerson and A.P. Sistla, eds., CAV 2000, LNCS 1855:247\u2013263, Chicago, Jul. 2000. Springer-Verlag."},{"key":"5_CR29","unstructured":"M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In [1], pages 332\u2013344."},{"issue":"4","key":"5_CR30","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/s100090050042","volume":"2","author":"W. Visser","year":"2000","unstructured":"W. Visser and H. Barringer. Practical CTL** model checking-should SPIN be extended? Software Tools for Technology Transfer, 2(4):350\u2013365, Apr. 2000.","journal-title":"Software Tools for Technology Transfer"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"W. Visser, H. Barringer, D. Fellows, G. Gough, and A. Williams. Efficient CTL** model checking for analysis of rainbow designs. In H. Li and D. Probst, eds., CHARME\u201997, pages 128\u2013145, Montr\u00e9al, Oct. 1997. IFIP WG 10.5, Chapman and Hall.","DOI":"10.1007\/978-0-387-35190-2_9"},{"issue":"2","key":"5_CR32","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1145\/244795.244803","volume":"19","author":"J. Yang","year":"1997","unstructured":"J. Yang, A. Mok, and Farn Wang. Symbolic model checking for event-driven real-time systems. ACM TOPLAS 19(2):386\u2013412, Mar. 1997","journal-title":"ACM TOPLAS"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T10:29:01Z","timestamp":1739874541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}