Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours

Nick Fischer, Rob van Glabbeek

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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.
Original languageEnglish
Pages (from-to)64-102
Number of pages39
JournalJournal of Logical and Algebraic Methods in Programming
Volume102
Early online date19 Oct 2018
DOIs
Publication statusPublished - 1 Jan 2019

Keywords / Materials (for Non-textual outputs)

  • Axiomatisation
  • Process algebra
  • Probability
  • Recursion

Fingerprint

Dive into the research topics of 'Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours'. Together they form a unique fingerprint.

Cite this