[FM-India] PhD opening at VERIMAG, Grenoble

[Madhavan Mukund]

PhD Proposal:

Data Mining  Dynamic Behaviors using Signal Temporal Logic

Tempo group
VERIMAG,
University of Grenoble-Alpes
France

Supervisors: Oded Maler and Nicolas Basset

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 in
http://www-verimag.imag.fr/~maler/Papers/checking.pdf
and a recent survey appears in
http://www-verimag.imag.fr/~maler/Papers/monitor-RV-chapter.pdf

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 in
http://www-verimag.imag.fr/~maler/Papers/identify-tl.pdf
and
http://www-verimag.imag.fr/~maler/Papers/parametric-hscc18.pdf
>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:

1) A comparison with other approaches to learn from temporal behaviors such as
RNN and automata;
2) Fundamental and algorithmic studies on the quantitative semantics of STL
which reflects the robustness of satisfaction in space and time;
3) An implementation of different approaches (search, quantifier elimination,
backward computation) to solve the parametric identification problem, exactly
or approximately;
4) Handling the fact that while observing system behaviors we have only
positive examples;
5) 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;
6) Applying the resulting algorithms to case-studies coming from
cyber-physical systems and mostly from systems biology.
7) 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 Computer
Science, Electrical Engineering, Mathematics 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 at univ-grenoble-alpes.fr and nicolas.basset1 at 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, 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. 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).

-- 
===============================================================
Oded Maler, VERIMAG, Bat. IMAG, 700 av. Centrale, 38401 St Martin d'Heres,
France. Phone: +33 (0) 4 57 42 22 29 fax: 4 57 42 22 22
http://www-verimag.imag.fr/~maler  Oded.Maler at univ-grenoble-alpes.fr
===============================================================