{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:01:04Z","timestamp":1765666864529},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_29","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"424-439","source":"Crossref","is-referenced-by-count":11,"title":["Construction of B\u00fcchi Automata for LTL Model Checking Verified in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Schimpf","sequence":"first","affiliation":[]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[]},{"given":"Jan-Georg","family":"Smaus","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"B\u00fcchi, R.: On a decision method in restricted second-order arithmetic. In: Intl. Cong. Logic, Methodology, and Philosophy of Science 1960, pp. 1\u201312. Stanford University Press (1962)"},{"key":"29_CR2","volume-title":"Model Checking","author":"E.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2002)"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"29_CR4","series-title":"Synthese Library: Studies in Epistemology, Logic, Methodology and Philosophy of Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logic","author":"M.C. Fitting","year":"1983","unstructured":"Fitting, M.C.: Proof Methods for Modal and Intuitionistic Logic. Synthese Library: Studies in Epistemology, Logic, Methodology and Philosophy of Science. D. Reidel, Dordrecht (1983)"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45089-0_5","volume-title":"Implementation and Application of Automata","author":"C. Fritz","year":"2003","unstructured":"Fritz, C.: Constructing B\u00fcchi automata from linear temporal logic using simulation relations for alternating B\u00fcchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 35\u201348. Springer, Heidelberg (2003)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"29_CR7","series-title":"IFIP Conference Proceedings","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"15th Intl. Symp. Protocol Specification, Testing, and Verification (PSTV 1996)","author":"R. Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) 15th Intl. Symp. Protocol Specification, Testing, and Verification (PSTV 1996). IFIP Conference Proceedings, vol.\u00a038, pp. 3\u201318. Chapman & Hall, Boca Raton (1996)"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-39724-3_10","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Gurumurthy","year":"2003","unstructured":"Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic B\u00fcchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 96\u2013110. Springer, Heidelberg (2003)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-31980-1_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.: Complementation constructions for nondeterministic automata on infinite words. In: Halbwachs, N., Zuck, L. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 206\u2013221. Springer, Heidelberg (2005)"},{"issue":"3","key":"29_CR10","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log.\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/3-540-44659-1_26","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Merz","year":"2000","unstructured":"Merz, S.: Weak alternating automata in Isabelle\/HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 424\u2013441. Springer, Heidelberg (2000)"},{"key":"29_CR12","first-page":"422","volume-title":"3rd IEEE Symp. Logic in Computer Science (LICS 1988)","author":"D. Muller","year":"1988","unstructured":"Muller, D., Saoudi, A., Schupp, P.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential tim. In: 3rd IEEE Symp. Logic in Computer Science (LICS 1988), Edinburgh, Scotland, pp. 422\u2013427. IEEE Press, Los Alamitos (1988)"},{"key":"29_CR13","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. Theoretical Computer Science\u00a013, 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"key":"29_CR14","unstructured":"Schimpf, A.: Implementierung eines Verfahrens zur Erzeugung von B\u00fcchi-Automaten aus LTL-Formeln in Isabelle. Diplomarbeit, Albert-Ludwigs-Universit\u00e4t Freiburg (2008), \n                    \n                      http:\/\/www.informatik.uni-freiburg.de\/~ki\/papers\/diplomarbeiten\/schimpf-diplomarbeit-08.pdf"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-48256-3_17","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Schneider","year":"1999","unstructured":"Schneider, K., Hoffmann, D.W.: A HOL conversion for translating linear time temporal logic to \u03c9-automata. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 255\u2013272. Springer, Heidelberg (1999)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","first-page":"257","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"1999","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 257\u2013263. Springer, Heidelberg (1999)"},{"issue":"1","key":"29_CR17","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H. Tauriainen","year":"2002","unstructured":"Tauriainen, H., Heljanko, K.: Testing LTL formula translation into B\u00fcchi automata. International Journal on Software Tools for Technology Transfer\u00a04(1), 57\u201370 (2002), \n                    \n                      http:\/\/www.tcs.hut.fi\/Software\/lbtt\/","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"29_CR18","first-page":"109","volume-title":"Jewels are forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa","author":"W. Thomas","year":"2000","unstructured":"Thomas, W.: Complementation of B\u00fcchi automata revisited. In: Rozenberg, G., Karhum\u00e4ki, J. (eds.) Jewels are forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pp. 109\u2013122. Springer, Heidelberg (2000)"},{"issue":"1","key":"29_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T13:28:59Z","timestamp":1552138139000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}