Order, Topology, and Recursion Induction in CSP

Abstract

Recursion induction is a method for proving that CSP processes which are defined as the least fixed points of some Scott-continuous function from a complete partial order on the set of all processes to itself meet a given behavioural specification. The Scott (order version) requires that (1) the specification S is closed via the least upper bound of directed sets in the complete partial order, (2) S(bottom), and (3) if S(P then S(F(P). It is then concluded that S(fix(F)), where fix(F) is the least fixed point of F. This version uses the Tarski fixed point theorem. The Roscoe (topology version) assumes not only the complete partial order on the set of all processes, but also a complete metric on the set of all processes. This version requires that the recursive function F be a contraction function with respect to the complete metric. It requires (1) S is closed with respect to limits in the complete metric, (2) there exists a P such that S(P), and (3) if S(P) then S(F(P). Again, it is then concluded that S(fix(F)), where fix(F) is the unique fixed point of F. This version uses the Banach fixed point theorem. The Scott version is sufficient in the traces model for CSP, since most useful predicates are satisfied by (bottom = STOP). However in the failures-divergences model, the Roscoe version is required, since few useful predicates are satisfied by (bottom = CHAOS). The usual model for the failures-divergences model is a Scott domain (i.e., an algebraic, bounded-complete, complete partial order), where the maximal elements are exactly the non-deterministic processes. The complete metric used for the Roscoe fixed point version agrees with the Scott topology on the set of maximal elements. In this talk we develop a general theory for recursion induction based on the Scott topology of the maximal elements in a domain. The theory assumes no other information, hence it is only applicable for functions which have their least fixed point as a maximal element. It includes all complete metric spaces. It covers spaces which are not metrizable. It covers the existing examples for recursion induction in CSP. As a result of our topological analysis, we answer several open questions in the literature about the topology of the set of maximal elements in a domain. One interesting example is showing that one proposition is independent and consistent with ZFC.