Published in Volume XXII, Issue 2, 2012, pages 367-394, doi: 10.7561/SACS.2012.2.367

Authors: A. Silva


Kleene algebra with tests (KAT) is an equational system that combines Kleene and Boolean algebras. One can model basic programming constructs and assertions in KAT, which allowed for its application in compiler optimization, program transformation and dataflow analysis. To provide semantics for KAT expressions, Kozen first introduced emph{automata on guarded strings}, showing that the regular sets of guarded strings plays the same role in KAT as regular languages play in Kleene algebra. Recently, Kozen described an elegant algorithm, based on “derivatives”, to construct a deterministic automaton that accepts the guarded strings denoted by a KAT expression. This algorithm generalizes Brzozowski’s algorithm for regular expressions and inherits its inefficiency arising from the explicit computation of derivatives.

In the context of classical regular expressions, many efficient algorithms to compile expressions to automata have been proposed. One of those algorithms was devised by Berry and Sethi in the 80’s (we shall refer to it as Berry-Sethi construction/algorithm, but in the literature it is also referred to as position or Glushkov automata algorithm).

In this paper, we show how the Berry-Sethi algorithm can be used to compile a $KAT$ expression to an automaton on guarded strings. Moreover, we propose a new automata model for KAT expressions and adapt the construction of Berry and Sethi to this new model.

Full Text (PDF)


[1] Allegra Angus and Dexter Kozen. Kleene algebra with tests and pro- gram schematology. Technical Report TR2001-1844, Computing and Information Science, Cornell University, July 2001.

[2] Valentin M. Antimirov. Partial derivatives of regular expressions and nite automaton constructions. Theor. Comput. Sci., 155(2):291-319, 1996. .

[3] Falk Bartels. On generalized coinduction and probabilistic speci cation formats. PhD thesis, Vrije Universiteit Amsterdam, 2004. PhD thesis.

[4] Gerard Berry and Ravi Sethi. From regular expressions to deterministic automata. Theor. Comput. Sci., 48(3):117-126, 1986. .

[5] Janusz A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481-494, 1964. .

[6] Jean-Marc Champarnaud, Florent Nicart, and Djelloul Ziadi. From the ZPC structure of a regular expression to its follow automaton. IJAC, 16(1):17-34, 2006. .

[7] Jean-Marc Champarnaud and Djelloul Ziadi. Canonical derivatives, partial derivatives and nite automaton constructions. Theor. Comput. Sci., 289(1):137-163, 2002. .

[8] V.M. Glushkov. The abstract theory of automata. Russian Math. Surveys, 16:1-53, 1961. .

[9] Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and Jose Meseguer, editors, Essays Dedicated to Joseph A. Goguen, volume 4060 of Lecture Notes in Computer Science, pages 375-404. Springer, 2006. .

[10] Donald M. Kaplan. Regular expressions and the equivalence of pro- grams. J. Comput. Syst. Sci., 3(4):361-386, 1969. .

[11] Dexter Kozen. Automata and Computability. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1997.

[12] Dexter Kozen. Automata on guarded strings and applications. Matematica Contempor^anea, 24:117-139, 2003.

[13] Dexter Kozen. Nonlocal ow of control and Kleene algebra with tests. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 105-117. IEEE Computer Society, 2008. .

[14] Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. Technical Report , Computing and Information Science, Cornell University, March 2008.

[15] Dexter Kozen and Maria-Christina Patron. Certi cation of com- piler optimizations using Kleene algebra with tests. In John W. Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Lus Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey, editors, Computational Logic, volume 1861 of Lecture Notes in Computer Science, pages 568-582. Springer, 2000. .

[16] Robert McNaughton and H. Yamada. Regular expressions and state graphs for automata. IRE Transactions on Electronic Computers, 9(1):39-47, 1960. .

[17] Michael O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:114-125, 1959. .

[18] Jan J. M. M. Rutten. Automata and coinduction (an exercise in coalge- bra). In Davide Sangiorgi and Robert de Simone, editors, CONCUR, volume 1466 of Lecture Notes in Computer Science, pages 194-218. Springer, 1998. .

[19] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. .

[20] Alexandra Silva. Kleene coalgebra. PhD thesis, Radboud University Nijmegen, 2010.

[21] Ken Thompson. Programming techniques: Regular expression search algorithm. Commun. ACM, 11(6):419-422, 1968. .


  title={Position Automata for Kleene Algebra with Tests},
  author={A. Silva},
  journal={Scientific Annals of Computer Science},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  publisher={``A.I. Cuza'' University Press}