LINEAR DYNAMIC KAHN NETWORKS ARE DETERMINISTIC

The (first part of the) Kahn principle states that networks with deter ministic nodes are deterministic on the I/O level: for each network, d ifferent executions provided with the same input streams deliver the s ame output streams. The Kahn principle has thus far not been proved fo r dynamic, nondeterministic networks. We consider a simple language L containing the fork-statement. For this language we introduce a nondet erministic transition system which defines all interleavings consistin g of basic steps, for all possible executions of a program. We prove t hat, although on the execution level there is much nondeterminism, thi s nondeterminism disappears because all executions deliver the same ou tput stream (or a prefix of it), given the same input stream. This pro ves the Kahn principle for linear, nondeterministic dynamic networks.