Technical Report Number
In Trace Theory the notion of a process is defined in terms of a set of finite-length traces over an alphabet. These processes are used as the semantics for a program notation. The program text for a recursive component naturally gives rise to an equation over trace sets. This paper takes two approaches at the analysis of that equation. The first approach is based on a partial order and it concentrates on the projection operator for processes. This yields a condition under which the greatest solution of that equation can be approximated by iteration. The second approach introduces a metric on the process domain. Application of Banach's Contraction Theorem results in a condition under which there exists a unique solution that can be approximated by iteration starting anywhere.
Udding, Jan Tijmen and Verhoeff, Tom, "Using a Partial Order and a Metric to Analyze a Recursive Trace Set Equation" Report Number: WUCS-88-17 (1988). All Computer Science and Engineering Research.