jeudi 9 Novembre, 14h en salle Markov
Euler’s method applied to the control of switched systems
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) synthezing 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. We will sketch out how the approach relates with other symbolic methods based on interval arithmetic and Lyapunov functions. We will also present some applicative examples which illustrate its advantages and limitations.
Exposés des semaines suivantes
jeudi 23 novembre, 14h en salle Lipari
Structural Analysis of Multi-Mode DAE Systems
Differential Algebraic Equation (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica, VHDL-AMS, or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multi-mode DAE (mDAE) systems are much harder to deal with, not only because of their mode-dependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs does not cover the multi-mode case. It typically says nothing about mode changes. This lack of foundations cause numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this talk we develop a comprehensive mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way.
jeudi 7 Décembre, 14h en salle Minquiers
Benoit Delahaye, Univ. Nantes
Reachability in Parametric Interval Markov Chains using Constraints
Parametric Interval Markov Chains (pIMCs) are a specification formalism that extend Markov Chains (MCs) and Interval Markov Chains (IMCs) by taking into account imprecision in the transition probability values: transitions in pIMCs are labeled with parametric intervals of probabilities. In this work, we study the difference between pIMCs and other Markov Chain abstractions models and investigate the two usual semantics for IMCs: once-and-for-all and at-every-step. In particular, we prove that both semantics agree on the maximal/minimal reachability probabilities of a given IMC. We then investigate solutions to several parameter synthesis problems in the context of pIMCs – consistency, qualitative reachability and quantitative reachability – that rely on constraint encodings. Finally, we propose a prototype implementation of our constraint encodings with promising results.
Lundi 11 Décembre, 11h en salle Minquiers
jeudi 14 Décembre, 14h en salle Minquiers
Shuvra S. Bhattacharyya, University of Maryland and Tampere University of Technology
The DSPCAD Framework for Dataflow-based Design and Implementation of Signal Processing Systems
Dataflow-based design methodologies are important for addressing the growing complexity of signal processing systems, including systems for wireless communications, machine learning, video processing, and biomedical instrumentation. This complexity is compounded by the need to exploit parallelism effectively, satisfy stringent power consumption requirements, and work with heterogeneous processing resources and sensing modalities. The DSPCAD Framework is a computer-aided design (CAD) framework that helps designers to apply the formalisms of the dataflow paradigm in software/hardware design processes for signal and information systems. The DSPCAD Framework is specifically oriented toward exploration of interactions and optimizations across different signal processing application areas; alternative dataflow models of computation; and alternative target platforms along with their associated platform-based tools (e.g., field programmable gate arrays, graphics processing units, multicore digital signal processors, and low power microcontrollers). In this talk, I will first review challenges in dataflow-based design methodologies for signal processing systems, and then present key aspects of the DSPCAD Framework that help to address these challenges.