STL is a simple extension of temporal logic to treat real-valued signals defined over continuous time. Its major use is to monitor behaviors (simulation traces, measurement from a real system during operation) and detect violations of temporal properties. Since its introduction in 2004, STL has been adopted by researchers in many application domains to specify and monitor behaviors of diverse systems such as robots, medical devices (artificial pancreas, anaesthesia machine), analog circuits, cellular pathways, and cyber-physical control systems, mostly within the automotive domain. An introduction to monitoring cyber-physical systems can be found in http://www-verimag.imag.fr/PEOPLE/m...
The underlying theory and algorithms around STL have been extended over the years in several directions that include : 1) definition of a quantitative (robustness) semantics that quantifies how much was a behavior close to violation or satisfaction. This measure has been used successfully in falsification (search for external inputs that drive a system to falsify a property in the framework of simulation-based verification) ; 2) development of more refined diagnostics to locate a minimal sub-signal that implies violation ; 3) the inverse problem of parametric identification : given a set of traces and a parameterized STL formula, find the set of parameters that render the formula satisfied by all the traces. This is a kind of learning from behaviors, resulting in a high-level logical description of the temporal data.
The topics on which the candidate is expected to work are :
1) The use of STL in data mining and machine learning. This is a new research direction whose goal is to observe a sample of dynamic behaviors of cars and other cyber-physical system and provide a succinct description in terms of a temporal logic formula that captures the observed behaviors. The problem may have several variants (positive and negative examples, only positive examples, unsupervised/clustering). This is a fascinating research direction that intends to fuse ideas from formal verification and machine learning in a rigorous but down-to-earth way.This is a relatively open-ended research, not bound to specific deliverables, that will give the candidate the opportunity to catch up with the state-of-the-art in temporal monitoring of cyber-physical system and participate in laying down the foundation of a new domain. It will involve collaboration with the AMA machine leaning group of LIG as well as our industrial partners, including Toyota.
2) Development of an STL-based interactive falsification procedure. Falsification means simulating with different input signals, trying to use the robustness measure to guide the search procedure toward a property-violating input. The work involves the encoding a subset of the input space by finitely many parameters and running a stochastic local search algorithm in this space where for every input signal encountered during the search a simulation and monitoring procedure is executed. The work will involve some programming and tool connection (MATLAB/Simulink, Breach) as well as a close interaction with our industrial collaborators at Toyota who will provide case-studies.
All in all, the job offers an opportunity to participate in a leading-edge research in a new and timely domain that combines clean and decent theory with *real* real-life applicability. Motivated candidates with a PhD degree in CS, EE, Math or even Physics, and a solid background in a non-empty subset of computer science, control, optimization, formal methods, machine learning, signal processing or statistical reasoning, are kindly asked to send (e-mail with "Post-Doc-candidate" in the title) a CV and a motivation letter to Oded.Maler@imag.fr,Thao.Dang@imag.fr and Eric.Gaussier@imag.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) and Barcelona (6 hours). It features one of Europe’s largest concentrations of academic/industrial research and development with a lot of students and a relatively-cosmopolite atmosphere. Many of the PhD and post-doc alumni are recruited by local hi-tech companies.
VERIMAG, http://www-verimag.imag.fr 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, as well as pioneering contributions to the study of timed and hybrid systems and its applications.
The AMA team (dAta analysis, Modeling and mAchine learning) was created in LIG in January 2011 to work on machine learning and information modeling for complex data. Within this framework, the team is interested in developing new theoretical tools, as well as new prototypes to be deployed in classification or simulation settings. The research activity in the AMA team is structured in the following three main themes : data analysis and learning theories, learning and perception systems, modeling social networks.
