Approximating Weak Bisimilarity of Basic Parallel Processes

TL;DR

This paper investigates approximation methods for deciding weak bisimilarity in Basic Parallel Processes, analyzing their effectiveness and limitations, and establishing lower bounds that answer open questions in the field.

Contribution

It introduces bounds for approximation techniques and clarifies their limitations, advancing understanding of weak bisimilarity decision procedures.

Findings

Lower bound of ω * ω for approximants with weak steps

Lower bound of ω + ω for approximants with action sequences

Negative answer to an open question by Jančar and Hirshfeld

Abstract

This paper explores the well known approximation approach to decide weak bisimilarity of Basic Parallel Processes. We look into how different refinement functions can be used to prove weak bisimilarity decidable for certain subclasses. We also show their limitations for the general case. In particular, we show a lower bound of {\omega} \ast {\omega} for the approximants which allow weak steps and a lower bound of {\omega} + {\omega} for the approximants that allow sequences of actions. The former lower bound negatively answers the open question of Jan\v{c}ar and Hirshfeld.