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

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.