Toward Systems Biology

May 30 - 31, June 1, 2011

Grenoble

Home         Confirmed speakers         Program         Registration         Venue         Accommodation

Under-Determined Dynamical Systems and Formal Verification

A dynamical system is a mathematical construction that produces trajectories, traces, etc., which are progressions of states over time. A simulator, in order to produce such a trace, needs a precise rule to proceed from one state to its successor. In reality, such deterministic models do not really exist and dynamical models are under-determined for many reasons:

  1. The initial state of the system is not the same in each instance
  2. The system parameters are not known exactly due to experimental limitation, e.g., kinetic parameters in biochemical reactions
  3. The systems in question are exposed to external disturbances, e.g., heat and each profile of this external input leads to a different trajectory;
  4. The model is part of a hierarchical multi-level system where each level is an abstraction or an approximation of a more detailed model at a lower level.

The result of all these and other reasons is that in system design and analysis, both in science and engineering, one has to deal with dynamical system models that are under-determined, they have some components which are not known precisely but ranging in some domain that we call the uncertainty space. This space can be static (choice of parameters or initial conditions) or dynamic (choices of external disturbances) which are sometimes referred to finite and infinite-dimensional.

A major question in all application domains is the following: how to take this uncertainty space into account while evaluating the system, either qualitatively or qualitatively. Each choice of a point in this space leads to a unique behavior (simulation trace) but there are typically infinitely-many such points and induced behaviors. In my talk I will survey three common approaches to handle the uncertainty space, namely:

  1. Taking one typical representative (fixing a parameter, initial condition and external input)
  2. Covering all the uncertainty space (formal verification, model checking, reachability computation for hybrid systems)
  3. Statistical coverage of the space assuming (or not) it admits some probability.

The utilization of these methods across disciplines and sub cultures is sometimes a result of historical accidents and sometimes reflects the nature of the dynamics (the more it is continuous and linear, a typical case will suffice) and the criticality of the systems.

Oded Maler, CNRS-VERIMAG, Grenoble