Re: Issue 20. Important weak satisfaction.

Hi Cindy,

perhaps I have a slight hairsplitting tendency but apart from that my
work on this issue has been motivatied entirely by implementation
concerns. We more or less use the formal semantics directly in our
implementation: We use rules derived from the operational semantics in
our basic algorithm for generating FSMs from properties. We also
rely heavily on being able to normalize PSL properties and for this we
need a denotational semantics for checking the correctness of rewriting
rules.

We soon realized that we would implement an operational approximation of
the official semantics not the official thing. In this situation we were
not satisfied with stating that our tool approximates the PSL semantics.
We also wanted to have a clear description of the differences with the
official one or perhaps a clear definition of the subset of PSL on which
we would be in agreement with the official semantics. We also needed a
denotational semantics equivalent with the operational one in order to
justify our normalization rules.

I think the situation where you implement a consistent semantics that is
slightly different from the official one but where you can specify
exactly the area of agreement is much more robust and acceptable than
the situation where you have to concede that there are more or less
unspecified semantic "bugs".

It also turns out that the area of agreement is more restricted than
just the structural-contradiction free language. We must also exclude
"potential" structural contradictions like for example
{a;a;a}&&{{b;b}||{c;c;c}}. This expression is no structural
contradiction as we defined it but it will be weakly satisfiable in the
operational/weak word sense without being it in the \top^k sense.

<(a,b),(a,b)>^-|=ws {a;a;a}&&{{b;b}||{c;c;c}}
  because
 <(a,b),(a,b)>^-|=ws {a;a;a}
 and
 <(a,b),(a,b)>^-|=ws {b;b}

but there is no k s.t.

<(a,b),(a,b)>\top^k|==psl {a;a;a}&&{{b;b}||{c;c;c}}

so

<(a,b),(a,b)>\top^\omega|/=psl {a;a;a}&&{{b;b}||{c;c;c}}

I only realized this after I had worked with the weak/strong words
semantics which indicates to me that this kind of semantic work is
necessary for even knowing what the corner cases are on which you will
not be in compliance.

It is true that there is a problem in our truncating regular expressions
paper, but I think we can simply sidestep that problem if we are to
define a new PSL semantics. That problem was with the finite neutral
case of the truncated semantics. The thing to realize is that we do not
need a neutral truncated semantics. What we need is a finite/infinite
neutral semantics using a weak/strong truncated semantics. We need to
keep the neutral finite/infinite case separated from the finite
weak/strong case. If we do this all will work out fine and the neutral
finite semantics will be in accordance with the traditional LTL one as
far as I can see, and I have already argued this in some detail with John.

Moreover: It is true that the operational semantics paper just covers
the weak part of PSL and a simplified variant at that, but I refer in
the paper to a tech report that I wrote that defines a weak/strong words
semantics for all of PSL and shows equivalence on the fragment that
doesn't contain potential structural contradictions.

Best Regards,

Johan M

