Kleene algebra with tests

ABSTRACT

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 while program can be simulated by a while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.

REFERENCES

• 1: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 2: ANDERAA, S. 1965. On the algebra of regular expressions. Appl. Math., 1-18.
• 3: ARCHANGELSKY, I<. V. 1992. A new finite complete solvable quasiequational calculus for algebra of regular languages. Manuscript, Kiev State University.
• 4: BACKHOUSE, R. C. 1975. Closure algorithms and the star-height problem of regular languages. Ph.D. thesis, Imperial College, London, U.K.
• 5: BERSTEL, J. 1979. Transductions and Context-free Languages. Teubner, Stuttgart, Germany.
• 6: BLOOM, S. L. AND t~SIK, Z. 1993. Equational axioms for regular sets. Math. Struct. Comput. Sci. 3, 1-24.
• 7: BOFFA, iV{. 1990. Une remarque sur les syst6mes complets d'identit6s rationnelles. Informatique Thdoretique et Applications//Theoretical Informatics and Applications 24, 4, 419-423.
• 8: Corrado Böhm , Giuseppe Jacopini, Flow diagrams, turing machines and languages with only two formation rules, Communications of the ACM, v.9 n.5, p.366-371, May 1966 [doi>10.1145/355592.365646]
• 9: COHEN, E. 1994a. Hypotheses in Kleene algebra. Available from ftp:////ftp, b ellcore, corn//pub//er nie//research//homepage, ht ml
• 10: COHEN, E. 1994b. Lazy caching. Available from ftp:////ftp, b ellcore, corn//pub//er nie//research//homepage, ht ml
• 11: 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
• 12: Ernie Cohen , Dexter Kozen , Frederick Smith, The Complexity of Kleene Algebra with Tests, Cornell University, Ithaca, NY, 1996
• 13: CONWAY, J. H. 1971. Regular Algebra and Finite Machines. Chapman and Hall, London, U.K.
• 14: FISCHER, M. J. AND LADNER, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 2, 194-211.
• 15: A. Gibbons , W. Rytter, On the decidability of some problems about rational subsets of free partially commutative monoids, Theoretical Computer Science, v.48 n.2-3, p.329-337, Dec., 1986
• 16: GORSHKOV, P. V. 1989. Rational data structures and their applications. Cybernetics 25, 6 (Nov.- Dec.), 760-765.
• 17: David Harel, On folk theorems, Communications of the ACM, v.23 n.7, p.379-389, July 1980 [doi>10.1145/358886.358892]
• 18: HIROSE, K. AND OYA, M. 1972. General theory of flowcharts. Comment. Math. Univ. St. Pauli 21, 2, 55-71.
• 19: Kazuo Iwano , Kenneth Steiglitz, A semiring on convex polygons and zero-sum cycle problems, SIAM Journal on Computing, v.19 n.5, p.883-901, Oct. 1990 [doi>10.1137/0219061]
• 20: KLEENE, S. C. 1956. Representation of events in nerve nets and finite automata. In Automata Studies, C. E. Shannon and J. McCarthy, Eds. Princeton University Press, Princeton, N.J., 3-41.
• 21: Dexter Kozen, On Induction vs. *-Continuity, Logic of Programs, Workshop, p.167-176, May 01, 1981
• 22: Dexter Kozen, On Kleene algebras and closed semirings, Proceedings on Mathematical foundations of computer science 1990, p.26-47, September 1990, Banska´ Bystrica, Czechoslovakia
• 23: Dexter C. Kozen, The design and analysis of algorithms, Springer-Verlag New York, Inc., New York, NY, 1992
• 24: Dexter Kozen, A completeness theorem for Kleene algebras and the algebra of regular events, Information and Computation, v.110 n.2, p.366-390, May 1, 1994
• 25: Dexter Kozen, Kleene Algebra withTests and Commutativity Conditions, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.14-33, March 27-29, 1996
• 26: Dexter Kozen, On the Complexity of Reasoning in Kleene Algebra, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.195, June 29-July 02, 1997
• 27: Dexter Kozen , Frederick Smith, Kleene Algebra with Tests: Completeness and Decidability, Selected Papers from the10th International Workshop on Computer Science Logic, p.244-259, September 21-27, 1996
• 28: Dexter Zozen , Jerzy Tiuryn, Logics of programs, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 29: Daniel Krob, Complete systems of B -rational identities, Theoretical Computer Science, v.89 n.2, p.207-343, Oct. 28, 1991 [doi>10.1016/0304-3975(91)90395-I]
• 30: W. Kuich, The Kleene and the Parikh theorem in complete semirings, 14th International Colloquium on Automata, languages and programming, p.212-225, July 1987, Karlsruhe, Germany
• 31: Werner Kuich , Arto Salomaa, Semirings, Automata and Languages, Springer-Verlag New York, Inc., Secaucus, NJ, 1985
• 32: MIRKOWSKA, G. 1972. Algorithmic logic and its applications. Ph.D. thesis, University of Warsaw. in Polish.
• 33: NG, K. C. 1984. Relation algebras with transitive closure. Ph.D. thesis, University of California, Berkeley.
• 34: Vaughan Pratt, Dynamic algebras as a well-behaved fragment of relation algebras, Proceedings of the international conference on cryptology on Algebraic logic and universal algebra in computer science, September 1990, Sydney, Australia
• 35: Vaughan Pratt, Action logic and pure induction, Proceedings of the European workshop on Logics in AI, p.97-120, March 1991, Amsterdam, The Netherlands
• 36: REDKO, V. N. 1964. On defining relations for the algebra of regular events. Ukrain. Mat. Z. 16, 120-126. In Russian.
• 37: Jacques Sakarovitch, Kleene's theorem revisited, Selected contributions on Trends, techniques, and problems in theoretical computer science. 4th International Meeting of Young Computer Scientists, p.39-50, January 1987, Smolenice, Czechoslovakia
• 38: Arto Salomaa, Two Complete Axiom Systems for the Algebra of Regular Events, Journal of the ACM (JACM), v.13 n.1, p.158-169, Jan. 1966 [doi>10.1145/321312.321326]
• 39: L. J. Stockmeyer , A. R. Meyer, Word problems requiring exponential time(Preliminary Report), Proceedings of the fifth annual ACM symposium on Theory of computing, p.1-9, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804029]
• 40: TARSKI, A. 1941. On the calculus of relations. J. Symb. Logic 6, 3, 65-106.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Structured programming**

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions; Assertions; Logics of programs; Specification techniques; Mechanical verification; Invariants
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation
          Subjects: Simplification of expressions
      I.1.3 Languages and Systems
          Subjects: Special-purpose algebraic systems
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification; Program transformation; Program modification; Program synthesis

General Terms:
Design, Languages, Theory, Verification

Keywords:
Kleene algebra, dynamic logic, specification