Process algebra with backtracking

Abstract

An extension of process algebra for modelling processes with backtracking is introduced. This extension is semantically based on processes that transform data because, in our view, backtracking is the undoing of the effects caused by a process in some initial data-state if this process fails. The data-states are given by a data environment, which is a structure that also defines in which data-states guards hold, and how (atomic) actions either transform these states or block and prevent subsequent processes from being executed. State operators are used to relate process terms to a given data environment. Backtracking is axiomatised in a few phases. First guarded commands (conditionals) and a standard type of guards, expressing the enabledness of actions, are added to basic process algebra (process algebra without operators for parallelism) by involving a Boolean algebra. Then the set of actions is partitioned in order to distinguish between different types of behaviour of actions in the scope of a (binary) operator for backtracking. Also functions on actions are defined that change the ‘type’ of an action. Next an axiom system for modelling processes with backtracking is presented, and it is proved that backtracking is associative, provided that some semantic constraints are satisfied. Finally a method for recursively specifying processes is defined and an example of a recursively defined process with backtracking is provided. An operational semantics is defined relative to the Boolean algebra, describing transitions between process terms labelled with ‘guarded actions’. The operational semantics is studied modulo strong bisimulation equivalence.