On Tue, Nov 30, 2004 at 03:15:40PM +0200, Cindy Eisner wrote:
>
>
>
>
> johan,
>
> i agree that this issue is an important and interesting theoretical one. i
> don't agree that it is more than minor from a practical point of view. for
> a user, this is a true corner case. for an implementor, getting it right
> as currently defined will take lots of work, whereas getting it wrong will
> be easy. but since it is a corner case, getting it wrong amounts to no
> more than a minor known bug. if we all guaranteed our tools were bug free,
> this would be a catastrophe. as it is, i do not see it as a big deal for a
> tool developer.
>
> regarding a solution: if there was a good known solution, i'd be all for
> using it. but, the solution that appears in our unpublished paper has a
> major weakness that is discussed in that paper. and the solution in your
> fmcad paper does not cover all of psl (i have not examined it carefully
> enough to know whether or not it contains the same weakness as our
> unpublished paper). in addition, i would be hesitant to commit to a
> certain time frame for finding that solution, since as we discovered when
> writing our unpublished paper the theoretical issue is a very tricky one.
>
> in summary: i think we all agree that the issue should be fixed. and i
> don't see the point of arguing the priority when we don't have a complete
> solution yet.
>
> regards,
>
> cindy.
>
> --------------------------------------------------------------------
> Cindy Eisner
> Formal Methods Group
> IBM Haifa Research Laboratory
> Haifa 31905, Israel
> Tel: +972-4-8296-266
> Fax: +972-4-8296-114
> e-mail: eisner@il.ibm.com
>
> Johan Mårtensson <johan.martensson@safelogic.se>@eda.org on 29/11/2004
> 12:17:55
>
> Sent by: owner-ieee-1850-extensions@eda.org
>
>
> To: ieee-1850-issues@eda.org, ieee-1850-extensions@eda.org
> cc:
> Subject: Issue 20. Important weak satisfaction.
>
>
>
> Hi Erich, and Extensions/Issues Committee,
>
> The more I think of it the more objectionable do I find the way issue 20
> is defined:
>
> > 20. (E:3) The semantics of ({{a} && {a;b}{ abort b).
> >
> > This is a minor issue (extreme corner case) in the formal semantic
> > definition of both PSL and SVA and needs to be resolved in parallel in
> > both languages.
>
> First of all, the (supposedly low) importance of this issue is stated in
> the description of the issue, which arguably is a little biased.
> Secondly I don't think it is a minor issue at all; It goes to the core
> of the question of implementability (and intuitive accuracy) of the
> formal semantics. Thirdly it is not just about the semantics of abort in
> combination with structural contradictions. It is about how to formulate
> weak satisfaction (used in abort and in weak embedding of seres) in a
> denotational semantics.
>
> Weak satisfaction on a finite run is meant to capture the intuitive
> operational concept of "so far true" or (which is the same) "not yet
> contradicted". For example, if an abort occurs at a point where the the
> aborted formula is "so far true" then then the formula should be
> accepted. Another example: Intuitively the weak embedding of the sere r
> {r} is true on a run w if r matches a prefix of w or if r is "so far
> true" or "not contradicted" on any prefix of r.
>
> Intuitively when checking whether a formula is "so far true" one should
> only have to inspect the finite number of states that have been visited.
> This is very important!
>
> When trying to encode this intuition into a denotational semantics there
> are choices to be made. In the PSL semantics (1.0, 1.1) this was done
> using a trick from modal logic: Weak satisfaction on a finite run is
> defined there in terms of satisfaction on a set of "reachable" runs,
> namely the set of extensions of the finite run in question. The
> difference between 1.0 and 1.1 is only in that in 1.1 special top states
> that satisfy any boolean are allowed in these extensions. It might be
> thought that "so far true" and "not yet contradicted" on a finite run is
> the same as satisfiability on a possible extension of this run, but it
> is clearly not!
>
> Intuitively the following weak embedding { [*];r } should be true on any
> run whatever r is, because [*];r will never be contradicted. This is
> because the [*] prefix can be extended indefinitely without being
> contradicted. Let's now look at how this is treated in the different
> relevant PSL semantics.
>
> (let FALSE be a boolean contradiction and b a satisfiable
> boolean)
>
> PSL 1.01
> --------
> let w be any w
>
> w|= {[*];b}
>
> not w|= {[*];FALSE}
>
> So {[*];b} is true on any w even if b happens to be false on every state
> in w. On the other hand {[*];FALSE} is false on any w although
> intuitively [*];FALSE is never contradicted. The reason is that every
> finite prefix of w can be extended to one that tightly matches {[*];b}
> since b is satisfiable, but no prefix of w can be extended to one that
> matches {[*];FALSE}.
>
> ({r} is not valid PSL 1.0 syntax on the top level. To express weak
> embedding of a sere r in PSL 1.0 one can write e.g. {[*1]}|-> {r} so
> above {r} can be regarded as an abbreviation of this suffix
> implication.)
>
>
> PSL 1.1
> --------
> let w be any w and sc = {b && {b;b}}
>
> w|= {[*];FALSE}
>
> not w|= {[*];sc}
>
> So {[*];FALSE} is true on any w. On the other hand {[*];sc} is false on
> any w although intuitively [*];sc is never contradicted. The reason is
> that every finite prefix of w can be extended to one that tightly
> matches {[*];FALSE} since FALSE is now satisfiable (on the state top),
> but no prefix of w can be extended to one that matches {[*];sc}, because
> no sequence of states even allowing top states will satisfy sc.
>
> The top states were introduced in order that (expensive and intuitively
> irrelevant) boolean satisfiabiliy analysis should not be required to
> evaluate formulas like {[*1]}|-> {[*];b} and ({[*1]}|-> {[*];b}! abort
> c). The problem was only that the remedy was not radical enough it
> seems; Now structural satisfiability analysis must be performed instead.
>
> Last winter me, John H, Cindy and Dana worked together to define
> a denotational semantics for truncated runs that would address this
> problem. It resulted in an article "Truncating Regular Expressions"
> which sadly is not yet published. This article defines a denotational
> semantics for LTL with embedded regular expressions and abort in which
> weak satisfaction on finite runs is not defined in terms of possible
> extensions of this run but purely in terms of the states in the run in
> question. A semantics of this kind for PSL would solve the present
> problems it seems.
>
> At FMCAD a couple of weeks ago me and Koen Claessen presented an article
> with an operational semantics for (somewhat simplified) PSL. This
> operational semantics is meant to capture the (operational) semantic
> intuitions behind PSL. It can also be used for implementation. In this
> article we also present a denotational semantics in line with the one
> from the "Truncating Regular Expressions" article and show that the
> operational and denotational ones are equivalent.
>
> I think we should consider giving an operational semantics for PSL in
> line with what we do in the article and also (or at least) consider
> adapting the definition of weak satisfaction so that it expresses the
> operational intuitions of weak satisfaction.
>
> Best Regards, Johan Mårtensson.
>
> PS. I attach the FMCAD article.
>
>
> On Sun, Nov 28, 2004 at 08:26:58PM -0800, Erich Marschner wrote:
> >
> > IEEE 1850 PSL WG participants,
> >
> > The Issues List has now been updated. You can view the updated list of
> issues by going to the IEEE 1850 PSL web page, at
> http://www.eda.org/ieee-1850, and clicking on the "Issue List" link on the
> right-hand side panel, or you can go directly to
> http://www.eda.org/ieee-1850/Issues/Issues.html.
> >
> > The updated list has several indices at the beginning:
> > - Issues Index: a list of all issue numbers (which link to the issue
> descriptions below)
> > - Issue Disposition: lists for each of LRM, Extensions, Rejected, Out of
> Scope, and Not Yet Dispositioned
> > - Issue Groups: lists for each of the groups of related issues defined
> so far
> >
> > The issue group identifiers (e.g, Group A) also link to a page
> summarizing the discussion of issues in this group and resolutions that
> have come out of the discussion. The same pages will be updated with LRM
> changes that are proposed to implement the resolutions.
> >
> > Please review the Issues List and let me know if you see any information
> that is incorrect, or if you think there is any information missing.
> >
> > Regards,
> >
> > Erich
> >
> >
>
> --
> ------------------------------------------------------------
> Johan Martensson, PhD Office: +46 31 7451913
> R&D Mobile: +46 703749681
> Safelogic AB Fax: +46 31 7451939
> Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> SE-411 33 Gothenburg, SWEDEN
> PGP key ID A8857A60
> www.safelogic.se
> ------------------------------------------------------------
>
>
>

-- 
------------------------------------------------------------
Johan Martensson, PhD            Office: +46 31 7451913    	
R&D                              Mobile: +46 703749681
Safelogic AB                     Fax: +46 31 7451939
Arvid Hedvalls Backe 4           johan.martensson@safelogic.se
SE-411 33 Gothenburg, SWEDEN 
PGP key ID A8857A60
www.safelogic.se
------------------------------------------------------------