Concurrent Kleene algebra with tests and branching automata

摘要

We introduce concurrent Kleene algebra with tests (CKAT) as a combination of Kleene algebra with tests (KAT) of Kozen and Smith with concurrent Kleene algebras (CKA), introduced by Hoare, Moller, Struth and Wehrman. CKAT provides a relatively simple algebraic model for reasoning about semantics of concurrent programs. We generalize guarded strings to guarded series-parallel strings, or gsp-strings, to give a concrete language model for CKAT. Combining nondeterministic guarded automata of Kozen with branching automata of Lodaya and Weil one obtains a model for processing gsp-strings in parallel. To ensure that the model satisfies the weak exchange law (x parallel to y)(z parallel to w) <= (xz)parallel to(yw) of CKA, we make use of the subsumption order of Gischer on the gsp-strings. We also define deterministic branching automata and investigate their relation to (nondeterministic) branching automata.