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
[email protected] and [email protected]
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).
--
Please note change of address, phone number and e-mail
===============================================================
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 [email protected]
===============================================================
----
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ [email protected] ]]
