Subject: [sv-ac] forward progress of time
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Mon Feb 03 2003 - 00:12:03 PST
all,
as i said previously, i wholeheartedly agree with john havlicek on the
problems of the sequence implication operator as it is currently defined,
and with his proposal to make it a property rather than a sequence. i
would like to say a few more words about the problems with the current
definition, to make sure that my point of thursday's meeting is clear.
john expresses the problem in terms of context sensitivity. i would like
to view the problem from another angle - that of the forward progress of
time (these are related, of course). consider the following:
((a;b;c) => (d;e;f)) ; w (example 1)
that is, a sequence implication of ((a;b;c) => (d;e;f)) concatenated with
"w". consider two paths:
1. a path where (a;b;c) occurs and is followed by (d;e;f)
2. a path where (a;b;c) does not occur. for instance, a path where only
(a;b) occurs, but "c" does not occur at the cycle following "b".
say that in both cases, the occurence of "a" is at time 0. then, according
to the current definition:
1. on path #1, "c" happens at time 2, so so does "d", and thus "f" happens
at time 4, and therefore we require "w" at time 5.
2. on path #2, the sequence ((a;b;c) => (d;e;f)) is matched vacuously
(according to page 58, last line) and returns true at time 0. therefore,
we require "w" at time 1.
thus, the theoretical problems of the current definition can be understood
intuitively as somehow confounding the "forward progress of time" in a
sequence, as someone put it in thursday's meeting. that is, whatever we
intuitively would have expected of example 1 above, it is not a requirement
that "w" occur the cycle following "a".
john's proposal to move the sequence implication operator up a level to a
property will eliminate this very undesirable characteristic of the current
definition.
regards,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
This archive was generated by hypermail 2b28 : Mon Feb 03 2003 - 00:09:35 PST