On Discrete Modeling and Model Checking for Nonlinear Analog Systems

摘要

In this contribution we present a new method for developing discrete models for nonlinear analog systems. Using an adaptive state space intersection method the main nonlinear properties of the analog system can be retained. Consequently, digital model checking ideas can be applied to analog systems. To describe analog specification properties an extension to the standard model checking language CTL and the appropriate, algorithmic modifications are needed. Two nonlinear examples are given to show the feasibility and the advantages of this method.