Bisimulation respecting first-order operations

Abstract

We identify two features of common process algebra operations: their first-order flavour and the fact that they respect bisimulation in a uniform manner. For this purpose two notions are introduced: first, a notion of first-order definable operations on process graphs and second, respect for sequence extension. In the first part of the paper those first-order definable operations are characterised whose defining formulas respect sequence extension. The second part uses the resulting format to calculate modal preconditions: it gives an algorithm that reduces modal truth in the output of certain process graph operations to modal truth in the inputs of this operation.