narain@randvax.UUCP (Sanjai Narain) (03/20/90)
Following are abstracts of two reports nearly ready for outside
distribution. They bear some relevance to recent enquiries on
real-time logic programming.
Regards.
Sanjai Narain
PROVING TEMPORAL PROPERTIES USING THE CAUSALITY RELATION
Sanjai Narain
ABSTRACT
Frequently, dynamic systems arise whose descriptions involve explicit
mention of time. A new technique is presented for proving temporal
properties of such systems. It offers two main advantages. First, it can
be used to prove temporal properties involving continuous time and state.
Second, it is fairly simple as it utilizes well-developed intuitions about
causality and top-down inference. It is illustrated by proving safety and
liveness properties about the abstract behavior of a system of real-time
programs.
The technique is based upon expressing temporal properties in terms of
questions about event occurrences. It is proposed that such questions can
be answered in a simple manner provided the causality relation between
events can be inferred. To facilitate its inference, it is proposed that
a model of a system be a definition of causality itself. However, if
important types of statements about it are formalized in the obvious
manner, causality can be quite difficult to infer. A new view of
causality is introduced which allows such statements to be formalized
using definite clauses. A simple proof procedure for these called
SLD-resolution greatly simplifies inference of causality.
A NEW MODELING TECHNIQUE BASED UPON
THE CAUSALITY RELATION
Sanjai Narain & Jeff Rothenberg
ABSTRACT
Formal techniques for modeling dynamic systems are intended either for
purely discrete systems, or for purely continuous systems. However,
systems which can exhibit both discrete and continuous behavior frequently
arise in engineering, manufacturing, robotics or computer animation. This
paper presents DMOD, an efficient, formal technique for modeling these,
based upon a novel view of the causality relation. It is proposed as a
logical description of the widely used event-scheduling view of the
discrete-event simulation technique. However, it is substantially simpler
yet more expressive.
A central task in modeling such systems is computing when critical
conditions are satisfied by their state. Due to the possibility of event
occurrences, this task cannot be accomplished by straightforward
extrapolation of continuous functions governing state. It is shown how it
can be accomplished by treating satisfaction of critical conditions as
events and using statements about causality which refer to the future of
causing events.