Splitting bisimulations and retrospective conditions

Abstract

We investigate conditions in the setting of the algebraic theory about processes known as ACP. We present ACPc, an extension of ACP with guarded commands, and its main models, called its full splitting bisimilation models. The conditions used in the guarded commands are taken from a Boolean algebra. We add two operators for condition evaluation to ACPc; and study their connection with alternative mechanisms found in other extensions of ACP with guarded commands, to wit state operators and signal emission. On purpose to incorporate the past in conditions, we add a retrospection operator on conditions to ACPc.

Preprint available here.