Content deleted Content added
Fix cite date errors |
m compound modifier |
||
| (18 intermediate revisions by 12 users not shown) | |||
Line 1:
{{redirect|Channel system|Earth's sea floor|Abyssal channel}}
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.▼
{{short description|Finite-state machine with fifo buffers for memory}}
▲In [[computer science]], a '''channel system''' is a [[finite
== Definition ==
=== Channel system ===
Formally, a '''channel system''' (or '''perfect channel system''') <math>S</math> is defined as a tuple <math>\langle Q,C,\Sigma,\Delta \rangle</math> with:
* <math>Q=\{q_1,\dots,q_m\}</math> a finite set of '''control states''',
* <math>q_0\in Q</math> an '''initial state''',
* <math>A</math> a finite alphabet (for the sake of notation simplicity, let <math>\epsilon \in A</math>),
* <math>C=\{c_1,\dots,c_n\}</math> a finite set of '''channels''',
* <math>\Sigma=\{a_1,\dots,a_p\}</math> a finite alphabet of '''messages''',
* <math>\Delta\subseteq Q\times C\times\{?,!\}\times\Sigma^*\times
Depending
=== Configuration ===
Line 19 ⟶ 22:
=== Step ===
Intuitively, a transition <math>(q,c_i,!,u,a,q')</math> means that the system may goes to control state <math>q</math> to <math>q'</math> by
Formally, given a configuration <math>(q,w_1,\dots,w_m)</math>, and a transition <math>(q,c_i,!,u,q')</math>, there is a perfect step <math>(q,w_1,\dots, w_{i-1}, w_i, w_{i+1},\dots,w_m)\xrightarrow{a}_{\mathtt{perf}}(q',w_1,\dots,w_{i-1},w_iu,w_{i+1},\dots,w_m)</math>, where the step adds a letter <math>u</math> to the end of the <math>i</math>-th word.
=== Run ===
Line 29 ⟶ 32:
Given a perfect or a lossy channel system <math>S</math>, multiple languages may be defined.
A word over <math>A^*</math> is accepted by <math>S</math> if it
The set of reachable configuration of <math>S</math>, denoted <math>R(S)</math> is defined as the set of configuration <math>\gamma</math> reachable from the initial state. I.e. as the set of configurations <math>\gamma'</math> such that <math>(q_0,\epsilon,\dots,\epsilon)\xrightarrow{*}\gamma'</math>.
Line 36 ⟶ 39:
== Channel system and Turing machine ==
Most problem related to perfect channel system are undecidable{{r|decidable|p=92}}.<ref name="easier">{{cite journal |last1=Cécé |first1=Gérard|last2=Finkel|first2=Alain |title=Unreliable Channels Are Easier to Verify Than Perfect Channels|journal =Information and Computation |date=10 January 1996 |volume=124 |issue=1 |pages=
Given a [[Turing machine]] <math>M</math>, there exists a perfect channel system <math>S</math> such that any run of <math>M</math> of length <math>n</math> can be simulated by a run of <math>S</math> of length <math>O(n^2)</math>. Intuitively, this simulation consists simply in having the entire tape of the simulated Turing machine in a channel. The content channel is then entirely read
== Variants ==
Line 47 ⟶ 50:
=== Counter machine ===
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 machine]]s. We call such systems '''counter machines'''. This same definition applies for all variants of channel system.<ref name="Counter">{{cite journal|first1=Richard|last1=Mayr|doi=10.1016/S0304-3975(02)00646-1|title=Undecidable problems in unreliable computations|volume=297|issue=
=== Completely specified protocol ===
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 <math>(q,w_1,\dots,a\cdot w_i,\dots,w_m)\rightsquigarrow(q,w_1,\dots,w_i,\dots,w_m)</math>.
=== Looseness ===
A '''lossy channel system''' or '''machine capable of
A lossy channel system admits two kinds of steps. Perfect steps, as defined above, and lossy step. We denote a lossy step, <math>(q,w_1,\dots,w_i\cdot a\cdot w'_i\dots,,w_m)\rightsquigarrow(q,w_1,\dots,w_i\cdot w'_i,w'_m)</math>.
▲It should be noted that 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.
==== Channel fairness ====
Given a message a channel <math>c</math>, a run is said to be channel fair with respect to <math>c</math> if, assuming there are infinitely many steps in which a letter is sent to <math>c</math> then there are infinitely many steps in which a letter is read from <math>c</math>. {{r|Undecidable over unreliable channels|p=88}}
Line 89 ⟶ 92:
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 <math>(q,w_1,\dots,w_i\cdot a\cdot w'_i\dots,,w_m)\rightsquigarrow(q,w_1,\dots,w_i\cdot a\cdot a\cdot w'_i,w'_m)</math>.{{r|easier|p=26}}
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
== Properties ==
The set of
== Problems and their complexity ==
Line 110 ⟶ 113:
=== Model checking problem ===
The '''model checking problem''' consists in deciding whether given a system <math>S</math> and a [[CTL*]]*-formula or a [[Linear temporal logic|LTL]]-formula <math>\phi</math> or a whether the language defined by <math>S</math> satisfies <math>\phi</math>. This problem is undecidable over lossy channel system.{{r|easier|p=23}}<ref name="Undecidable over unreliable channels">{{cite journal |last1=Abdulla |first1=Parosh Aziz|last2=Jonsson|first2=Bengt |title=Undecidable Verification Problems for Programs with Unreliable Channels|journal = Information and Computation |date= 10 October 1996 |volume=130 |issue=1 |pages=
=== Recurrent state problem ===
The '''recurrent state problem''' consists in deciding, given a channel system <math>S</math> and an initial configuration <math>\gamma</math> and a state <math>s</math> whether there exists a run of <math>S</math>, starting at <math>\gamma</math>, going infinitely often through state <math>s</math>. This problem is undecidable over lossy channel system, even with a single channel.{{r|easier|p=23}}{{r|Undecidable over unreliable channels|p=80}}
=== Equivalent finite
Given a system <math>S</math>, there is no algorithm which computes a [[finite
=== Boundedness problem ===
Line 128 ⟶ 131:
=== Structural termination ===
The '''structural
==Communicating Hierarchical State Machine==
Hierarchical state machines are finite
However, it was proved that the coexistence of hierarchy and concurrency intrinsically costs language inclusion, language equivalence, and all of universality.<ref>Alur, Rajeev; Kannan, Sampath; Yannakakis, Mihalis. "Communicating hierarchical state machines," Automata, Languages and Programming. Prague: ICALP, 1999</ref>
== References ==
<references />
| |||