Using Analytic CLP to Model and Analyze Hybrid Systems
Timothy J. Hickey, David Wittenberg · 2004
We use CLP(F), an Analytic Constraint Logic Programming language, to model hybrid systems. Analytic CLP languages combine intervals, constraints, and ODEs in a clean and natural way. CLP(F) provides a implementation of an ACLP language based on Interval Arithmetic. The semantics of CLP(F) rigorously handle non-linear ODEs and round-off error. The ODEs describing a hybrid system need only a minor change of syntax to become a CLP(F) program. This simple transformation from a physical description of a hybrid system to a program which can be used to provide a proof of safety properties of the system bridges the gap between practical tools and formal models, and allows one to easily prove statements about real-world systems. The combination of Interval Arithmetic with Analytic Constraint Logic Programming makes it easy to pose and answer many sorts of queries about a system. For example, “At what point does the system change from one state to another?”, or “What control settings result in a cycle with period t?” 1