Re: [sv-ac] informal definition of the weak operator

Hi Doron,

I like this kind of thing. Me, John, Dana Fisman and Cindy Eisner wrote
a paper (unpublished and called "Truncating Regular Expressions") back
in 2004 on what I think is a similar thing which we called the
weak/strong word semantics.  The purpose was to solve the embarrassing
problem of structural contradictions in weakly embedded sequences and
abort.

For example

if sc is the sequence (1 intersect (1[*2])) then

*) weak(1[*0:$] ##1 sc) 

will not be satisfiable according to the current semantics. The problem
is that sc will not match tightly on any word not even if all the
letters are of the type \top.

I think there is a sound intuition about weak embedding saying that *
should be true on every trace regardless of what sc is, because we
should not even have to consider what sc is because the 1[*0:$] prefix
will never get contradicted.

also for similar reasons

accept_on(b) weak(1[*0:$] ##1 sc) 

will not be satisfiable according to the current semantics.

The weak/strong word semantics defines partial match of sequences and
properties on finite weak and strong words (defined in the paper) in a
way that disregards the parts of the formulas that are not matched.

One problem with the current \top, \bot semantics is that although it
solves similar problems when sc is a boolean contradiction by allowing
satisfaction of a boolean contradiction on a letter it doesn't do the
same thing for structural contradictions. The root problem as I see it
is that the \top,\bot semantics retains the requirement of tight match
of the entire sequence, albeit on a word containing letters that will
accept any boolean.

Best Regards,

Johan


On Thu, Dec 06, 2007 at 09:36:41AM +0200, Bustan, Doron wrote:
> Hi,
> 
>  
> 
> I just remembered that in 921 we have a definition of a weak match. This
> 
> 
> definition is formal and does match the current definition for sequences
> with  intersect (and its derived operators 
> 
> "and", "within", "throughout".) For infinite words we need to say that
> it shall match every prefix. So, there are 
> 
> several reasons not to add it to 1932. Nevertheless, it adds intuition
> to a confusing definition, and thus maybe it worth it.
> 
> (In my opinion this is a better definition then the current one.)
> 
> The definition is inductive: ||= is the new defined relation, |== is
> tight satisfaction.
> 
>  
> 
> *      w,L0||= b iff either |w|=0 or |w|=1 and w |= b
> 
> *      w,L0||= (1,v=e) iff either |w|<=1 
> 
> *      w.L0||= R[*0] iff |w| = 0 
> 
> *      w.L0||= ( R ) iff w,L0 ||= R 
> 
> *      w.L0||= R1 or R2 iff w,L0 ||= R1 or w,L0 ||= R2
> 
> *      w.L0||= R1 intersect R2 iff w,L0 ||= R1 and w,L0 ||= R2
> 
> *      w.L0||= R1 ##1 R2 iff either w,L0 ||= R1 or for some xy=w and L1,
> x,L0,L1|== R1 and ,y,L1 ||= R2
> 
> *      w.L0||= R1 ##0 R2 iff either for some y, |y|>0 wy,L0 ||= R1 or
> for some xyz=w and L1, |y| = 1,  xy,L0,L1|== R1 and ,yz,L1 ||= R2
> 
> *      w.L0||= first_match(R1) iff w.L0||= R1 and for every xy=w and L1,
> if |y|> 0 then x,L0,L1 |/== R1 
> 
> *      w.L0||= R1[*1:$] iff for some xy=w and L1, x,L0,L1 |== R1[*0:$],
> and y,L1||= R1
> 
>  
> 
> Do you think it worth adding this definition somehow to the discussion?
> 
>  
> 
> 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.
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Kvarnbergsgatan 2                Fax: +46 31 7451914
411 05 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

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