The major goal of the project is to develop new techniques for extracting information from temporal behaviors (signals, wave-forms, sequences), and come up with succinct representation that captures their properties. These behaviors, can be a result of running simulations or measuring actual systems in various domains. In some application domains temporal data mining is handled by techniques coming from machine learning (recurrent neural networks (RNN), automaton learning), statistics and control (system identification). The project will explore the applicability of Signal Temporal Logic (STL) for inferring classifiers and for clustering of such behaviors.

STL is a simple extension of temporal logic used to specify properties of real-valued signals defined over continuous time. It can express, for example constraints on the temporal distance between events such as threshold crossings of various variables. 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, biochemical models of cellular pathways, and cyber-physical control systems, mostly within the automotive domain. An introduction to can be found here and a recent survey appears here

The starting point of the thesis will be the work on parametric identification of temporal properties which solves the following problem: given a behavior and a parametric STL (PSTL) formula, a formula where some threshold and timing constants have been replaced by parameters, find the set of parameters that makes the behavior satisfy the property. More details can be found here and here From the point of view of machine learning, the formula can be viewed as a feature extractor which reduces the signal into a low-dimensional set in the parameter space that can be used for classification and clustering.

The goal of the thesis is to develop these ideas further, theoretically and practically, to the point of being applicable to real-life case-studies. The actual evolution of the thesis will depend, of course, on intermediate results but also on the qualifications and tendencies of the student. Among the topics to be investigated we find:

- A comparison with other approaches to learn from temporal behaviors such as RNN and automata;
- Fundamental and algorithmic studies on the quantitative semantics of STL which reflects the robustness of satisfaction in space and time;
- An implementation of different approaches (search, quantifier elimination, backward computation) to solve the parametric identification problem, exactly or approximately;
- Handling the fact that while observing system behaviors we have only positive examples;
- Developing efficient algorithms for sub-problems encountered during the development of the classification and clustering algorithms, e.g., computing the Hausdorff distance between unions of poyhedra, or approximating monotone functions;
- Applying the resulting algorithms to case-studies coming from cyber-physical systems and mostly from systems biology.
- Integrating the results in the AMT toolbox.

All in all, the thesis offers an opportunity to participate in a leading-edge research in a new and timely domain that combines clean and decent theory, real-life applicability and international collaboration. The thesis is part of the SYMER multi-disciplinary project of the Grenoble university, in collaboration with biologists working on cellular metabolism and epigenetics and the project results will be applied to models developed within the project.

We are looking for motivated candidates with a Masters degree in CS, EE, Math or even Physics, and a solid background in a non-empty subset of computer science (algorithms, automata, logic), control, optimization, formal methods, machine learning, signal processing 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 and a motivation letter to Oded.Maler@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) and Barcelona (6 hours). 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 Ausrtria) or integrate in industry (Mathworks, Intel, local start-ups) or R&D organization (Austrian Institute of Technology).