Skip to main content

Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours

Authors

Nick Fischer and Rob van Glabbeek

DATA61

Saarland University

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.

BibTeX Entry

  @article{Fischer_Glabbeek_19,
    publisher        = {Elsevier},
    doi              = {10.1016/j.jlamp.2018.09.006},
    journal          = {Journal of Logical and Algebraic Methods in Programming},
    author           = {Fischer, Nick and van Glabbeek, Rob},
    month            = jan,
    volume           = {102},
    keywords         = {axiomatisation; process algebra; probability; recursion},
    year             = {2019},
    date             = {2019-1-2},
    title            = {Axiomatising Infinitary Probabilistic Weak Bisimilarity of Finite-State Behaviours},
    pages            = {64-102}
  }

Download

Served by Apache on Linux on seL4.