On convergence-sensitive bisimulation and the embedding of CCS in timed CCS

TL;DR

This paper introduces a convergence-sensitive bisimulation concept based on reduction and context, characterizes it within timed CCS, and demonstrates its use for embedding untimed processes into timed ones, including divergence sensitivity.

Contribution

It presents a new bisimulation notion that is sensitive to convergence, providing a semantic framework for embedding untimed processes into timed CCS.

Findings

Characterizes convergence-sensitive bisimulation via labelled transition systems

Provides a fully abstract embedding of untimed into timed processes

Refines the bisimulation to account for divergence sensitivity

Abstract

We propose a notion of convergence-sensitive bisimulation that is built just over the notions of (internal) reduction and of (static) context. In the framework of timed CCS, we characterise this notion of `contextual' bisimulation via the usual labelled transition system. We also remark that it provides a suitable semantic framework for a fully abstract embedding of untimed processes into timed ones. Finally, we show that the notion can be refined to include sensitivity to divergence.