Fixed Point Semantics in Process Algebras

摘要

Nondeterministic uniform processes as introduced by de Bakker and Zucker, with composition, union, merge, mu-operator, and semantics in metric spaces are considered. A collection of such processes are represented as the projective limit of collections of finite processes. Here a finite process is generated from a set of atomic actions by means of the operations sequential composition and nondeterministic union. The process algebra thus obtained is augmented by an operation ''left merge' in terms of which the usual merge operator is defined. The existence of solutions of equations x = s(x), where s(x) is a mu-free expression, is shown. This yields the existence of a fixed point semantics for process expressions containing the mu-operator. The proof amounts to a combinatorial analysis showing that certain iteration sequences stabilize on each finite level.