Trajectory constraints in qualitative simulation

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.