Re: [sv-ac] 1932 Questions on non vacuity.

Hi Doron,


On Thu, Oct 25, 2007 at 02:06:28PM +0200, Bustan, Doron wrote:
> >> 
> >> 4. The judgment whether there is a witness for non vacuity for a
> property >in 
> >>    a model is made per attempt. In other words from every property
> there 
> >>    going to be at most one extracted cover property. I think this
> create >the 
> >>    problem with your example because what we need are two cover
> >properties 
> >>    "a ##1 b" and "c ##1 d" but these properties may be hit on
> different 
> >>    attempts in different simulation runs. 
> >
> >The rewrite I suggested will give you the formula 'a #-# b or c #-# d'
> >for the original formula 'a|->b or c|->d'
> >
> > N(a|->b or c|->d) 
> >=
> > N(a|->b) or N(c|->d) 
> >=
> > a #-# N(b) or c #-# N(d) 
> >=
> > a #-# b or c #-# d 
> >
> >The trace w in the example will then come out as vacuous since although
> >w|= a|->b or c|->d, it is the case that w|/= a #-# b or c #-# d.
> 
> [DB] I have not study your proposal yet, but I have 2 comments.
> 
> The first is N(weak(r)) = strong(r), consider the property 
> "weak(a[*1:$] ##1 0)" which is equivalent to "always a". Making the
> Sequence strong makes the property a contradiction.

I think it is hard to get a definition that will give the same result
for all equivalent formulas. Consider for example the pair 'a|->b' and
'!b|->!a'. I guess, a|->b should be non vacuous for a trace where a and
b are always true, but what about the second one?


> 
> The second is that you need to add a definition for #=# and s_until_with
> (the dual of until). Since you push "not" to the leaves you cannot use
> the derived forms. For #-# the solution looks obvious "N(r #-# p) = r
> #-# N(p)" but what about the strong until?
> 

Actually the transformation that I use is defined for strong operators
too:

N(a) = a
N(not P) = not N(p)
N(weak(r)) = strong(r)
N(strong(r)) = weak(r)
N(P1 or P2) = N(P1) or N(P2)
N(P1 and P2) = N(P1) and N(P2)
N(X P) = X! N(P)
N(X! P) = X N(P)
N(P1 until P2) = (not P2) s_until_with N(P1)
N(P1 s_until P2) = N(P2) until_with (not P1)
N(r |-> P) = r #-# N(P)
N(r |=> P) = r #=# N(P)


If P is safety then N(P) is co-safety so if true, N(P) has a finite
witness trace w (i.e. w is such that w|=+ N(P)).

It gives pretty intuitive results for many safety properties. For non
safety the results are often weird though.

Best Regards,

Johan

> 
> >> 
> >> 5. Another principle that we didn't fully achieve is that checking
> for  
> >>    vacuity should be "for free" as a by product of checking the
> >assertion.
> >> 
> >> 
> >> There are much more intuitive definitions in the literature. However,
> I >think that all of them conflict with principles 4 and 5. We should
> consider >what we want but I suspect we will not change the basic
> concept for the >2008 release.
> >> 
> >> I would go for something close to definition of
> >> 
> >> R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A.
> Tiemeyer, >and M. Vardi. 
> >> Enhanced vacuity detection in linear temporal logic. 
> >> In Computer Aided Verfication, 15th Inte.l Conf., (CAV 2003), volume
> 2725 >of LNCS, pages 368-380, 2003.
> >
> >In the article the problem of determining which subformulas of a
> formula
> >F true of a model M are non-affecting in that formula w.r.t. M. How is
> this
> >related to the problem at hand?
> >
> >We are trying to define a relation of non-vacuity between traces and
> >formulas. How exactly is this problem related to the problem of
> >subformula vacuity w.r.t. to models discussed in the article?
> >
> >I can see some connections but I am not sure about the details. For
> >example even in a situation where the formula F has non-affecting
> >subformulas w.r.t. the model M we may want to compute a non vacuous
> >trace for F, and in fact the current definition does. Consider the
> >formula 'p|->p'.  The subformula p is not affecting for any M.
> >Nevertheless if w^0|-p then w|=non p|->p.
> >
> 
> The idea is that for every sub property p' of p create a cover property
> that witnesses that p' influences p. This is not compliant with the
> non-vacuous relation but for every property that never pass
> non-vacuously according to the current definition we will have a cover
> property that is not covered. 
> Such cover properties have a potential to flush many more problems, and
> your example of r->r is one of them. I would like to know that one of my
> sub properties is a tautology, because it probably not my intent (unless
> I wrote "1"). 
> 
> Doron
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.