Content deleted Content added
→Channel system: It is mentioned that the alphabet can be empty, depending on the author. Here let's define $\epsilon$ is always in $A$, so that the notation is simpler |
m Disambiguating links to LTL (link changed to Linear temporal logic) using DisamAssist. |
||
Line 112:
=== 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}}</ref>
=== Recurrent state problem ===
| |||