Abstracts

Temporal Logic and QSIM

Temporal Logic Trajectory Constraints and QSIM

  • Giorgio Brajnik and Daniel J. Clancy. 1997. Focusing qualitative simulation using temporal logic:Theoretical Foundations To appear in the Annals of Mathematics and Artificial Intelligence.
  • 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.

  • Giorgio Brajnik and Daniel J. Clancy. 1997. Control of Hybrid Systems using Qualitative Simulation. Working notes from the 11th International Workshop on Qualitative Reasoning about Physical Systems (QR-97) , June 1997.
  • 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.

  • Giorgio Brajnik and Daniel J. Clancy. 1996. Temporal constraints on trajectories in qualitative simulation. In Proceedings of the National Conference on Artificial Intelligence (AAAI-96), AAAI/MIT Press, 1996.
  • 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.

  • Giorgio Brajnik and Daniel J. Clancy. 1996. Temporal constraints on trajectories in qualitative simulation. In Working Papers of the Tenth International Workshop on Qualitative Reasoning (QR-96), Fallen Leaf Lake, California.
  • 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.

  • Giorgio Brajnik and Daniel J. Clancy. Guiding and refining simulation using temporal logic. Third International Workshop on Temporal Representation and Reasoning (TIME'96), 1996.
  • 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.


    [QR home]

    BJK