Using a Partial Order and a Metric to Analyze a Recursive Trace Set Equation
Jan Tijmen Udding · Open Scholarship Institutional Repository (Washington University in St. Louis) · 1988
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.