Toward Model Selection by Formal Methods

We address the problem of selecting a model from a list of potential models in the field of dynamical systems. The selection is based on model behaviour specified in temporal logic rather than time series. This provides more global constraints on the system dynamics. Not only to select one model but also to create an ordered structure, we propose the model ordering problem. We suggest and apply several ordering relations comparing models given property specification. To provide a formal method with global results for the proposed setting we employ and adapt model checking and parameter synthesis methods. To evaluate the method, we apply the proposed method to several qualitative models of regulatory networks.