Convergence Theorem in Process Algebra

摘要

A convergence phenomenon in the projective limit model A sup inf for process algebra, an axiom system in the framework of process algebra for processes built from atomic actions by means of alternative composition (+) and sequential composition (x), and subject to the operations merge and left-merge is studied. The model is also a complete metric space. It is shown that for every element q is a member of the set A sup inf the sequence q, s(q), s sq(q) ..., s sup n(q) ... converges to a solution of the (possibly unguarded) recursion equation X = s(X) where s(X) is an expression in the signature of PA involving the recursion variable X. As the convergence holds for arbitrary starting points q, this result does not seem readily obtainable by the usual convergence proof techniques. The connection is between projective models and models based on process graphs is studied. These models are compared with the process model introduced by De Bakker and Zucker (1982).