We present a method
for specifying
temporal
con-
straints on trajectories
of dynamical
systems and en-
forcing them during qualitative
simulation.
This ca-
pability can be used to focus a simulation,
simulate
non-autonomous
and piecewise-continuous
systems,
reason about boundary
condition problems and incor-
porate observations
into the simulation.
The method
has been implemented
in TeQSIM, a qualitative simu-
lator that combines the expressive power of qualitative
differential
equations
with temporal
logic.
It inter-
leaves temporal
logic model checking with the simu-
lation to constrain
and refine the resulting predicted
behaviors and to inject discontinuous
changes into the
simulation.
