Result: A free construction of Kleene algebras with tests

Title:
A free construction of Kleene algebras with tests
Source:
MPC 2004 : mathematics of program construction (Stirling, 12-14 July 2004)Lecture notes in computer science. :129-141
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 9 ref
Original Material:
INIST-CNRS
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Research Center for Verification and Semantics, AIST, 3-11-46 Nakoji, Amagasaki, Hyogo, 661-0974, Japan
ISSN:
0302-9743
Rights:
Copyright 2004 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.15993822
Database:
PASCAL Archive

Further Information

In this paper we define Kleene algebra with tests in a slightly more general way than Kozen's definition. Then we give an explicit construction of the free Kleene algebra with tests generated by a pair of sets. We also show that the category KAT of Kleene algebras with tests and the category KAT⊆ of Kozen's Kleene algebras with tests are related by an adjunction. This fact shows that an infinitely-generated free Kleene algebra with tests in the sense of Kozen can be obtained as the image of our free algebra under the left adjoint from KAT to KAT⊆; moreover, the image is isomorphic to itself. Therefore, our free Kleene algebra with tests is isomorphic to Kozen and Smith's free Kleene algebra with tests if their construction available. Finally, we show that Kozen and Smith's free Kleene algebra with tests can be presented as a coproduct of Kleene algebras. This is induced from our free construction.