{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:26:27Z","timestamp":1725456387442},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540645702"},{"type":"electronic","value":"9783540693536"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028005","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:02:06Z","timestamp":1132642926000},"page":"18-34","source":"Crossref","is-referenced-by-count":2,"title":["LISA: A specification language based on WS2S"],"prefix":"10.1007","author":[{"given":"Abdelwaheb","family":"Ayari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"issue":"1\u20132","key":"2_CR1","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0304-3975(94)90209-7","volume":"122","author":"H. Ait-Kaci","year":"1994","unstructured":"H. Ait-Kaci, A. Podelski, and G. Smolka. A feature constraint system for logic programming with entailment. Theoretical Computer Science, 122(1\u20132):263\u2013283, Jan. 1994.","journal-title":"Theoretical Computer Science"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"D. N. Arden. Delayed-logic and finite-state machines. In Proceedings of the Second Annual Symposium and Papers from the First Annual Symposium on Switching Circuit Theory and Logical Design, pages 133\u2013151. American Institute of Electrical Engineers, 1961.","DOI":"10.1109\/FOCS.1961.13"},{"key":"2_CR3","unstructured":"A. Ayari, D. Basin, and A. Podelski. Lisa: A specification language based on ws2s. Available at http:\/\/www.informatik.uni-freiburg.de\/\u2248ayari\/pubs\/, 1998."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"R. Backofen and G. Smolka. A complete and recursive feature theory. In Proceedings of the 31st ACL, pages 193\u2013200, Columbus, Ohio, 1993. ACL. A full version has appeared as Research Report RR-92-30, Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz, Saarbr\u00fccken, Germany.","DOI":"10.3115\/981574.981600"},{"key":"2_CR5","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-60045-0_38","volume":"939","author":"D. A. Basin","year":"1995","unstructured":"D. A. Basin and N. Klarlund. Hardware verification using monadic second-order logic. Lecture Notes in Computer Science, 939:31\u201341, 1995.","journal-title":"Lecture Notes in Computer Science"},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0304-3975(80)90069-9","volume":"10","author":"J. A. Brzozowski","year":"1980","unstructured":"J. A. Brzozowski and E. Leiss. On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science, 10(1):19\u201335, Jan. 1980.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"2_CR7","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A. K. Chandra","year":"1981","unstructured":"A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114\u2013133, Jan. 1981.","journal-title":"Journal of the ACM"},{"key":"2_CR8","volume-title":"Tree Automata","author":"F. G\u00e9cseg","year":"1984","unstructured":"F. G\u00e9cseg and M. Steinby. Tree Automata. Akad\u00e9miai Kiad\u00f3, Budapest, 1984."},{"key":"2_CR9","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume":"1019","author":"J. G. Henriksen","year":"1995","unstructured":"J. G. Henriksen, J. Jensen, M. Joergensen, and N. Klarlund. MONA: Monadic second-order logic in practice. Lecture Notes in Computer Science, 1019:89\u2013101, 1995.","journal-title":"Lecture Notes in Computer Science"},{"key":"2_CR10","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BFb0035388","volume":"1217","author":"P. Kelb","year":"1997","unstructured":"P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. MOSEL: A flexible toolset for monadic second-order logic. Lecture Notes in Computer Science, 1217:183\u2013195, 1997.","journal-title":"Lecture Notes in Computer Science"},{"key":"2_CR11","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/3-540-63166-6_41","volume":"1254","author":"Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, and A. Pnueli. Symbolic model checking with rich assertional languages. Lecture Notes in Computer Science, 1254:424\u2013435, 1997.","journal-title":"Lecture Notes in Computer Science"},{"key":"2_CR12","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BFb0024435","volume":"1169","author":"N. Klarlund","year":"1996","unstructured":"N. Klarlund, M. Nielsen, and K. Sunesen. A case study in verification based on trace abstractions. Lecture Notes in Computer Science, 1169:341\u2013353, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"2_CR13","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1007\/3-540-59293-8_237","volume":"915","author":"Z. Manna","year":"1995","unstructured":"Z. Manna, N. Bjoerner, A. Browne, and E. Chang. STeP: The Stanford Temporal Prover. Lecture Notes in Computer Science, 915:793\u2013794, 1995.","journal-title":"Lecture Notes in Computer Science"},{"key":"2_CR14","unstructured":"F. Morawietz and T. Cornell. On the recognizibility of relations over a tree definable in a monadic second order tree description language. Research Report SFB 340-Report 85, Sonderforschungsbereich 340 of the Deutsche Forschungsgemeinschaft, Februar 1997."},{"issue":"2-3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0304-3975(85)90077-5","volume":"41","author":"G. Slutzki","year":"1985","unstructured":"G. Slutzki. Alternating tree automata. Theoretical Computer Science, 41(2-3):305\u2013318, 1985.","journal-title":"Theoretical Computer Science"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J. W. Thatcher","year":"1968","unstructured":"J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem in second-order logic. Math. Systems Theory, 2:57\u201381, 1968.","journal-title":"Math. Systems Theory"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133\u2013191. Elsevier Science Publishers B. V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"2_CR18","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume":"1043","author":"M. Y. Vardi","year":"1996","unstructured":"M. Y. Vardi. An automata-theoretic approach to linear temporal logic. Lecture Notes in Computer Science, 1043:238\u2013266, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-61511-3_91","volume":"1104","author":"S. Vorobyov","year":"1996","unstructured":"S. Vorobyov. An improved lower bound for the elementary theories of trees. Lecture Notes in Computer Science, 1104:275\u2013287, 1996.","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028005","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:51:18Z","timestamp":1586573478000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028005"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540645702","9783540693536"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0028005","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}