LSV ,ENS de Cachan, salle de conférences du pavillon des jardins (accès ici).
Abstract : Hybrid systems are a powerful formalism for modeling and reasoning about cyber-physical systems. They mix the continuous and discrete natures of the evolution of computerized systems. Switched systems are a special kind of hybrid systems, with restricted discrete behaviours: those systems only have finitely many different modes of (continuous) evolution, with isolated switches between modes. Such systems provide a good balance between expressiveness and controllability, and are thus in widespread use in large branches of industry such as power electronics and automotive control. The control law for a switched system defines the way of selecting the modes during the run of the system. Controllability is the problem of (automatically) synthesizing a control law in order to satisfy a desired property, such as safety (maintaining the variables within a given zone) or stabilisation (confinement of the variables in a close neighborhood around an objective point). In order to compute the control of a switched system, we need to compute the solutions of the differential equations governing the modes. Euler’s method is the most basic technique for approximating such solutions. We present here an estimation of the Euler’s method local error, using the notion of “one-sided Lispchitz constant’’ for modes. This yields a general synthesis approach which can encompass uncertain parameters, local information and stochastic noise.
Abstract : Discrete regulatory network modelling combines a graph of pairwise influences between the variables of the system and a parametrisation, from which can be derived a discrete transition system. Given the influence graph only, the exploration of possible parametrisations is computationally challenging due to combinatorial explosion of both parametrisation and reachable state space.
We introduce an abstraction of the parametrisation space, including a refinement with respect to transitions. The abstraction is then coupled with unfolding semantics for Parametric Regulatory Networks taking advantage of concurrency between transitions to achieve a compact representation of reachable state space.