{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T01:49:39Z","timestamp":1674870579377},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[1997,5]]},"abstract":"\n We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every\n while<\/jats:bold>\n program can be simulated by a while program can be simulated by a\n while<\/jats:bold>\n program with at most one\n while<\/jats:bold>\n loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.\n <\/jats:p>","DOI":"10.1145\/256167.256195","type":"journal-article","created":{"date-parts":[[2002,10,7]],"date-time":"2002-10-07T13:52:47Z","timestamp":1033998767000},"page":"427-443","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":321,"title":["Kleene algebra with tests"],"prefix":"10.1145","volume":"19","author":[{"given":"Dexter","family":"Kozen","sequence":"first","affiliation":[{"name":"Cornell Univ., Ithaca, NY"}]}],"member":"320","published-online":{"date-parts":[[1997,5]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"AHO A. V. HOPCROFT J. E. AND ULLMAN J. D. 1975. The Design and Analysis of Computer Algorithms. Addison-Wesley Reading Mass. AHO A. V. HOPCROFT J. E. AND ULLMAN J. D. 1975. The Design and Analysis of Computer Algorithms. Addison-Wesley Reading Mass."},{"key":"e_1_2_1_2_1","first-page":"1","article-title":"On the algebra of regular expressions","author":"ANDERAA S.","year":"1965","journal-title":"Appl. Math."},{"key":"e_1_2_1_3_1","unstructured":"ARCHANGELSKY I<. V. 1992. A new finite complete solvable quasiequational calculus for algebra of regular languages. Manuscript Kiev State University. ARCHANGELSKY I<. V. 1992. A new finite complete solvable quasiequational calculus for algebra of regular languages. Manuscript Kiev State University."},{"key":"e_1_2_1_4_1","unstructured":"BACKHOUSE R. C. 1975. Closure algorithms and the star-height problem of regular languages. Ph.D. thesis Imperial College London U.K. BACKHOUSE R. C. 1975. Closure algorithms and the star-height problem of regular languages. Ph.D. thesis Imperial College London U.K."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"BERSTEL J. 1979. Transductions and Context-free Languages. Teubner Stuttgart Germany. BERSTEL J. 1979. Transductions and Context-free Languages. Teubner Stuttgart Germany.","DOI":"10.1007\/978-3-663-09367-1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129500000104","article-title":"Equational axioms for regular sets","volume":"3","author":"BLOOM S. L.","year":"1993","journal-title":"Math. Struct. Comput. Sci."},{"issue":"4","key":"e_1_2_1_7_1","first-page":"419","article-title":"Une remarque sur les syst6mes complets d'identit6s rationnelles","volume":"24","author":"BOFFA V{.","year":"1990","journal-title":"Informatique Thdoretique et Applications\/\/Theoretical Informatics and Applications"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/355592.365646"},{"key":"e_1_2_1_9_1","unstructured":"COHEN E. 1994a. Hypotheses in Kleene algebra. Available from ftp:\/\/\/\/ftp b ellcore corn\/\/pub\/\/er nie\/\/research\/\/homepage ht ml COHEN E. 1994a. Hypotheses in Kleene algebra. Available from ftp:\/\/\/\/ftp b ellcore corn\/\/pub\/\/er nie\/\/research\/\/homepage ht ml"},{"key":"e_1_2_1_10_1","unstructured":"COHEN E. 1994b. Lazy caching. Available from ftp:\/\/\/\/ftp b ellcore corn\/\/pub\/\/er nie\/\/research\/\/homepage ht ml COHEN E. 1994b. Lazy caching. Available from ftp:\/\/\/\/ftp b ellcore corn\/\/pub\/\/er nie\/\/research\/\/homepage ht ml"},{"key":"e_1_2_1_11_1","unstructured":"COHEN E. 1994c. Using Kleene algebra to reason about concurrency control. Available from ftp:\/\/ftp b ellcore corn\/pub \/ er nie\/research \/ homepage ht ml COHEN E. 1994c. Using Kleene algebra to reason about concurrency control. Available from ftp:\/\/ftp b ellcore corn\/pub \/ er nie\/research \/ homepage ht ml"},{"key":"e_1_2_1_13_1","unstructured":"CONWAY J. H. 1971. Regular Algebra and Finite Machines. Chapman and Hall London U.K. CONWAY J. H. 1971. Regular Algebra and Finite Machines. Chapman and Hall London U.K."},{"issue":"2","key":"e_1_2_1_14_1","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"FISCHER M. J.","year":"1979","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/0304-3975(86)90101-5","article-title":"On the decidability of some problems about rational subsets of free partially commutative monoids","volume":"48","author":"GIBBONS A.","year":"1986","journal-title":"Theor. Comput. Sci."},{"key":"e_1_2_1_16_1","first-page":"6","article-title":"Rational data structures and their applications","volume":"25","author":"GORSHKOV P. V.","year":"1989","journal-title":"Cybernetics"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/358886.358892"},{"issue":"2","key":"e_1_2_1_18_1","first-page":"55","article-title":"General theory of flowcharts","volume":"21","author":"HIROSE K.","year":"1972","journal-title":"Comment. Math. Univ. St. Pauli"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1137\/0219061"},{"key":"e_1_2_1_20_1","first-page":"3","article-title":"Representation of events in nerve nets and finite automata. In Automata Studies, C. E. Shannon and J. McCarthy, Eds. Princeton University Press, Princeton","author":"KLEENE S. C.","year":"1956","journal-title":"N.J."},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. Workshop on Logic of Programs, Kozen, Ed","author":"KOZEN D. C."},{"key":"e_1_2_1_22_1","first-page":"26","volume-title":"Proc. Math. Found. Comput. Sci., Rovan, Ed. Lecture Notes in Computer Science","volume":"452","author":"KOZEN D. C.","year":"1990"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"KOZEN D. C. 1991. The Design and Analysis of Algorithms. Springer-Verlag New York. KOZEN D. C. 1991. The Design and Analysis of Algorithms. Springer-Verlag New York.","DOI":"10.1007\/978-1-4612-4400-4"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_1_25_1","first-page":"14","volume-title":"Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96)","volume":"1055","author":"KOZEN D. C.","year":"1996"},{"key":"e_1_2_1_26_1","volume-title":"Proc. 12th Syrup. Logic in Comput. Sci. IEEE, Los Alamitos, Ca. To appear. Cornell Tech. Report","author":"KOZEN D. C.","year":"1997"},{"key":"e_1_2_1_27_1","volume-title":"Proc. Conf. Computer Science Logic (CSL'96)","author":"KOZEN D. C.","year":"1996"},{"key":"e_1_2_1_28_1","first-page":"789","article-title":"Logics of programs. In Handbook of Theoretical Computer Science, van Leeuwen, Ed. Vol. B. North Holland","author":"KOZEN D. C.","year":"1990","journal-title":"Amsterdam"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90395-I"},{"key":"e_1_2_1_30_1","first-page":"212","volume-title":"Proc. l~th Colloq. Automata, Languages, and Programming, T. Ottmann, Ed. Lecture Notes in Computer Science","volume":"267","author":"KUICH W.","year":"1987"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"KUICH W. AND SALOMAA A. 1986. Semirings Automata and Languages. Springer-Verlag Berlin. KUICH W. AND SALOMAA A. 1986. Semirings Automata and Languages. Springer-Verlag Berlin.","DOI":"10.1007\/978-3-642-69959-7"},{"key":"e_1_2_1_32_1","unstructured":"MIRKOWSKA G. 1972. Algorithmic logic and its applications. Ph.D. thesis University of Warsaw. in Polish. MIRKOWSKA G. 1972. Algorithmic logic and its applications. Ph.D. thesis University of Warsaw. in Polish."},{"key":"e_1_2_1_33_1","unstructured":"NG K. C. 1984. Relation algebras with transitive closure. Ph.D. thesis University of California Berkeley. NG K. C. 1984. Relation algebras with transitive closure. Ph.D. thesis University of California Berkeley."},{"key":"e_1_2_1_34_1","first-page":"77","volume-title":"Proc. Conf. on Algebra and Computer Science, D. Pigozzi, Ed. Lecture Notes in Computer Science","volume":"425","author":"PRATT V.","year":"1988"},{"key":"e_1_2_1_35_1","volume-title":"Proc. Logics in AI: European Workshop JELIA '90","volume":"478","author":"PRATT V.","year":"1990"},{"key":"e_1_2_1_36_1","first-page":"120","article-title":"On defining relations for the algebra of regular events","volume":"16","author":"REDKO V. N.","year":"1964","journal-title":"Ukrain. Mat. Z."},{"key":"e_1_2_1_37_1","first-page":"39","volume-title":"Eds. Lecture Notes in Computer Science","volume":"281","author":"SAKAROVITCH J.","year":"1987"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/321312.321326"},{"key":"e_1_2_1_39_1","first-page":"1","volume-title":"Proc. 5th Syrup. Theory of Computing. ACM, ACM","author":"STOCKMEYER L. J.","year":"1973"},{"issue":"3","key":"e_1_2_1_40_1","doi-asserted-by":"crossref","first-page":"65","DOI":"10.2307\/2268577","article-title":"On the calculus of relations","volume":"6","author":"TARSKI A.","year":"1941","journal-title":"J. Symb. Logic"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/256167.256195","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T22:05:23Z","timestamp":1672437923000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/256167.256195"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,5]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,5]]}},"alternative-id":["10.1145\/256167.256195"],"URL":"http:\/\/dx.doi.org\/10.1145\/256167.256195","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":["Software"],"published":{"date-parts":[[1997,5]]},"assertion":[{"value":"1997-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}