Kahn's fixed-point characterization for linear dynamic networks

We consider dynamic Kahn-like dataflow networks defined by a simple language L containing the fork-statement. The first part of the Kahn principle states that such networks are deterministic on the I/O level: for each network, different executions provided with the same input deliver the same output. The second part of the principle states that the function from input streams to output streams (which is now defined because of the first part) can be obtained as a fixed point of a suitable operator derived from the network specification. The first part has been proven by us in an earlier publication. To prove the second part, we will use the metric framework. We introduce a nondeterministic transition system NT from which we derive an operational semantics On. We also define a deterministic transition system DT and prove that the operational semantics Od derived from DT is the same as On. Finally, we define a denotational semantics D and prove D = Od. This implies On =