Content deleted Content added
m Open access bot: doi added to citation with #oabot. |
m Open access bot: doi added to citation with #oabot. |
||
Line 11:
* <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 \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 of 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>
| |||