Weak Concurrent Kleene Algebra with Application to Algebraic Verification
| Autor: | McIver, Annabelle, Rabehaja, Tahiry, Struth, Georg |
|---|---|
| Rok vydání: | 2013 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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 $\eta$-simulation equivalence. Applicability is demonstrated by algebraic treatments of two examples: algebraic may testing and Rabin's solution to the choice coordination problem. Comment: 17 pages |
| Databáze: | arXiv |
| Externí odkaz: |
|