Kleene algebra

In <a href="/facts/Mathematics/pxTouaz4">mathematics</a> and <a href="/facts/Theoretical_computer_science/jSkGGuvy">theoretical computer science</a>, a Kleene algebra is a <a href="/facts/Semiring/7cSvWXVQ">semiring</a> that generalizes the theory of <a href="/facts/Regular_expression/KFL3veHX">regular expressions</a>: it consists of a <a href="/facts/Set_(mathematics)/BfucfHMq">set</a> supporting union (addition), concatenation (multiplication), and <a href="/facts/Kleene_star/I6SX0f2Y">Kleene star</a> operations subject to certain algebraic laws. The addition is required to be idempotent (
 
 
 
 x
 +
 x
 =
 x
 
 
 {\displaystyle x+x=x}
 
 for all 
 
 
 
 x
 
 
 {\displaystyle x}
 
), and induces a <a href="/facts/Partially_ordered_set/qb4a3FAX">partial order</a> defined by 
 
 
 
 x
 ≤
 y
 
 
 {\displaystyle x\leq y}
 
 if 
 
 
 
 x
 +
 y
 =
 y
 
 
 {\displaystyle x+y=y}
 
. The Kleene star operation, denoted 
 
 
 
 x
 ∗
 
 
 {\displaystyle x*}
 
, must satisfy the laws of the <a href="/facts/Closure_operator/Ysc3N0co">closure operator</a>.
Kleene algebras have their origins in the theory of regular expressions and <a href="/facts/Regular_language/ahxw67T1">regular languages</a> introduced by Kleene in 1951 and studied by others including V.N. Redko and <a href="/facts/John_Horton_Conway/g3PA1zoK">John Horton Conway</a>. The term was introduced by <a href="/facts/Dexter_Kozen/c5Nspr5d">Dexter Kozen</a> in the 1980s, who fully characterized their algebraic properties and, in 1994, gave a finite axiomatization.
Kleene algebras have a number of extensions that have been studied, including Kleene algebras with tests (KAT) introduced by Kozen in 1997. Kleene algebras and Kleene algebras with tests have applications in <a href="/facts/Formal_verification/BYD4GnJR">formal verification</a> of computer programs. They have also been applied to specify and verify <a href="/facts/Computer_network/3w5RM99p">computer networks</a>.

Kleene algebra open-in-new

Kleene algebra