Subject: Re: Temporal e
From: Matthew Morley (matthew@verisity.com)
Date: Tue Jul 10 2001 - 16:47:04 PDT
mjm> for the purposes of defining the semantics of temporal e we
mjm> introduced negation as an operator to the abstract syntax, but
mjm> you will see that we use it only to define user-expressible
mjm> constructs "firstmatch" and "fail" -- without which the language
mjm> would indeed be rather weak. the operational semantics of both
mjm> these operators introduce deterministic state machines.
vardi> Does "Temporal e" includes negation? Your document indicates
vardi> that it does.
i attempted above to clarify, my apologies if i failed to succeed.
temporal e defines "fail" and "not" operators, neither of which is
true "negation" (or "complement"). in defining the semantics of the
concrete syntactic elements of the language we have used negation
purely as a technical device. the same goes for infinite disjunction.
i should perhaps add that i don't believe this committee would want to
adopt the semantics of the "not" operator as it is defined in e (see
the language definition manual). this operator could perhaps be called
"not now" -- the embedded temporal expression does not succeed now, on
this clock cycle.
vardi> L. Stockmeyer. The complexity of decision problems in automata
vardi> and logic, Ph.D. Thesis, MIT, 1974.
thanks.
vardi> What is the "sigma star fragment"? What is "the omega extension
vardi> of the sigma star language"?
the "Semantics of Temporal e" paper describes the finite sequences
(sigma star is the universe of discourse). for those sentences in the
language that cannot be decided (one way or the other) in finite time,
things like
@p => fail {[..];@p} // concrete syntax!
one needs omega length sequences. David's note discusses this. the
principle requirement of course is that the semantics agree on those
properties that can be defined in finite time.
vardi> Yes, EXPSPACE is indeed elementary, since it is included in
vardi> dobly exponential time. I infer, however, that youhave not
vardi> developed a tableau construction for full Temporal e. Right?
again, as i said in the earlier email, we have tableau constructions
for the finite sequence semantics (or simulation semantics if you
like), and the infinite sequence semantics. the latter builds directly
on the former.
please refer to the table on page 16 of the "semantics of Temporal e"
paper for a succinct statement of the operators of the language.
please also accept my sincere apologies for the slight confusion that
the presence of "negation" in the definition of these operator causes.
i couldn't see a better way at the time!
M
--
This archive was generated by hypermail 2b28 : Tue Jul 10 2001 - 16:48:47 PDT