This fully-funded thesis will take place in the Tempo team at the laboratory Verimag (Grenoble, France) in the context of validation, monitoring and control of cyber-physical systems modelled by timed and hybrid systems. Such a system exhibits both continuous and discrete dynamics and can be seen as a functional operator that maps input signals to output signals. Signals here are multi-dimensional functions from a continuous time domain to a real and/or Boolean valued domain. We are interested in sets of input signals subject to complex temporal constraints described by temporal logics (such as Signal Temporal Logic STL), timed regular expressions (TRE), and timed automata. Both STL and TRE were created in the Tempo team at Verimag. These temporal constraints are more challenging to represent and manipulate than usual mathematical conditions, for example Lipschitz-continuity, bounded variability, etc. An efficient constrained signal space representation is needed in order to analyze the system behaviours induced by such input signals, for both validation and control purposes. The purpose of validation is to check whether under all the possible input signals the system satisfies a desired specification, e.g. the speed of an automatic car is never above a given threshold when in the first gear. The purpose of control is, on the other hand, to find an input signal so that the system satisfies a desired specification while optimising some system performance index.
The thesis consists first of a theoretical study on the metrics between signals that enable to approximate an uncountable constrained set of signals by a finite set of signals, using the notion of epsilon-net or epsilon-separated set from topology and information theory. These metrics should have good properties with respect to system specification formalisms of interest. The second theoretical study involves designing parametrizations of signal sets. Each parameter valuation maps to a signal in the constrained sets, and such parametrizations enable random sampling and optimization directly over constrained signal sets without resorting to costly rejection sampling methods. A dual question to investigate is learning a constrained set that best describes a finite set of input signals.
This theoretical framework will then be applied to validation and control of cyber-physical systems in particular from automotive industry.
We are looking for motivated candidates with (or completing) a Master degree in Computer Science, Mathematics, Control Engineering, and a solid background in a non-empty subset of Computer Science (algorithms, automata, logics), control theory, optimization, formal methods and statistical reasoning. Such candidates who are ready to learn new things and complete their background, are kindly requested to send e-mail (with "PhD-candidate" in the title) a CV, a motivation letter, and if already available a university transcript and Master manuscript, to thao.dang@univ-grenoble-alpes.fr and nicolas.basset1@univ-grenoble-alpes.fr
The Grenoble area, in addition to being surrounded skiable mountains is easily accessible: Lyon (1 hour), Geneva (1.5 hours), Torino (2 hours), Paris (3 hours by train). It features one of Europe's largest concentrations of academic/industrial research and development with a lot of students, a cosmopolite atmosphere and work opportunities.
VERIMAG, is a leading academic lab in verification and model-based design of embedded cyber-physical systems. Its past contributions include model checking (J. Sifakis, Turing Award 2007), the data-flow language Lustre (P. Caspi, N. Halbwachs) underlying the SCADE programming environment for safety-critical systems. The Tempo group at VERIMAG has made pioneering contributions to the study of hybrid cyber-physical systems and its applications, and in particular the development of STL. Group alumni have proceeded to post-doc abroad (Berkeley, Carnegie-Mellon, Cornell, Boston University, IST Austria) or integrate in industry (Mathworks, Intel, local start-ups) or R&D organization (Austrian Institute of Technology).