[FM-India] PhD position at Grenoble

Deepak D'Souza deepakd at csa.iisc.ernet.in
Tue Feb 14 13:10:35 IST 2017

Request to circulate from Oded Maler:

VERIMAG is Looking for a PhD Candidate

VERIMAG in Grenoble, France, is one of the leading laboratories
worldwide in topics related to the design, implementation and
validation of Cyber-Physical Systems. VERIMAG's past achievements
include the pioneering work on Model Checking (J. Sifakis, Turing
award) and the development of the synchronous data-flow languages
Lustre (P. Caspi and N. Halbwachs) underlying the SCADE programming
environment for safety-critical systems.

The Tempo team led by Oded Maler is among have made pioneering and
high impact work on hybrid (discrtete-continuous) systems that
include: 1) verification by reachability computation; 2) simulation
-based verification and falsification and 3) Monitoring against
properties specified in STL (signal temporal logic).  The group has
now a new PhD opening, partially financed by a French-Indian project,
and is looking for an Indian PhD candidate. A brief description of the
topic is given below.

Topic: Analysis of Network Flows using Hybrid

Automata Supervisors: Oded Maler and Goran Frehse

We are interested in networks consisting of buffers with bounded
capacity, connected through channels that can be opened and closed.
The channels are characterized by bounds on their flow rates. The
system is subject to uncertainty (non-determinism) due to unknown
inflows and imprecise rates. Such systems can model networks of
containers in chemical plants, approximate models of river basins as
well as communication networks and highway traffic flows.

We will use as a starting point the work of [1,2] which translates
such networks into "linear" hybrid automata (LHA) where each discrete
state (mode) corresponds to a combination of open/closed channels, and
transitions between the states can be either due to uncontrolled
events (a buffer becomes empty) or a decision of a con troller to
open/close a channel. The continuous variables indicate the levels in
each buffer. The derivative of each continuous variable is constrained
to be between two constants as a function of its inflow and outflow.

In principle, the behavior of such systems can be analyzed by
reachability techniques for LHA, as implemented in the Phaver branch
of the SpaceEx tool, but since the number of states in the automaton
increases exponentially with the number of network components, state
explosion will be manifested soon.

The thesis will improve the state-of-the-art in modeling and analysis
of such network s. Its goal is to develop verification-style
techniques for the analysis and controller synthesis for such system
s in order to satisfy safety (e.g. no overflow) and liveness
(e.g. reaching some level at some buffer within a pre-specified time)
properties. Activities during the thesis include:

1) Developing a modeling methodology, adapted to each
of the selected application domains, taking care of sanity conditions
(conservation laws, non-Zeno behaviors) as well as complexity/fidelity

2) Improving the algorithmics of the Phaver branch of the SpaceEx
tools so as to enlarge the scope of LHA that can be treated.

3) Develop ing abstraction and aggregation techniques that
collapse a sub-network into a single buffer at the price of
over-approximating the reachable states.

4) Replacing or augmenting set-based reachability with s tatistical
and guided exploration of individual scenarios.

5) Develop ing synthesis algorithms in a game-theoretic framework for
this type of systems.

We are looking for excellent candidates with the following features:

1) Master degree in CS/EE/Math or equivalent.

2) Satisfactory understanding of
theoretical computer science (automata, algorithms, logic) as well as
linear algebra.

3) Decent programming skills.

4) A genuine motivation (if not passion) to do research.

5) Acquaintance with verification and applied mathematics is an 

Serious candidates should send a CV and a motivation letter by e-mail
to Oded.Maler at imag.fr and Goran.Frehse at imag.fr with "Phd position" in
the title.


[1] O. Maler, Guest Editorial: Verification of
Hybrid Systems, Europ ean Journal of Control 2001

[2] G. Frehse, O. Maler,
Modeling and Analysis of Switched Buffer Networks using Hybrid
Automata, 2006.  http://www-verimag.imag.fr/~maler/Papers/buffers.pdf

This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.

More information about the FMIndia mailing list