キャット（KAT）とバオ（BAO）を統合できないか

KozenのKAT（Kleene Algebra with Test）は、ブール半環上のベキ等半加群として再定義できる。一方で、異なる状態空間のあいだの遷移を認める形でKleene圏を定義できる。KATとKleene圏の統合は、ブール半環を対象として、A, Bのhom-set K(A, B)として左A-右Bな両側半加群を採用すればよい。ベキ等半加群（IAM, Idempotent Abelian Monoid）でenrichさていれば、order-enrichもされている。

BAO（Boolean Algebra with Operator）は、状態空間Sの述語のブール代数A（A⊆Pow(S)と考えてよい）と、S上の遷移αによる作用【[α]p】 = α^-1(【p】) を一緒に考えたものだ。遷移αが一価全域なら、αはブール代数の準同型となる。

一般には、遷移が一価全域であることは仮定が強すぎる。S→Pow(S)とするなら、ブール代数のmeet semi-lattice構造しか保存しない。meet保存のオペレータを様相オペレータと呼ぶことにする。

ジャコブスとゴールドブラッドの双対に関する仕事を寄せ集めると、様相オペレータ付きブール代数が遷移系（transition system、クリプキ構造）を定義するようである。

KATもBAOも、状態空間／述語／遷移と強く結びついている。なにか同じものの別な側面のように思える。基礎となるのは、ブール代数と準同型の圏で、これはBoole/Stone空間と連続写像の圏だと思ってもよい（反対圏の実現）。