Weak Concurrent Kleene Algebra with Application to Algebraic Verification
Formal Languages and Automata Theory
2013-01-31 v1
Abstract
We propose a generalisation of concurrent Kleene algebra \cite{Hoa09} 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.
Keywords
Cite
@article{arxiv.1301.7153,
title = {Weak Concurrent Kleene Algebra with Application to Algebraic Verification},
author = {Annabelle McIver and Tahiry Rabehaja and Georg Struth},
journal= {arXiv preprint arXiv:1301.7153},
year = {2013}
}
Comments
17 pages