Denotational Semantics of Nets with Nondeterminism

摘要

A topological framework for streams of traces, in which Kahn's method generalizes to nets with bounded nondeterminism is defined. Fixpoints of multivalued functions are considered. A standard fixed point theorem can be used to model feedback loops, as can iteration. A general syntax of nets is used to analyze them in the stream framework. It is shown how to avoid the Brock-Ackerman and Keller anomalies. The fair merge, which is a continuous function in the framework, and delay along lines are modeled. A lemma which says that the order in which nodes are connected does not matter, is proved. For nodes with unbounded nondeterminism, fixpoints can be employed without losing the iteration theorem in the topological framework.