Robustness of a bisimulation-type faster-than preorder

TL;DR

This paper investigates the robustness of bisimulation-type faster-than preorders in TACS, an extension of CCS with timing, showing that most variants maintain the same preorder under extended semantics, with some exceptions.

Contribution

It extends the operational semantics of TACS and analyzes the robustness of different bisimulation variants, highlighting which variants preserve the preorder.

Findings

Two variants maintain the same preorder under extended semantics.

One variant fails to preserve the preorder after extension.

Mixing old and new semantics can produce smaller relations still proving the same preorder.

Abstract

TACS is an extension of CCS where upper time bounds for delays can be specified. Luettgen and Vogler defined three variants of bismulation-type faster-than relations and showed that they all three lead to the same preorder, demonstrating the robustness of their approach. In the present paper, the operational semantics of TACS is extended; it is shown that two of the variants still give the same preorder as before, underlining robustness. An explanation is given why this result fails for the third variant. It is also shown that another variant, which mixes old and new operational semantics, can lead to smaller relations that prove the same preorder.