Focusing qualitative simulation using temporal logic: theoretical foundations |
| |
Authors: | Giorgio Brajnik Daniel J Clancy |
| |
Affiliation: | (1) Dipartimento di Matematica e Informatica, Università di Udine, 33100 Udine, Italy;(2) Department of Computer Sciences, University of Texas at Austin, Austin, Texas 78712, USA |
| |
Abstract: | 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 revised version was published online in June 2006 with corrections to the Cover Date. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|