Objectives

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.