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

Hi Johan,
------------------------------------------------------------------------

 w|= (P1 until P2) 
<=> 
 either there exists 0 <= j < |w| so that w^{j..} |= P2 
                         and for every 0 <= i < j; w^{i..} |= P1, 
 or for every 0 <= i < |w|; w^{i..} |= P1.

I think this is a little cumbersome. Maybe we should consider making the
strong variants s_next and s_until primitive and define the rest in
terms of these.


 s_next[0] p == p (s_next[0] is needed for the definition of
eventually[0:x])
 s_next[n] p == s_next (s_next[n-1] p) [n>0]
 
 and
 next[n] p == not s_next[n] not p [n>0]
 
 s_eventually[m:m] p == s_next[m] p [m>=0]
 s_eventually[m:n] p == s_eventually[m:n-1] p or s_next[n] p [0<=m<n]
 s_always[m:m] p == s_next[m] p [m>=0]
 s_always[m:n] p == s_always[m:n-1] p and next[n] p [0<=m<n]
 eventually[m:n] p = not s_always[m:n] not p [0<=m<n]
 always[m:n] p = not s_eventually[m:n] not p [0<=m<n]
 
In that case we could define

 w|= (P1 s_until P2) 
<=> 
 there exists 0 <= j < |w| so that w^{j..} |= P2 
                         and for every 0 <= i < j; w^{i..} |= P1, 
------------------------------------------------------------------------

[DB] The reason that I use the weak forms for until and next is the
ability to place them in recursive properties. There strong operators
are not allowed neither the not operator. 

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