The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
We will describe our novel high-performance algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems based on coloured model checking. The method employs a symbolic representation of sets of parameter valuations in terms of first-order theory of the reals. Moreover, we will discuss an interesting extension of the algorithm that allows to address the problem of bifurcation analysis of parameterised high-dimensional dynamical systems.
To this end, we introduce the hybrid CTL logic augmented with direction formulae. This allows us to describe various behaviour patterns and phase portraits. Finally, we will describe applications of the method to a class of piecewise multi-affine dynamical systems representing dynamics of biological systems with complex non-linear behaviour involving multi-stability or limit cycles.