In computer science, a channel system is a finite state machine similar to communicating finite-state machine in which there is a single system communicating with itself instead of many systems communicating with each other. A channel system is similar to a pushdown automaton where a queue is used instead of a stack. Those queues are called channels. Intuitively, each channel represents a sequence a message to be sent, and to be read in the order in which they are sent.
Formally, a channel system (or perfect channel system)
S
\langleQ,C,\Sigma,\Delta\rangle
Q=\{q1,...,qm\}
q0\inQ
A
\epsilon\inA
C=\{c1,...,cn\}
\Sigma=\{a1,...,ap\}
\Delta\subseteqQ x C x \{?,!\} x \Sigma* x A x Q
\Sigma*
\Sigma
Depending on the author, a channel system may have no initial state and may have an empty alphabet.[2]
A configuration or global state of the channel system is a
n+1
| n(\Sigma | |
| Q x \prod | |
| i=1 |
*)
\gamma=(q,w1,...,wm)
q
i
wi
The initial configuration is
(q0,\epsilon,...,\epsilon)
\epsilon
Intuitively, a transition
(q,ci,!,u,a,q')
q
q'
u
ci
(q,ci,?,u,a,q')
q
q'
u
ci
Formally, given a configuration
(q,w1,...,wm)
(q,ci,!,u,q')
(q,w1,...,wi-1,wi,wi+1,...,wm)\xrightarrow{a}perf(q',w1,...,wi-1,wiu,wi+1,...,wm)
u
i
(q,ci,?,u,q')
(q,w1,...,wi-1,uwi,wi+1,wm)\xrightarrow{a}perf(q',w1,...,wi-1,wi,wi+1,...,wm)
i
u
A perfect run is a sequence of perfect step, of the form
\gamma0\xrightarrow{a0}perf\gamma1...
\gamma\xrightarrow[perf]{*}\gamma'
\gamma
\gamma'
Given a perfect or a lossy channel system
S
A word over
A*
S
S
S
S
The set of reachable configuration of
S
R(S)
\gamma
\gamma'
(q0,\epsilon,...,\epsilon)\xrightarrow{*}\gamma'
Given a channel
c
c
(w1,...wm)
(c,w1,...,wm)\inR(S)
Most problem related to perfect channel system are undecidable.[3] This is due to the fact that such a machine may simulates the run of a Turing machine. This simulation is now sketched.
M
S
M
n
S
O(n2)
Multiple variants of channel systems have been introduced. The two variants introduced below does not allow to simulate a Turing machine and thus allows multiple problem of interest to be decidable.
A one-channel machine is a channel system using a single channel. The same definition also applies for all variants of channel system.
When the alphabet of a channel system contains a single message, then each channel is essentially a counter. It follows that those systems are essentially Minsky machines. We call such systems counter machines. This same definition applies for all variants of channel system.[4]
A completely specified protocol (CSP) is defined exactly as a channel system. However, the notion of step and of run are defined differently.
A CSP admits two kinds of steps. Perfect steps, as defined above, and a message loss transition step. We denote a message loss transition step by
(q,w1,...,a ⋅ wi,...,wm)\rightsquigarrow(q,w1,...,wi,...,wm)
A lossy channel system or machine capable of lossiness error is an extension of completely specified protocol in which letters may disappear anywhere.
A lossy channel system admits two kinds of steps. Perfect steps, as defined above, and lossy step. We denote a lossy step,
(q,w1,...,wi ⋅ a ⋅ w'i...,,wm)\rightsquigarrow(q,w1,...,wi ⋅ w'i,w'm)
A run in which channel are emptied as soon as messages are sent into them is a valid run according to this definition. For this reason, some fairness conditions may be introduced to those systems.
Given a message a channel
c
c
c
c
A computation is said to be channel fair if it is channel fair with respect to each channel
c
The impartiality condition is a restriction to the channel fairness condition in which both the channel and the letter are considered.
Given a message
m
c
c
m
m
c
m
c
A computation is said to be impartial with respect to a channel
c
c
m
c
The message fairness property is similar to impartiality, but the condition only have to hold if there is an infinite number of step at which
m
c
m
m
c
i
q
(q,m,q')
m
c
The run is said to have bounded lossiness if the number of letter removed between two perfect steps is bounded.
A machine capable of insertion of error is an extension of channel system in which letters may appear anywhere.
A machine capable of insertion of error admits two kinds of steps. Perfect steps, as defined above, and insertion steps. We denote an insertion step by
(q,w1,...,wi ⋅ w'i...,,wm)\rightsquigarrow(q,w1,...,wi ⋅ a ⋅ w'i,w'm)
A machine capable of duplication error is an extension of machine capable of insertion of error in which the inserted letter is a copy of the previous letter.
A machine capable of insertion of error admits two kinds of steps. Perfect steps, as defined above, and duplication steps. We denote an insertion step by
(q,w1,...,wi ⋅ a ⋅ w'i...,,wm)\rightsquigarrow(q,w1,...,wi ⋅ a ⋅ a ⋅ w'i,w'm)
A non-duplicate machine capable of duplication error is a machine which ensures that in each channel, the letters alternate between a special new letter #, and a regular letter from the alphabet of message. If it is not the caes, it means a duplication occurred and the run rejects. This process allow to encode any channel system into a machine capable of duplication error, while forcing it not to have errors. Since channel systems can simulate machines, it follows that machines capable of duplication error can simulate Turing machine.
The set of reachable configurations is recognizable for lossy channel machines and machines capable of insertions of errors. It is recursively enumerable for machine capable of duplication error.
This section contain a list of problems over channel system, and their decidability of complexity over variants of such systems.
The termination problem consists in deciding, given a channel system
S
\gamma
S
\gamma
This problem is decidable but nonprimitive recursive over lossy channel system. This problem is trivially decidable over machine capable of insertion of errors.
The reachability problem consists in deciding, given a channel system
S
\gamma
\gamma'
S
\gamma
\gamma'
The deadlock problem consists in deciding whether there is a reachable configuration without successor. This problem is decidable over lossy channel system and trivially decidable over machine capable of insertion of errors. It is also decidable over counter machine.[5]
The model checking problem consists in deciding whether given a system
S
\phi
S
\phi
The recurrent state problem consists in deciding, given a channel system
S
\gamma
s
S
\gamma
s
Given a system
S
R(S)
The boundedness problem consists in deciding whether the set of reachable configuration is finite. I.e. the length of the content of each channel is bounded. This problem is trivially decidable over machine capable of insertion of errors. It is also decidable over counter machine.
The eventuality property, or inevitability property problem consists in deciding, given a channel system
S
\Gamma
S
\gamma
\Gamma
The safety property problem consists in deciding, given a channel system
S
R
The structural termination problem consists in deciding, given a channel system
S
S
Hierarchical state machines are finite state machines whose states themselves can be other machines. Since a communicating finite state machine is characterized by concurrency, the most notable trait in a communicating hierarchical state machine is the coexistence of hierarchy and concurrency. This had been considered highly suitable as it signifies stronger interaction inside the machine.
However, it was proved that the coexistence of hierarchy and concurrency intrinsically costs language inclusion, language equivalence, and all of universality.[7]