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
------------------------------------------------------------