Kahn's fixed-point characterization for linear dynamic networks

Abstract

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 [BN96, BN97]. 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 O_n. We also define a deterministic transition system DT and prove that the operational semantics O _d derived from DT is the same as O _n. Finally, we define a denotational semantics D and prove D = O _d. This implies O _n = D. Thus the second part of the Kahn principle is established.