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

Hi


Some more comments on LTL_Formal.0701009.pdf


F.3.1.1 Rewrite rules for sequences 

 REPLACE
 The transformation T^s(S,c) recursively defined below produces an
 unclocked sequence R equivalent to a given clocked sequence S with a
 leading clock c:
 
 WITH
 The transformation T^s recursively defined below produces an
 unclocked sequence R=T^s(S) equivalent to a given clocked sequence S:

 Let T^s(S) be short for T^s(S,1)
 
It seems to me that if S is a clocked sequence it already contains
its leading clock. It is true that in that case T^s(S,c) = T^s(S,1). But
if we specify the rewritten sequence as T^s(S,c) it seems we need to
have access to the leading clock to start the rewrite.

F.3.1.2 Rewrite rules for properties 

 REPLACE
 The transformation T^p(P,c) recursively defined below produces an
 unclocked property P equivalent to a given clocked property Q with a
 leading clock c:
 WITH
 The transformation T^p recursively defined below produces an
 unclocked sequence P=T^p(Q,1) equivalent to a given clocked property Q:
 
 Let T^p(Q) be short for T^p(Q,1)

F.3.3
 w|=Q <=> w|=T^p(Q)

I don't think T^p as a unary operation is defined. Either define T^p(Q)
as T^p(Q,1) or write:


 w|=Q <=> w|=T^p(Q,1)

------------------------------------------------------------------------

 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, 

Best Regards,

Johan M

On Tue, Oct 23, 2007 at 02:54:47PM +0200, Johan Mårtensson wrote:
> Hi,
> 
> 
> The following are some comments on F.2 of LTL_Formal.0701009.pdf
> 
> 
> 
> F.2.1
> p.1
> In the comments to the abstract grammar:
> 
> "s_next" form  ==> "next" form 
> "s_until" form  ==> "until" form 
> 
> p.2
> Same as above in abstract grammar for clocked properties.
> 
> p.6
> F.2.3.2.7
> REPLACE
> (p s_until q) == ((p s_until q) and eventually p) [circular]
> WITH
> (p s_until q) == ((p until q) and s_eventually q)
> OR
> (p s_until q) == not (not q until_with not p)
> 
> 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.
> 
> 
> 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:
> 
> 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]
> 
> eventually[m:m] p == next[m] p [m>=0]
> eventually[m:n] p == eventually[m:n-1] p or next[n] p [0<=m<n]
> always[m:m] p == always[m] p [m>=0]
> always[m:n] p == always[m:n-1] p and next[n] p [0<=m<n]
> s_eventually[m:n] p = not always[m:n] not p
> s_always[m:n] p = not eventually[m:n] not p
> 
> 
> /Johan
> -- 
> ------------------------------------------------------------
> Johan Mårtensson                 Office: +46 31 7451913
> Jasper Design Automation         Mobile: +46 703749681 
> Arvid Hedvalls backe 4           Fax: +46 31 7451939
> 411 33 Gothenburg, Sweden        Skype ID: johanmartensson
> ------------------------------------------------------------
> 
> -- 
> 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 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.