-- ________________________________________________________________________ Hartmut Wittke OFFIS e.V Division Embedded Systems Escherweg 2 - D-26121 Oldenburg - Germany Fon : +49 441 798 2164 E-mail: hartmut.wittke@offis.de - URL: hhtp://www.offis.de
attached mail follows:
Hi Fabio,
> > ha> 2) What kind of verification ,your software supports? > > CTL model checking. More details can be found in the on-line > documentation (http://vlsi.colorado.edu/~vis/whatis.html). > > The next release of VIS will also support LTL model checking. > > Fabio
In your answer to the mail of Hadi Afshar you wrote the next version of VIS will also support LTL model checking. This sounds very interesting to us. How will this be realized? Are you planning to re-use the language emptyness check for this feature with an externally generated buechi-automaton or will VIS directly accept LTL formulas as input? Have you thought about mixing LTL for assumptions with CTL for commitments?
If there are concrete plannings, when will this version of VIS be available?
If you use Buechi automata in either way, what will be the basis for the tableau construction? The ordinary way or/and the generation you suggested in the CAV 2000 paper?
Regards Hartmut
-- ________________________________________________________________________ Hartmut Wittke OFFIS e.V Division Embedded Systems Escherweg 2 - D-26121 Oldenburg - Germany Fon : +49 441 798 2164 E-mail: hartmut.wittke@offis.de - URL: hhtp://www.offis.de
This archive was generated by hypermail 2b30 : Tue May 28 2002 - 09:55:03 MDT