Axiomatising Infinitary Probabilistic Weak Bisimilarity of Finite-State Behaviours

TL;DR

This paper develops a sound and complete axiomatisation for infinitary probabilistic weak bisimilarity in finite-state behaviors, addressing a gap in the theoretical understanding of unbounded internal actions in probabilistic processes.

Contribution

It introduces the first complete axiomatisation for infinitary probabilistic weak bisimilarity, extending previous finitary results to include unguarded recursion.

Findings

Provides a sound and complete axiomatisation for the infinitary case

Addresses the challenge of unguarded recursion in probabilistic bisimilarity

Enhances the theoretical framework for reasoning about infinite behaviors in probabilistic systems

Abstract

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.