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}