Reasoning About Continuous Processes

Abstract

Overcoming the disadvantages of equidistant discretization of continuous actions, we introduce an approach that separates time into slices of varying length bordered by certain events. Such events are points in time at which the equations describing the system's behavior---i.e., the equations which specify the ongoing processes--- change. Between two events the system's parameters stay continuous. A high-level semantics for drawing logical conclusions about dynamic systems with continuous processes is presented, and we develop an adequate calculus to automate this reasoning process. In doing this, we have combined logical reasoning and numerical calculus offering qualitative reasoning as well as precise, quantitative system information. The example of multiple balls moving in 1-dimensional space interacting with a pendulum serves as demonstration of our method. Acknowledgments We wish to thank Jason Brown for valuable programming hints in PROLOG and Antje Strohmaier for some mathema...