Bisimilarity and Simulatability of Processes Parameterized by Join Interactions

TL;DR

This paper introduces a weakened form of parameterized bisimilarity based on join interactions, explores its properties, and extends the concept to simulatability, providing logical characterizations and discussing its relation to existing notions.

Contribution

It defines and analyzes join-interaction parameterized bisimilarity and simulatability, showing their relation to existing concepts and providing modal logic characterizations.

Findings

Join-interaction parameterized bisimilarity coincides with parameterized bisimilarity in deterministic environments.

The weakened bisimilarity is coarser than the original in general.

Modal logic characterizes parameterized simulatability and bisimilarity.

Abstract

Departing from Larsen's concept of parameterized bisimilarity of processes with respect to interaction with environments, we start an exploration of its natural weakening: bisimilarity of unrestricted join interactions with environments. Parameterized bisimilarity relates processes p and q with respect to an environment e if p and q behave bi-similarly while joining -- respectively the same -- transitions from e. The weakened variant relates processes p and q with respect to environment e if the join-interaction processes p & e and q & e of p and q with e are bisimilar. (Hereby join interactions r & f facilitate a step with label a to r' & f' if and only if r and f permit a-steps to r' and f' , respectively.) Join-interaction parameterized (ji-parameterized) bisimilarity coincides with parameterized bisimilarity for deterministic environments, but that it is a coarser equivalence in general. We explain how Larsen's concept can be recovered from ji-parameterized bisimilarity by 'determinizing' interactions. We show that by adaptation to simulatability (simulation preorder) the same concept arises: parameterized simulatability coincides with ji-parameterized simulatability. For the discrimination preorder of (ji-)parameterized simulatability on environments we obtain the same result as Larsen did for parameterized bisimilarity. Also, we give a modal-logic characterization of (ji-)parameterized simulatability. Finally we gather open problems, and provide an outlook on our current related work.