Digital Signal Processing Reference
In-Depth Information
Proposition 1.
The input/output relation of a determinate labeled transition system
is a continuous function.
λ
is a labeled transition system, we use
is determinate, this is an I/O
function
.
An important property in process networks is a deadlock condition. We can
define a deadlock as the possibility to reach a state from which no further transitions
are possible, a finite maximal execution. It is usually called a deadlock only if this
is an undesirable situation. An important corollary from the analysis above is that if
a determinate LTS has some execution which leads to a deadlock state, then
all of
its executions
lead to the same deadlock state. In other words, the deadlock cannot
be avoided by a smarter scheduling strategy, it is inherent to the determinate LTS
specification and as we will see, therefore also holds for KPN.
f
λ
to denote its I/O relation. In particular, if
λ
3.3
Operational Semantics
We can now formalize an operational semantics of a KPN as a determinate LTS.
Definition 4.
(K
AHN PROCESS NETWORK
) A Kahn process network is a tuple
(
P
,
C
,
I
,
O
,
Act
,{
λ
p
|
p
∈
P
}
)
that consists of the following elements:
A finite set
P
of
processes
.
A finite set
C
⊆
Chan
of
internal channels
, a finite set
I
⊆
Chan
of input channels
and a finite set
O
⊆
Chan
of output channels, all distinct.
Every constituent process
p
∈
P
is itself defined by a determinate labeled
transition system
λ
p
=(
S
p
,
s
p
,
0
,
I
p
,
O
p
,
Act
p
,
p
)
, with
I
p
⊆
I
∪
C
and
O
p
⊆
O
∪
C
.
of internal actions of the processes are disjoint.
Theset
Act
of
actions
consisting of the actions of the constituent processes:
Act
The sets
Act
p
\
(
Act
p
|
(
I
p
∪
O
p
))
=
p
∈
P
Act
p
.
For every channel
c
∈
C
∪
I
, there is exactly one process
p
∈
P
that reads from it
(
c
∈
I
p
) and for every channel
c
∈
C
∪
O
, there is exactly one process
p
∈
P
that
O
p
).
To define the operational semantics of a KPN, we need a notion of
global state
of
the network; this state is composed of the individual states of the processes and the
current contents of the internal channels. A configuration of the process network is
apair
writes to it (
c
∈
(
π
,
γ
)
consisting of a process state
π
and a channel state
γ
,where
=
p
∈
P
S
p
is a function that maps every process
p
a
process state
π
:
P
→
S
∈
P
on a local state
π
(
p
)
∈
S
p
of its transition system;
→
Σ
∗
is a history function that maps every internal channel
a
channel state
γ
:
C
Σ
c
.
The set of all configurations is denoted by
Confs
and there is a designated initial
configuration
c
0
=(
π
0
,
γ
0
)
c
∈
C
on a
finite
string
γ
(
c
)
over
,where
π
0
maps every process
p
∈
P
to its initial state
