RE: [sv-ac] 1932 LTL_Formal.0701009.pdf partial review.

Hi Johan, 

I fixed most of your comments, but there are some, which need further
discussion. See my notes below

> 
> MAYBE REPLACE
> (p s_until_with q) == (p s_until (p and q))
> WITH
> (p s_until_with q) == not (not q until not p)
> 
> With the last two replacements the duality of the different until
operators
> becomes more visible.

[DB:] I agree that it makes the duality more visible, but I think that
it makes the semantics very difficult to understand. I think that I will
add some equivalences in a dedicated section in clause 16.


> 
> 
> F.2.3.2.8 
> 
> It seems unnecessarily convoluted to me to define  next[m] in terms of
> s_next[m] which then is defined in terms of s_next which is defined in
terms of
> next.
> 
> Why not instead define the weak wariant of the ranged operators in
terms of the
> weak primitive operator, and then define the strong ranged operators
in terms
> of the weak ranged operators:
> 
[DB:] done

> next[0] p == p (next[0] is needed for the definition of
eventually[0:x])
> next[n] p == next (next[n-1] p) [n>0]
> 
> and
> s_next[n] p == not next[n] not p [n>0]

[DB:] The reason next[m] starts from 1, is that we want to reserve
next[0] as synchronizing operator for multi clock properties. I just saw
a presentation by Dana Fisman on a similar operator in PSL. I am waiting
for the proceeding of the conference HVC07, that should be published at
November 19, to see what she has done.

Regards

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.