Programming Research Group  -  University of Amsterdam  -  TR P9805 


           Some Verifications in Process Algebra with Iota
            
                         Mark van der Zwaag


In this paper, I present the process  algebra  ACP  extended  with a
constant iota that will be used to represent internal activity.

The  representation  of internal  activity  that is standard  in the
literature  is the silent  step tau.  The silent  step  behaves as a
right unit for sequential  composition  and therefore has a tendency
to disappear during  verifications.  The internal step iota does not
disappear.  Typically,  internal  activity  renamed into iota can be
compressed  to a  single  iota-action,  acting  as an  indicator  of
internal activity, but this is not always the case.

I will interpret  process  expressions in the frame model.  Although
frames have been around for a while, this  interpretation  has never
been made precise.

The  introduction of the internal step gives rise to a new notion of
equivalence   between   processes,   so-called   rooted   orthogonal
bisimilarity.

One of the main reasons to consider  this new  constant  lies in the
problems involved in incorporating a priority  operator in a process
algebra with the silent  step.  I claim that the  priority  operator
theta can be successfully combined with the internal step.

Three well-known simple protocols are verified:  the Alternating Bit
Protocol, the Concurrent  Alternating  Bit Protocol and the Positive
Acknowledgement  and Retransmission  Protocol.  These  verifications
differ from existing verifications not only in the representation of
internal   activity   but   also  in  the   absence   of   recursive
specifications; components are specified with the binary Kleene star
operator and during the  verifications  no  recursive  specification
principles are used.