From: Ian Harris (harris_at_igor.ics.uci.edu)
Date: Mon Apr 25 2005 - 14:45:34 MDT
I believe that LTL is a subset of ACTL*. I'm looking at the book Model
Checking by E. Clarke, O. Grumberg, and D. A. Peled. In Ch 3 page 30 I
see the following statement, "Linear Temporal Logic (LTL), on the other
hand will consist of formulas that have the form A f where f is a path
formula in which the only state subformulas permitted are atomic
prepositions". The precise definition of LTL is given in the next few
lines. Then in Ch. 3 page 31 I see the following statement, "The
restriction of CTL to universal path quantifiers is called ACTL*". Since
all LTL formulas are of the for A f and f has no path quantifiers, it
sounds like LTL is a subset of ACTL*.
- Ian Harris
On Tue, 26 Apr 2005, Roopak Sinha wrote:
> We are planning to do some experiments with NuSMV, but need the answer to this
> very basic question. Could someone help us?
>
> Regards
> Roopak
>
This archive was generated by hypermail 2.1.7 : Mon Apr 25 2005 - 14:49:29 MDT