Clocks, Trees and Stars in Process Theory
Wan Fokkink

Abstract:
Process algebra, or process theory, constitutes an attempt to reason about 
`behaviours of systems' in a mathematical framework. Starting from a syntax,
each syntactic object is supplied with some kind of behaviour, and a semantic 
equivalence says which behaviours are to be identified. (Bisimulation is such 
a semantic equivalence.) Process algebra expresses semantic equivalences in 
axioms, or equational laws. It requires that a set of axioms is sound (i.e. if 
two behaviours can be equated, then they are semantically equivalent), and it 
desires that it is complete (i.e. if two behaviours are semantically 
equivalent, then they can be equated). Process algebra can be applied to prove 
correctness of system behaviour. It enables to express (un)desirable properties 
of the behaviour of a system in an abstract way, and to deduce by mathematical 
manipulations whether or not the behaviour satisfies such a property. 

Forty years ago, Kleene introduced a binary operator x*y, called iteration or 
Kleene star. The process x*y can choose to execute either x, after which it 
evolves into x*y again, or y, after which it terminates. In Chapter 3 it is 
proved that BPA extended with iteration, modulo bisimulation, is axiomatized 
completely by the five standard axioms for BPA together with three extra 
axioms for iteration. In Chapter 2 it is proved that basic CCS extended with 
prefix iteration a*x, where the left argument is restricted to atomic actions, 
is axiomatized completely, modulo bisimulation, by the four standard axioms 
for basic CCS together with two extra axioms for prefix iteration. 

In order to describe a semantic equivalence by means of axioms, it is essential 
that such an equivalence is a congruence. Groote and Vaandrager proved that 
behaviours generated by well-founded Plotkin rules in the tyft/tyxt format are 
always a congruence for strong bisimulation. In Chapter 4 it is shown that the 
well-foundedness restriction can be omitted in this congruence result. This 
follows from a stronger result, which says that for each collection of 
transitions rules in tyft/tyxt format, there is an equivalent collection of 
transition rules in the more restrictive tree format. 

In Chapter 5, a classic result from unification theory, which says that if a 
finite set of equations allows a unifier then it allows an idempotent most 
general unifier, is generalized to infinite sets. 

In Chapter 6, a subalgebra of the regular processes in ACPrI with recursion is 
determined, such that for each pair of processes p and q in this algebra, their 
merge p||q is in this algebra too. The subalgebra is very specific, because if 
it is enlarged or restricted in any obvious way, then this elimination result 
is lost. The discovered algebra is equal to the class of timed automata of 
Alur and Dill. 

In Chapter 7 it is proved that strong bisimulation equivalence for the timed 
process algebra ACPrI is decidable, i.e. for each pair of terms in ACPrI it 
can be decided whether or not they are bisimilar.

Finally, Chapter 8 presents a complete axiomatization for Basic Process Algebra 
extended with the constants silent step and deadlock and recursion and time,