Subject: Re: sugar: case-by-case analysis of accellera requirements
From: Moshe Vardi (vardi@cs.rice.edu)
Date: Tue Nov 20 2001 - 08:34:42 PST
> >attributing to [1] the claim of "no change in semantics for
> >the vast majority of properties used in practice" is a misattribution.
> >Maidl says nothing of that sort. All she does is characterize the
> >properties that are in the intersection of LTL and ACTL.
>
> as i am sure is clear to anyone who has been following this discussion, i
> never claimed that [1] discusses anything other than ltl and ctl.
Which means that it says nothing about the relationship between OldSugar
and NewSugar.
>
> >Suerly, however, you are not syaing that there is no practical
> >impact for implementors of the language.
>
> indeed there is an impact for the implementors. both ltl and ctl model
> checkers will have to implement a check whether or not a formula coded with
> the other formalism is in the common fragment. if so, then the formula can
> be checked in "native mode", by ignoring quantifiers or the lack of them,
> respectively. if it turns out that the formula is not in the common
> fragment, then the ltl model checker can give an error that it does not
> support the optional branching extension. the ctl model checker can use
> tableau construction, without the need to change its core algorithms.
1. We do not know how to decide if the path quantifiers of a NewSugar
formula can be deleted. Maidl's work applies only to LTL and ACTL.
2. Your earlier description of the model checking algorithm for NewSugar
said nothing about a tableau construction.
Moshe
This archive was generated by hypermail 2b28 : Tue Nov 20 2001 - 08:51:16 PST