Kahn Process Networks and a Reactive Extension - Signal Processing Systems - page 1034

Using the operational semantics of KPN, we can now reason about resources
such as buffer capacities for the FIFOs connecting the processes. Abstracting from
specific buffer sizes, we can also consider whether finite buffer capacities are
sufficient. In the Fibonacci example of Fig. 3 , there exist executions which require
a buffer size of 2 on channel e , for instance if we take the path according to the
upper envelope of the picture, two write actions occur in the channel e before the
first read action. The path along the bottom envelope of the picture requires only a
buffer size of 1 for channel e because the first read occurs before the second write.
An execution

σ is bounded if there exists a mapping B : C → N such that at any state

( π , γ ) C . Not every KPN allows a bounded execution.

Some KPNs may have both bounded and unbounded executions. This is relevant for
realizations of KPNs, as discussed in Sect. 6 .

of σ , | γ ( c ) |≤ B ( c ) for all c ∈

4 The Kahn Principle

The operational semantics given in the previous section is a model closer to a
realization of a KPN than the denotational semantics of Sect. 2 . The denotational
semantics defines behavior as the least solution to a set of network equations [ 29 ] .
The correspondence between both semantics, demonstrating that they are consistent,
is referred to as the Kahn Principle . It was stated convincingly, but without proof,
by Kahn in [ 29 ] and was later proved by Faustini [ 17 ] for an operational model of
process networks, in [ 48 ] for an operational model of concurrent transition systems
and in [ 38 ] for an operational characterization using I/O automata.
Based on the operational semantics, a determinate LTS, a functional relation is
obtained between inputs and outputs. This function is shown to correspond to the
least solution of Kahn's network equations.
The proof presented here is similar to the proof of the Kahn Principle for
I/O automata of [ 38 ] . We reproduce it here in outline, because it illustrates the
connections between denotational and operational semantics and the essential
properties of the KPN model. We first show that if the operational behaviors of
individual processes of the KPN respect their functional specifications, then so does
the KPN as a whole. For an execution

σ with input i , we use the notation h ( σ , i )

to denote the history identical to h except for the input channels, which are

mapped according to i , since some of the input of i offered to the network may not
(yet) have been consumed. Thus h

( σ )

.We
can derive from an execution of the overall KPN how individual processes have
contributed to that execution.

( σ , i ) is equal to the mapping i ∪ σ ! ( C ∪ O )

σ | p denotes execution σ projected on process p .If

α n 0

α 0 α 1 α 2

σ =( π 0 , γ 0 ) ( π 1 , γ 1 ) ( π 2 , γ 2 ) ... .Then σ | p = π n 0 ( p ) π n 1 ( p )

α n 1 α n 2

π n 2 ( p ) ... where n 0 , n 1 etcetera are such that n 0 < n 1 <... and α n 0 ,

α n 1 , ...are precisely the actions from process p .