Weak Concurrent Kleene Algebra with Application to Algebraic Verification

2013/01/30 by McIver, Annabelle, Rabehaja, Tahiry, Struth, Georg
#68Q70 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL)

paper · doi:10.48550/arxiv.1301.7153

Abstract

We propose a generalisation of concurrent Kleene algebra \citeHoa09 that can take account of probabilistic effects in the presence of concurrency. The algebra is proved sound with respect to a model of automata modulo a variant of rooted η-simulation equivalence. Applicability is demonstrated by algebraic treatments of two examples: algebraic may testing and Rabin's solution to the choice coordination problem.

Related

• An Event Structure Model for Probabilistic Concurrent Kleene Algebra
• Concurrent Kleene Algebra of Partial Strings
• Kleene Algebra
• A Unifying Categorical View of Nondeterministic Iteration and Tests
• Weak Kleene Algebra is Sound and (Possibly) Complete for Simulation