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

Hi Doron,

the thing you mention was just one suggestion in that discussion. To me
it seemed very hard to get it working. The definition I am talking about is
an alternative definition of weak and strong satisfaction on finite words
of formulas containing embedded regular expression. This definition
doesn't make use of any special letters like \top and \bot, and it gives
intuitively correct results even for formulas containing structural
contradictions. Me and Koen Claessen defined a semantics on those lines
for the weak fragment of PSL and showed it to be equivalent to an
operational semantics. We presented this at FMCAD 2004.

The semantics you cite below seems to have much in common with the
semantics I am talking about now. It seems to be a definition of tight
matching on truncated words, i.e. the word isn't required to match all
of the sequence to the right. This is an effect of you clause


 *      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

This was something we considered on the way to the formulation we
converged on at that time.


Best Regards,

Johan



On Thu, Dec 06, 2007 at 01:56:29PM +0200, Bustan, Doron wrote:
> Hi Johan,
> 
> I remember talking with John about the things that you mentioned on 2005...
> There were some e-mail exchange with Cindi and Dana, and I remember some
> new definition where \top satisfies every sequence. Maybe we can do something about that in the 2010 release. 
> 
> Doron
> 
> >>-----Original Message-----
> >>From: Johan M?rtensson [mailto:johan.martensson@jasper-da.com]
> >>Sent: Thursday, December 06, 2007 1:04 PM
> >>To: Bustan, Doron
> >>Cc: sv-ac@eda.org
> >>Subject: 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
> >>------------------------------------------------------------
> ---------------------------------------------------------------------
> 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 
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.