================================================================================
P9322   N.J. Drost
        "Unification in an algebra with choice and sequential composition"


This paper contains a unification algorithm for a restricted process algebra 
with as only operators nondeterministic choice + (associative, commutative, 
idempotent, and with unit element) and sequential composition . 
(associative, right-distributive over +, and with left zero element). 
The algebra contains only finite processes. The algorithm is based on rules, and
is proved sound and complete. As unification in this algebra is infinitary, the 
algorithm does not terminate in  general. Termination is proved for problems 
consisting of equations where at least one of the two terms is closed. In
this case the produced set of solutions is also a minimal set of most general
unifiers, and the algorithm has exponential complexity. 


ALSO APPEARED IN:

@phdthesis{Dro94,
        author =        {N.J. Drost},
        year =          1994,
        month =         feb,
        school =        {University of Amsterdam},
        title =         {Process theory and equation solving}
}