A New Branching Bisimulation for Probabilistic Processes
Logic in Computer Science
Summary
The authors propose a new way to compare probabilistic processes called branching bisimulation, which is more detailed than existing methods that ignore invisible steps. They also develop a rooted version of this comparison, ensuring it works smoothly with typical programming features like recursion. This helps better understand and verify complex systems that involve both chance and hidden actions.
Authors
Guo Li, Zhaokai Li, Xinxin Liu, Zhiming Liu, Quan Sun, Wei Zhang
Abstract
We introduce a new branching bisimulation for probabilistic processes, which induces a more refined equivalence relation than any known equivalence that abstracts from unobservable actions, with a rooted version that is a congruence for a language of probabilistic process with the usual static as well as dynamic constructs including recursion.