Benjamin Shults and Benjamin Kuipers. 1997.
Proving properties of continuous systems:
qualitative simulation and temporal logic.
Artificial Intelligence 92: 91-129, 1997.
Abstract
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.
Download full paper
[QR home: http://www.cs.utexas.edu/users/qr]
BJK