The DISTOL project (Distributed systems, stochastic models and logics) aims at gathering researchers from
INRIA Rennes, two institutes in Chennai, India (CMI and IMSC) and National University of Singapore, working on formal modeling and verification of distributed systems. This project covers four main research directions. Each of these directions rely on specific and complementary competences:

## R1: Robustness and time issues in distributed systems models

Our main objective is to consider robustness for true concurrency models in a context where each
process has its own measurement of time. We will start this study with timed variants of Petri
nets, building on former results on this model [E-AHJLR12,E-AHJR12], and on experience gained
for automata with independently evolving clocks [E-AGMK08]. A first step is to formalize independence
of processes and clocks in time(d) Petri nets, and the robustness problems for this model. Several
problems could be undecidable, so the next step is to find reasonable restrictions ensuring the
existence of (semi) decision procedures.
## R2: Applications of formal models & techniques to Web Services

We want to consider realistic models for Web-Services. We have already proposed a session model for
Web Services [J-DHM11]. It describes finite sets of agents running an arbitrary number of concurrent
transactions. Coverability of some (bad) configuration is decidable for this model. We first want to
extend our model and decision procedures to systems with arbitrary numbers of agents. A key challenge
is to build realistic but well-structured models, to allow straightforward decidability of interesting
safety properties. The second objective is to consider more elaborated properties than coverability,
such as conflicts of interest between agents, etc. Overall, we wish to propose a highly expressive model
together with a decidable logic to reason on this model. The techniques used to reach this goal will
build on our knowledge of Well-Structured Transition System [O-FS01], and Petri nets variants. The
last and most exploratory objective is monitoring for session systems: from a model M of a system,
an implementation I of this model, and a property to monitor, we want to instrument I with observers
(synthesized from M) that raise an alarm when they are sure that the property is violated. Monitoring
was studied for pi-calculus [O-HYC08], but it is not yet clear whether the proposed solutions apply
to our setting.
## R3: Quantitative verification for distributed systems

In the next three years, we will develop algorithms to compute precisely probabilities of logical properties,
in particular in the presence of imperfect information and/or time. We will build on our work in [J-BG11].
We will also improve the precision of approximated inference algorithms for distributed (parameterized or not)
systems, and deduce formal bounds that guarantee the probability to be in an interval of bounded size.
For that, we will develop the techniques we introduced in [J-PAGT11]. In particular, we will provide a
decomposition algorithm such that the global approximated probability will be more accurate (through a
better accuracy on each component) than by considering the system as a monolith. This has been a major
objective in analysis of distributed system, but in general, it cannot be reached exactly. However,
approximation gives more freedom for clustering. Last, we will develop approximated verification for
logics different from PCTL, leveraging on [J-AAGT12].
## R4 : Unification of Control Theory of Distributed Systems

The goal of this research direction is a unified theoretical framework for supervisory control theory.
We will investigate to which extent techniques from epistemic reasoning and game theory can be applied
to address control problems for distributed systems. The first milestone will be to reformulate supervisory
control in logical and game-theoretical terms. In that respect, epistemic logic should help to handle
partial observation. The second milestone will consist in bringing together epistemic logic and imperfect
information games to handle individual (i.e. subsystems) knowledge. It is a challenging task because,
taking apart control theory issues, the logical foundation of games with imperfect information is an
emerging field with only few results [O-GDE11,E-MPB11]. The third milestone will consist in incrementing
the previous framework by considering communication mechanisms between the subsystems. In game theory,
communication between players is very primitive, whereas in epistemic logic, there are powerful rigorous
ways to model effects of atomic communication events on the individual knowledge. It is a challenging
task to transfer this apparatus to games and will probably lead to new results in game theory but more
importantly, in distributed control. The fourth milestone will consist in studying properties of the d
eveloped unified framework, both computational and in terms of expressiveness. For this, we may link
the new framework with existing logical formalisms and/or game-based settings.