================================================================================
P9306b  J.A. Bergstra, A. Ponse & J.J. van Wamel
        "Process algebra with backtracking"
        (revised version of P9306)


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.



TO APPEAR IN 

@inproceedings{P9306b,
        author =        {J.A. Bergstra and A. Ponse and J.J. van Wamel},
        title =         {Process algebra with backtracking},
        pages =         {},
        booktitle =     {A Decade of Concurrency - Reflections and
                         Perspectives (REX Proceedings)},
        place =         {Noordwijkerhout},
        year =          {1993},
        editor =        {G. Rozenberg},
        series =        {LNCS},
        volume =        {},
        publisher =     {Springer}
}