>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> Can you please tell by an example,in which cases
vg> CTL model checking fails and we go for Language Containment.
Language containment is a notion connected with the verification of
linear-time properties. A linear-time property defines a set of
admissible linear traces. When the propery is given, for instance, in
the form of an LTL formula or a Buechi automaton, the traces form a
so-called omega-regular language.
The system to be verified also produces a set of traces, which form
the language of the system. If the language of the system is
contained in the language of the property, then the system's traces
are all admissible, and the property holds.
If the property we want to prove is not expressible in CTL, but is
expressible, say, in LTL, then we can resort to language containment.
(A classical LTL property that cannot be expressed in CTL is FGp.)
Notice that VIS has a command for language emptiness, rather than one
for language containment. The idea is that we check the language of
the system against the language for the negation of the property.
This is doen by composing a Buechi automaton for the negation of the
property with the system. If the language is empty, the system and
the automaton have no traces in common, which means that no system's
traces satisfy the negation of the property. Hence the property
itself holds.
Fabio
This archive was generated by hypermail 2b30 : Mon Aug 27 2001 - 14:36:43 MDT