{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T12:10:26Z","timestamp":1737288626053,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404934"},{"type":"electronic","value":"9783540450610"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45061-0_56","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:54:04Z","timestamp":1184601244000},"page":"714-724","source":"Crossref","is-referenced-by-count":5,"title":["Upper Bounds for a Theory of Queues"],"prefix":"10.1007","author":[{"given":"Tatiana","family":"Rybina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"key":"56_CR1","doi-asserted-by":"crossref","unstructured":"M. Benedikt, L. Libkin, T. Schwentick, and L. Segoufin. A model-theoretic approach to regular string relations. In Proc. 16th Annual IEEE Symposium on Logic in Computer Science, LICS 2001, pages 431\u2013440, 2001.","DOI":"10.1109\/LICS.2001.932518"},{"key":"56_CR2","unstructured":"N.S. Bj\u00f8rner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Computer Science Department, Stanford University, 1998."},{"key":"56_CR3","unstructured":"N.S. Bj\u00f8rner. Reactive verification with queues. In ARO\/ONR\/NSF\/DARPA Workshop on Engineering Automation for Computer-Based Systems, pages 1\u20138, Carmel, CA, 1998."},{"key":"56_CR4","doi-asserted-by":"crossref","unstructured":"A. Blumensath and E. Gr\u00e4del. Automatic structures. In Proc. 15th Annual IEEE Symp. on Logic in Computer Science, pages 51\u201362, Santa Barbara, California, June 2000.","DOI":"10.1109\/LICS.2000.855755"},{"key":"56_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(90)90080-L","volume":"48","author":"K.J. Compton","year":"1990","unstructured":"K.J. Compton and C.W. Henson. A uniform method for proving lower bounds on the computational complexity of logical theories. Annals of Pure and Applied Logic, 48:1\u201379, 1990.","journal-title":"Annals of Pure and Applied Logic"},{"key":"56_CR6","doi-asserted-by":"crossref","unstructured":"J. Ferrante and C.W. Rackoff. The computational complexity of logical theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, 1979.","DOI":"10.1007\/BFb0062837"},{"key":"56_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/3-540-60178-3_93","volume-title":"Logic and Computational Complexity, International Workshop LCC\u2019 94","author":"B. Khoussainov","year":"1995","unstructured":"B. Khoussainov and A. Nerode. Automatic presentations of structures. In Daniel Leivant, editor, Logic and Computational Complexity, International Workshop LCC\u2019 94, volume 960 of Lecture Notes in Computer Science, pages 367\u2013392. Springer Verlag, 1995."},{"issue":"2","key":"56_CR8","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1145\/371316.371494","volume":"2","author":"T. Rybina","year":"2001","unstructured":"T. Rybina and A. Voronkov. A decision procedure for term algebras with queues. ACM Transactions on Computational Logic, 2(2):155\u2013181, 2001.","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1","key":"56_CR9","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(92)90090-3","volume":"103","author":"W. Thomas","year":"1992","unstructured":"W. Thomas. Infinite trees and automaton definable relations over omega-words. Theoretical Computer Science, 103(1):143\u2013159, 1992.","journal-title":"Theoretical Computer Science"},{"key":"56_CR10","first-page":"509","volume":"45","author":"H. Volger","year":"1983","unstructured":"H. Volger. A new hierarchy of elementary recursive decision problems. Methods of Operations Research, 45:509\u2013519, 1983.","journal-title":"Methods of Operations Research"},{"key":"56_CR11","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(83)90038-5","volume":"23","author":"H. Volger","year":"1983","unstructured":"H. Volger. Turing machines with linear alternation, theories of bounded concatenation and the decision problem of first order theories (Note). Theoretical Computer Science, 23:333\u2013337, 1983.","journal-title":"Theoretical Computer Science"},{"key":"56_CR12","doi-asserted-by":"crossref","unstructured":"S. Vorobyov and A. Voronkov. Complexity of nonrecursive logic programs with complex values. In PODS\u201998, pages 244\u2013253, Seattle, Washington, 1998. ACM Press.","DOI":"10.1145\/275487.275515"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45061-0_56","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T11:43:45Z","timestamp":1737287025000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45061-0_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404934","9783540450610"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45061-0_56","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}