{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T02:29:55Z","timestamp":1775096995386,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631729","type":"print"},{"value":"9783540692010","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63172-0_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:16:08Z","timestamp":1330298168000},"page":"244-259","source":"Crossref","is-referenced-by-count":55,"title":["Kleene algebra with tests: Completeness and decidability"],"prefix":"10.1007","author":[{"given":"Dexter","family":"Kozen","sequence":"first","affiliation":[]},{"given":"Frederick","family":"Smith","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"15_CR1","unstructured":"A. V. Aho, J. E. Hopcroft, and J. D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1975."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"J. Berstel. Transductions and Context-free Languages. Teubner, 1979.","DOI":"10.1007\/978-3-663-09367-1"},{"key":"15_CR3","unstructured":"E. Cohen. Hypotheses in Kleene algebra. ftp:\/\/ftp.bellcore.com\/pub\/ernie\/research\/homepage.html, April 1994."},{"key":"15_CR4","unstructured":"E. Cohen. Lazy caching. ftp:\/\/ftp.bellcore.com\/pub\/ernie\/research\/homepage.html, 1994."},{"key":"15_CR5","unstructured":"E. Cohen. Using Kleene algebra to reason about concurrency control, ftp:\/\/ftp.bellcore.com\/pub\/ernie\/research\/homepage.html, 1994."},{"key":"15_CR6","unstructured":"E. Cohen, D. Kozen, and F. Smith. The complexity of Kleene algebra with tests. Tech. Rep. TR96-1598, Cornell University, July 1996."},{"key":"15_CR7","unstructured":"J. H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, 1971."},{"issue":"2","key":"15_CR8","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer","year":"1979","unstructured":"M. J. Fischer and R. E. Ladner. Prepositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194\u2013211, 1979.","journal-title":"J. Comput. Syst. Sci."},{"key":"15_CR9","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/0304-3975(86)90101-5","volume":"48","author":"A. Gibbons","year":"1986","unstructured":"A. Gibbons and W. Rytter. On the decidability of some problems about rational subsets of free partially commutative monoids. Theor. Comput. Sci., 48:329\u2013337, 1986.","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"15_CR10","first-page":"379","volume":"23","author":"D. Harel","year":"1980","unstructured":"D. Harel. On folk theorems. Comm. Assoc. Comput. Mach., 23(7):379\u2013389, July 1980.","journal-title":"Comm. Assoc. Comput. Mach."},{"issue":"5","key":"15_CR11","doi-asserted-by":"crossref","first-page":"883","DOI":"10.1137\/0219061","volume":"19","author":"K. Iwano","year":"1990","unstructured":"K. Iwano and K. Steiglitz. A semiring on convex polygons and zero-sum cycle problems. SIAM J. Comput., 19(5):883\u2013901, 1990.","journal-title":"SIAM J. Comput."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"S. C. Kleene. Representation of events in nerve nets and finite automata. In Shannon and McCarthy, editors, Automata Studies, pages 3\u201341. Princeton University Press, 1956.","DOI":"10.1515\/9781400882618-002"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"D. Kozen. On induction vs. *-continuity. In Kozen, editor, Proc. Workshop on Logic of Programs, volume 131 of Lect. Notes in Comput. Sci., pages 167\u2013176. Springer, 1981.","DOI":"10.1007\/BFb0025782"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"D. Kozen. On Kleene algebras and closed semirings. In Rovan, editor, Proc. Math. Found. Comput. Sci., volume 452 of Lect. Notes in Comput. Sci., pages 26\u201347. Springer, 1990.","DOI":"10.1007\/BFb0029594"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"D. Kozen. The Design and Analysis of Algorithms. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-4400-4"},{"issue":"2","key":"15_CR16","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","unstructured":"D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput., 110(2):366\u2013390, May 1994.","journal-title":"Infor. and Comput."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"D. Kozen. Kleene algebra with tests and commutativity conditions. In T. Margaria and B. Steffen, editors, Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of Lect. Notes in Comput. Sci., pages 14\u201333. Springer, March 1996.","DOI":"10.1007\/3-540-61042-1_35"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"W. Kuich and A. Salomaa. Semirings, Automata, and Languages. Springer, 1986.","DOI":"10.1007\/978-3-642-69959-7"},{"key":"15_CR19","unstructured":"G. Mirkowska. Algorithmic Logic and its Applications. PhD thesis, University of Warsaw, 1972. In Polish."},{"key":"15_CR20","volume-title":"PhD thesis","author":"K. C. Ng","year":"1984","unstructured":"K. C. Ng. Relation Algebras with Transitive Closure. PhD thesis, University of California, Berkeley, 1984."},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"V. R. Pratt. Models of program logics. In Proc. 20th Symp. Found. Comput. Sci., pages 115\u2013122. IEEE, 1979.","DOI":"10.1109\/SFCS.1979.24"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"V. R. Pratt. Dynamic algebras and the nature of induction. In Proc. 12th Symp. Theory of Comput., pages 22\u201328. ACM, 1980.","DOI":"10.1145\/800141.804649"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"V. R. Pratt. Dynamic algebras as a well-behaved fragment of relation algebras. In D. Pigozzi, editor, Proc. Conf. on Algebra and Computer Science, volume 425 of Lect. Notes in Comput. Sci., pages 77\u2013110. Springer, June 1988.","DOI":"10.1007\/BFb0043079"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time. In Proc. 5th Symp. Theory of Computing, pages 1\u20139. ACM, 1973.","DOI":"10.1145\/800125.804029"},{"issue":"3","key":"15_CR25","doi-asserted-by":"crossref","first-page":"65","DOI":"10.2307\/2268577","volume":"6","author":"A. Tarski","year":"1941","unstructured":"A. Tarski. On the calculus of relations. J. Symb. Logic, 6(3):65\u2013106, 1941.","journal-title":"J. Symb. Logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63172-0_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:04Z","timestamp":1605647824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63172-0_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631729","9783540692010"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-63172-0_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}