Axiomatising Infinitary Probabilistic Weak Bisimilarity of Finite-State Behaviours

Select | Print


Fischer, Nick; van Glabbeek, Rob


2019-01-02


Journal Article


Journal of Logical and Algebraic Methods in Programming


102


64-102


In concurrency theory, weak bisimilarity is often used to relate processes exhibiting the same observable behaviour. The probabilistic environment gives rise to several generalisations; we study the infinitary semantics, which abstracts from a potentially unbounded number of internal actions being performed when something observable happens. Arguing that this notion yields the most desirable properties, we provide a sound and complete axiomatisation capturing its essence. Previous research has failed to achieve completeness in the presence of unguarded recursion, as only the finitary variant has been axiomatised, yet.


Elsevier


Axiomatisation; Process algebra; Probability; Recursion


Computational Logic and Formal Languages


https://doi.org/10.1016/j.jlamp.2018.09.006


Link to Publisher's Version


EP188524


Journal article - Refereed


English


Fischer, Nick; van Glabbeek, Rob. Axiomatising Infinitary Probabilistic Weak Bisimilarity of Finite-State Behaviours. Journal of Logical and Algebraic Methods in Programming. 2019; 102:64-102. https://doi.org/10.1016/j.jlamp.2018.09.006



Loading citation data...

Citation counts
(Requires subscription to view)