We demonstrate an automated method for proving temporal logic statements about solutions to ordinary differential equations (ODEs), even in the face of an incomplete specification of the ODE. The method combines an implemented, on-the-fly, model-checking algorithm for statements in the temporal logic CTL* [Bhat, et al, 1995; Clarke, et al, 1986; Emerson, 1990] with the output of the qualitative simulation algorithm QSIM [Kuipers, 1986, 1994]. Based on the QSIM Guaranteed Coverage Theorem, we prove that for certain CTL* statements, $\Phi$, if $\Phi$ is true for the temporal structure produced by QSIM, then a corresponding temporal statement, $\Phi'$, holds for the solution of any ODE consistent with the qualitative differential equation (QDE) that QSIM used to generate the temporal structure.
A more detailed formalization of part of the QSIM framework has been found to be useful. That formalization is presented here in brief. The new formalization makes it easier to make and prove some useful statements. The formalization of temporal reasoning about continuous systems [Shults and Kuipers, 1996] and the precise definition of completeness are examples of the usefulness of this formalization.
An intelligent agent, reasoning symbolically in a continuous world, needs to infer properties of the behaviors of continuous systems. A qualitative simulator, such as QSIM, constructs a set of possible behaviors consistent with a qualitative differential equation (QDE) and initial state. This set of behaviors is expressed as a finite tree of qualitative state descriptions. In the case of QSIM, this set is guaranteed to contain the ``actual'' behavior under certain circumstances. We call this property the ``soundness'' of QSIM. The behavior tree can then be interpreted as a model for statements in a branching-time temporal logic such as Expressive Behavior Tree Logic (EBTL), which we introduce. Because QSIM is sound, validity of an EBTL proposition {\tt (necessarily $p$)} implies the corresponding theorem about the dynamical system described by the QDE. Therefore, at least for universals, statements in temporal logic about continuous systems can be proved by qualitative simulation. This allows a hybrid reasoning system to prove such common-sense statements as ``what goes up (in a constant gravitational field) must come down", or to do such expert reasoning about dynamical systems as proving the stability of a non-linear, heterogeneous controller.
We illustrate TeQSIM, a qualitative simulator for continuous dynamical systems that combines the expressive power of qualitative differential equations with temporal logic to constrain and refine the resulting predicted behaviors. Temporal logic is used to specify constraints that restrict the simulation to a region of the state space and to specify trajectories for input variables. A propositional linear--time temporal logic is adopted, which is extended to a three valued logic that allows a formula to be conditionally entailed when quantitative information specified in the formula can be applied to a behavior to refine it. We present a formalization of the logic with correctness and completeness results for the adopted model checking algorithm. We show an example of the simulation of a non--autonomous dynamical system and illustrate possible application tasks, ranging from simulation to monitoring and control of continuous dynamical systems, where TeQSIM can be applied.
This paper presents a methodology for synthesizing, under uncertainty, a sequence of robust, discrete control actions to drive a continuous dynamical plant through admissible trajectories specified via temporal logic expressions. An action is defined as a modification to the value of a controllable exogenous variable. The TeQSIM algorithm combines qualitative simulation with temporal logic model checking to validate or refine a proposed plan. Qualitative simulation is used to infer a branching--time description of the system behaviors that potentially follow from a sequence of control actions. This description is queried using temporal logic based goal constraints to perform plan validation. Plan refinement infers bounds on the sequence of actions within a plan to guarantee that the specified goal constraints are satisfied.
A framework for plan generation is presented that uses a phase portrait representation to reason about the effect of each action within a particular system configuration. Each set of distinct values for the controllable exogenous variables defines a separate configuration of the dynamical system. The behavior of the system within each configuration is described using a phase portrait representation. These representations are compared to determine the effect of an action within a region of the phase plane and to determine when the action is appropriate to resolve a goal violation. This methodology is able to prune the plan search space by eliminating actions that are unable to resolve a detected violation.
We present a method for specifying temporal constraints on trajectories of dynamical systems and enforcing them during qualitative simulation. This capability can be used to focus a simulation, simulate non--autonomous and piecewise--continuous systems, reason about boundary condition problems and incorporate observations into the simulation. The method has been implemented in TeQSIM, a qualitative simulator that combines the expressive power of qualitative differential equations with temporal logic. It interleaves temporal logic model checking with the simulation to constrain and refine the resulting predicted behaviors and to inject discontinuous changes into the simulation.
We present a new method for specifying temporal constraints on trajectories of dynamical systems and enforcing them during qualitative simulation. Such constraints are otherwise inexpressible using standard qualitative reasoning techniques. Trajectory constraints can be used to restrict the simulation to a region of the state space and to inject discontinuities. This capability can be used to focus the simulation for larger, more complex simulations, simulate non--autonomous and piecewise--continuous systems, reason about boundary condition problems and incorporate observations into the simulation. The method has been implemented in TeQSIM, a qualitative simulator. It combines the expressive power of qualitative differential equations with temporal logic by interleaving temporal logic model checking with the simulation to constrain and refine the resulting predicted behaviors and to inject discontinuous changes into the simulation.
The paper discusses the applicability of temporal constraints in tasks ranging from simulation to monitoring and control of continuous dynamical systems. We present a real--world control problem in the domain of water supply. Finally, the basic algorithm and theoretical results (soundness and completeness) are described.
We illustrate TeQSIM, a qualitative simulator for continuous dynamical systems. It combines the expressive power of qualitative differential equations with temporal logic by interleaving simulation with model checking to constrain and refine the resulting predicted behaviors. Temporal logic expressions are used to specify constraints that restrict the simulation to a region of the state space and to specify trajectories for input variables. A propositional linear--time temporal logic is adopted, which is extended to a three valued logic that allows a formula to be conditionally entailed when quantitative information specified in the formula can be applied to a behavior to refine it. We present a formalization of the logic with theoretical results concerning the adopted model checking algorithm (correctness and completeness). We show also an example of the simulation of a non--autonomous dynamical system and illustrate possible application tasks, ranging from simulation to monitoring and control of continuous dynamical systems, where TeQSIM can be applied.