Subject: Re: draft of reponse to vardi: Re: Clocked Sugar Formulas (fwd)
From: Moshe Vardi (vardi@cs.rice.edu)
Date: Tue Aug 07 2001 - 08:59:48 PDT
Thanks for the 4th version of Sugar's clock semantics, Dana. I think that
Andreas and I have done more than enough to debug your semantics, so we'll
stop at this point.
Note, however, that it might be quite unintuitive to say that "p is
inevitable" (i.e., AFp), only to discover that p never occurs because the
clock did not tick. ForSpec lets the user decide if the clock is strong or
weak.
Moshe
---------- Forwarded message ----------
Date: Wed, 8 Aug 2001 05:49:30 +0300
From: Dana Fisman <DANAF@il.ibm.com>
To: Moshe Vardi <vardi@cs.rice.edu>
Cc: dana@narkis.wisdom.weizmann.ac.il
Subject: Re: draft of reponse to vardi: Re: Clocked Sugar Formulas (fwd)
Moshe,
AFp::c = A [true U p]::c =
= A [!c W (c & A[(!c | (c&true)) U (A [(!c W (c&p)])])]
= A [!c W (c & AF (A [(!c W (c&p)])]
Thus, if there is an infinite number of clocks, p is required to arrive,
whereas if there is only finite number of clocks, there is no requirement.
This is similar to the case of the formula AF false on a finite model.
I attached a revised version of the clocks definition, as some cases have
been left out, as well as the sentence saying we work on the positive
normal form.
Dana.
(See attached file: sugar_clocks.ps)
---------- Forwarded message ----------
Date: Mon, 6 Aug 2001 07:56:44 -0500 (CDT)
From: Moshe Vardi <vardi@cs.rice.edu>
To: dana@narkis.wisdom.weizmann.ac.il
Subject: Re: Clocked Sugar Formulas
As an example, give me the semantics of AFp::c.
Thanks,
Moshe
*******Attachment(s) have been removed*******
This archive was generated by hypermail 2b28 : Tue Aug 07 2001 - 09:09:57 PDT