A Complete Axiomatisation for Probabilistic Trace Equivalence
We provide an axiomatisation for =pTr , a variant of probabilistic trace equivalence as formulated by Bernardo et al., 2014, in the setting of the alternating model of Hansson. The equivalence considers traces individually instead of trace distributions. We show that our axiomatisation is sound and...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Alexandru Ioan Cuza University of Iasi
2020-08-01
|
| Series: | Scientific Annals of Computer Science |
| Subjects: | |
| Online Access: | https://www.info.uaic.ro/en/sacs_articles/a-complete-axiomatisation-for-probabilistic-trace-equivalence/ |
| Summary: | We provide an axiomatisation for =pTr , a variant of probabilistic trace equivalence as formulated by Bernardo et al., 2014, in the setting of the alternating model of Hansson. The equivalence considers traces individually instead of trace distributions. We show that our axiomatisation is sound and also complete for recursion-free sequential processes. Due to the nature of the trace equivalence, the axiomatisation is particularly complex. |
|---|---|
| ISSN: | 1843-8121 2248-2695 |