{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T09:10:40Z","timestamp":1774775440773,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540001416","type":"print"},{"value":"9783540361350","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36135-9_20","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:43:21Z","timestamp":1180665801000},"page":"308-326","source":"Crossref","is-referenced-by-count":79,"title":["From States to Transitions: Improving Translation of LTL Formulae to B\u00fcchi Automata"],"prefix":"10.1007","author":[{"given":"Dimitra","family":"Giannakopoulou","sequence":"first","affiliation":[]},{"given":"Flavio","family":"Lerda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., and Park, S. \u201cModel Checking Programs\u201d, in Proc. of the 15th IEEE International Conference on Automated Software Engineering (ASE\u20192000. 11\u201315 September 2000, Grenoble, France. IEEE Computer Society, pp. 3\u201311. Y. Ledru, P. Alexander, and P. Flener, Eds.","DOI":"10.1109\/ASE.2000.873645"},{"issue":"5","key":"20_CR2","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J., The Model Checker SPIN. IEEE Transactions on Software Engineering, Vol. 23(5), May 1997: pp. 279\u2013295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., and Yannakakis, M., Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design, Vol. 1, 1992: pp. 275\u2013288.","journal-title":"Formal Methods in System Design"},{"key":"20_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Optimizing Buechi automata","author":"K. Etessami","year":"2000","unstructured":"Etessami, K. and Holzmann, G. \u201cOptimizing Buechi automata\u201d, in Proc. of the 11th International Conference on Concurrency Theory (CONCUR\u20192000). August 2000, Pennsylvania, USA. Springer, LNCS 1877."},{"key":"20_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Efficient Buechi automata from LTL Formulae","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F. and Bloem, R. \u201cEfficient Buechi automata from LTL Formulae\u201d, in Proc. of the 12th International Conference on Computer Aided Verification (CAV 2000). July 2000, Chicago, USA. Springer, LNCS 1855. E.A. Emerson and A.P. Sistla, Eds."},{"key":"20_CR6","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., and Wolper, P. \u201cSimple On-the-fly Automatic Verification of Linear Temporal Logic\u201d, in Proc. of the 15th IFIP\/WG6.1 Symposium on Protocol Specification, Testing and Verification (PSTV\u201995). June 1995, Warsaw, Poland."},{"key":"20_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Improved Automata Generation for Linear Temporal Logic","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., and Vardi, M.Y. \u201cImproved Automata Generation for Linear Temporal Logic\u201d, in Proc. of the 11th International Conference on Computer Aided Verification (CAV 1999). July 1999, Trento, Italy. Springer, LNCS 1633."},{"key":"20_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Fast LTL to Buechi Automata Translation","author":"P. Gastin","year":"2001","unstructured":"Gastin, P. and Oddoux, D. \u201cFast LTL to Buechi Automata Translation\u201d, in Proc. of the 13th International Conference on Computer Aided Verification (CAV 2001). July 2001, Paris, France. Springer, LNCS 2102, pp. 53\u201365. G. Berry, H. Comon, and A. Finkel, Eds."},{"key":"20_CR9","unstructured":"Clarke, E.M., Grumberg, O., and Peled, D.A., Model Checking: The MIT press, 1999."},{"key":"20_CR10","unstructured":"Giannakopoulou, D. and Lerda, F., \u201cEfficient translation of LTL formulae into B\u00fcchi automata\u201d, RIACS, Technical Report, 01.29, June 2001."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Wolper, P. \u201cConstructing Automata from Temporal Logic Formulas: A Tutorial\u201d, in Proc. of the FMPA 2000 summer school. July 2000, Nijmegen, the Netherlands.","DOI":"10.1007\/3-540-44667-2_7"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36135-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:17:37Z","timestamp":1556464657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36135-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001416","9783540361350"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-36135-9_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}