>>>>> "HW" == Hartmut Wittke <Hartmut.Wittke@Informatik.Uni-Oldenburg.DE> writes:
HW> Hi Fabio,
HW> In your answer to the mail of Hadi Afshar you wrote the next
HW> version of VIS will also support LTL model checking. This sounds
HW> very interesting to us. How will this be realized? Are you
HW> planning to re-use the language emptyness check for this feature
HW> with an externally generated buechi-automaton or will VIS
HW> directly accept LTL formulas as input?
VIS 2.0 reads LTL formulae directly, translates them internally into
Buechi automata, and then uses a slightly modified version of the
language emptiness check already in VIS 1.4 to verify the property.
VIS 2.0 will also have bounded model checking for a subset of LTL
(safety properties). For that, VIS interfaces to zchaff.
HW> Have you thought about mixing LTL for assumptions with CTL for
HW> commitments?
The new LTL parser is in effect a CTL* parser, but CTL* model checking
is not part of VIS 2.0. With CTL* you'll be able to do what you
describe, if my understanding is correct.
HW> If there are concrete plannings, when will this version of VIS be
HW> available?
We are in the testing phase. Release is expected in a few weeks.
HW> If you use Buechi automata in either way, what will be the basis
HW> for the tableau construction? The ordinary way or/and the
HW> generation you suggested in the CAV 2000 paper?
Right now (i.e., for 2.0), the algorithm is a simplified version of
the one in the CAV 2000 paper.
Fabio
This archive was generated by hypermail 2b30 : Tue May 28 2002 - 10:42:01 MDT