{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:01Z","timestamp":1763467981713,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230243"},{"type":"electronic","value":"9783540301240"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30124-0_15","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T12:27:59Z","timestamp":1267532879000},"page":"160-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":52,"title":["The Boundary Between Decidability and Undecidability for Transitive-Closure Logics"],"prefix":"10.1007","author":[{"given":"Neil","family":"Immerman","sequence":"first","affiliation":[]},{"given":"Alex","family":"Rabinovich","sequence":"additional","affiliation":[]},{"given":"Tom","family":"Reps","sequence":"additional","affiliation":[]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[]},{"given":"Greta","family":"Yorsh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,9,9]]},"reference":[{"key":"15_CR1","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1996","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1996)"},{"key":"15_CR2","first-page":"139","volume-title":"Principles of Database Systems","author":"G. Dong","year":"1995","unstructured":"Dong, G., Su, J.: Space-bounded foies. In: Principles of Database Systems, pp. 139\u2013150. ACM Press, New York (1995)"},{"key":"15_CR3","first-page":"328","volume-title":"Proc. 29th IEEE Symposium on Foundations of Computer Science","author":"E.A. Emerson","year":"1988","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. In: Proc. 29th IEEE Symposium on Foundations of Computer Science, pp. 328\u2013337. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"53","DOI":"10.2307\/421196","volume":"3","author":"E. Gr\u00e4del","year":"1997","unstructured":"Gr\u00e4del, E.: On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic\u00a03, 53\u201369 (1997)","journal-title":"Bulletin of Symbolic Logic"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s001530050130","volume":"38","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E., Otto, M., Rosen, E.: Undecidability results on two-variable logics. Archive of Math. Logic\u00a038, 313\u2013354 (1999)","journal-title":"Archive of Math. Logic"},{"key":"15_CR6","first-page":"45","volume-title":"Proc. 14th IEEE Symposium on Logic in Computer Science","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E., Walukiewicz, I.: Guarded fixed point logic. In: Proc. 14th IEEE Symposium on Logic in Computer Science, pp. 45\u201354. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019. Springer, Heidelberg (1995)"},{"key":"15_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0539-5","volume-title":"Descriptive Complexity","author":"N. Immerman","year":"1999","unstructured":"Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-27813-9_22","volume-title":"Computer Aided Verification","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Verification via structure simulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 281\u2013294. Springer, Heidelberg (2004)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Meyer, A.R.: Weak monadic second-order theory of successor is not elementary recursive. In: Logic Colloquium. Proc. Symposium on Logic, Boston, pp. 132\u2013154 (1975)","DOI":"10.1007\/BFb0064872"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1002\/malq.19750210118","volume":"21","author":"M. Mortimer","year":"1975","unstructured":"Mortimer, M.: On languages with two variables. Zeitschr. f. math. Logik u. Grundlagen d. Math\u00a021, 135\u2013140 (1975)","journal-title":"Zeitschr. f. math. Logik u. Grundlagen d. Math"},{"key":"15_CR12","volume-title":"Computational Complexity","author":"C. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.: Computational Complexity. Addison Wesley, Reading (1994)"},{"key":"15_CR13","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc.\u00a0141, 1\u201335 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Trans. On Prog. Lang. and Syst., pp. 217\u2013298 (2002)","DOI":"10.1145\/514188.514190"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 530\u2013545. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30124-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T20:03:12Z","timestamp":1579723392000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30124-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230243","9783540301240"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30124-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]},"assertion":[{"value":"9 September 2004","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}