Channel system (computer science): Difference between revisions

Revision as of 14:04, 4 April 2019

Latest revision as of 02:46, 26 December 2024

(15 intermediate revisions by 10 users not shown)

Line 1:

{{redirect|Channel system|Earth's sea floor|Abyssal channel}}

{{short description|Finite-state machine with fifo buffers for memory}}

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.

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.

== 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 (A\cup\{\epsilon\}) \times Q</math> a finite set of transition rules with <math>\Sigma^*</math> being the set of finite (potentially empty) words over the alphabet <math>\Sigma</math>.<ref name="decidable">{{cite journal |last1=Abdulla |first1=Parosh Aziz |last2=Jonsson|first2=Bengt|title=Verifying Programs with Unreliable Channels|journal =Information and Computation |year=1996 |volume=127 |issue=2 |pages=91–101 |doi=10.1006/inco.1996.0053|doi-access=free }}</ref>

Depending ofon the author, a '''channel system''' may have no initial state and may have an empty alphabet.<ref name="Nonprimitive recursive">{{cite journal |last1=Schnoebelen |first1=Ph |title=Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity |journal =Information Processing Letters |date=15 September 2002 |volume=83 |issue=5 |pages=251–261 |doi=10.1016/S0020-0190(01)00337-4}}</ref>

=== Configuration ===

Line 22 ⟶ 24:

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 writing an <math>u</math> to the end of the channel <math>c_i</math>. Similarly <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 removing a <math>u</math> starting the word <math>c_i</math>.

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. GivenSimilarly, given a transition <math>(q,c_i,!?,u,q')</math>, if <math>w_i=uw'_i</math>, there is a perfect step <math>(q,w_1,\dots,w_{i-1},uw_i,w_{i+1},w_m)\xrightarrow{a}_{\mathtt{perf}}(q',w_1,\dots,w_{i-1}, w_i', w_{i+1},\dots,w_m)</math> where the first letter of the <math>i</math>-th word is <math>u</math> and has been removed during the step.

=== Run ===

Line 37 ⟶ 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=20–31 |doi=10.1006/inco.1996.0003|doi-access=free }}</ref>{{rp|22}} This is due to the fact that such a machine may simulates the run of a [[Turing machine]]. This simulation is now sketched.

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, and aimmediately steprewritten isin simulatedthe whilechannel, itwith one exception, the part of the content representing the head of the Turing machine is readchanged, to simulate a step of the Turing machine computation.

== Variants ==

Line 48 ⟶ 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=1-31–3|date = 17 March 2008 |pages=337–354|journal=Theoretical Computer Science|doi-access=free}}</ref>{{rp|337}}

=== 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 lossinnesslossiness 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, <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 aA 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 ====

Line 93 ⟶ 95:

== Properties ==

The set of rechablereachable configurations is recognizable for lossy channel machines{{r|easier|p=23}} and machines capable of insertions of errors{{r|easier|p=26}}. It is recursively enumerable for machine capable of duplication error{{r|easier|p=27}}.

== Problems and their complexity ==

Line 111 ⟶ 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=71–90 |doi=10.1006/inco.1996.0083|doi-access=free }}</ref>

=== 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 -state machine ===

Given a system <math>S</math>, there is no algorithm which computes a [[finite -state machine]] representing <math>R(S)</math> for the class of lossy channel system.{{r|easier|p=24}} This problem is decidable over machine capable of insertion of error .{{r|easier|p=26}}

=== Boundedness problem ===

Line 129 ⟶ 131:

=== Structural termination ===

The '''structural termiantiontermination''' problem consists in deciding, given a channel system <math>S</math> if the termination problem holds for <math>S</math> for every initial configuration. This problem is undecidable even over counter machine.{{r|Counter|p=342}}

==Communicating Hierarchical State Machine==

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.<ref>Alur, Rajeev; Kannan, Sampath; Yannakakis, Mihalis. "Communicating hierarchical state machines," Automata, Languages and Programming. Prague: ICALP, 1999</ref>