Subject: Re: efficiency claims
From: Moshe Vardi (vardi@cs.rice.edu)
Date: Tue Nov 20 2001 - 08:28:05 PST
This is like saying that the same algorithm works for both CTL and CTL*.
As you may recall, model checking OldSugar was doubly exponential in the
worst case. As far as I can see, model checking NewSugar is triply
exponential in the worst case.
Moshe
> moshe,
>
> the whole point is that the same solution works for both.
>
> cindy.
>
>
> To: Cindy Eisner/Haifa/IBM@IBMIL, havlicek@adttx.sps.mot.com
> Subject: Re: efficiency claims
>
>
>
> Cindy, did you describe the algorithm for Sugar or for Sugar FL?
>
> Moshe
>
>
>
This archive was generated by hypermail 2b28 : Tue Nov 20 2001 - 08:46:07 PST