{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:48:01Z","timestamp":1725551281535},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_25","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:13:28Z","timestamp":1269882808000},"page":"321-326","source":"Crossref","is-referenced-by-count":4,"title":["Yet Another Look at LTL Model Checking"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Schneider","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"25_CR1","series-title":"Lect Notes Comput Sci","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, Nice, France, September 1999. Springer Verlag."},{"key":"25_CR2","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. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In Conference on Computer Aided Verification (CAV), LNCS 818, pp. 415\u2013427, Standford, California, USA, June 1994. Springer-Verlag."},{"key":"25_CR3","series-title":"Lect Notes Comput Sci","first-page":"477","volume-title":"Computer Aided Verification (CAV)","author":"G.G. Jong de","year":"1991","unstructured":"G.G de Jong. An automata theoretic approach to temporal logic. In Computer Aided Verification (CAV), LNCS 575, pp. 477\u2013487, Aalborg, July 1991. Springer-Verlag."},{"key":"25_CR4","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133\u2013191, Amsterdam, 1990. Elsevier Science Publishers."},{"key":"25_CR5","series-title":"IFIP","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\u273b. In C. Delgado Kloos, editor, IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL), pp. 40\u201359, Toledo, Spain, April 1997. IFIP, Chapman and Hall."},{"key":"25_CR6","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, CA, November 1998. Springer Verlag."},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Y. Vardi. Freedom, weakness, and determinism: From lineartime to branching-time. In IEEE Symposium on Logic in Computer Science, 1998.","DOI":"10.1109\/LICS.1998.705645"},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0019-9958(79)90653-3","volume":"43","author":"K. Wagner","year":"1979","unstructured":"K. Wagner. On \u273b regular sets. Information and control, 43:123\u2013177, 1979.","journal-title":"Information and control"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T09:48:14Z","timestamp":1551088094000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}