Task R1: Robustness and time issues in distributed systems models

This year, we have proposed a verification framework for a timed variant of Petri nets called time Petri nets with Urgency. Two models have been mainly considered in the literature: time Petri nets, which associate ages to tokens, constraints to flows and allow firing a transition t if for each place p in the preset of a the transition, there is a token which age satisfy the constraint associated to p and t. Time Petri nets allow for the verification of coverability properties, but cannot model urgency: tokens are simply useless when they become too old. On the other hand, timed Petri nets associate firing intervals to transitions, Intervals describe the time that can elapse since enabling of a transition. Reaching the upper bound of an interval forces a transition to fire. Unlike time Petri nets, most of properties of timed Petri nets are undecidable. We have proposed a variant of timed Petri nets with urgency, and showed that a simple separation of places into bounded/unbounded places, together with a restriction on the urgency constraints attached to transitions that consume tokens from unbounded places allow to decide reachability properties. A paper is submitted (INDIA-FRANCE). Next year will be devoted to robustness in such a setting.

Task R2: Well-structure of Session systems over infinite sets of agents

We have progressed on the work initiated in 2013 to model transactional systems and Web-based architectures. The model proposed last year is called session systems, and allows for the modeling of distributed systems in which agents collaborate within sessions. This model allows for specification of behaviors involving arbitrary numbers of agents and arbitrary number of sessions. We have shown that configurations of such systems can be represented as graphs and that upon the restriction that these graphs are decomposable into connected components of bounded size, some interesting security properties can be checked. We have considered business rules such as conflicts of interest, and Chinese wall properties. These results have been presented at ACSD 2014 in June (INDIA-FRANCE).

Task R3: Quantitative verification for distributed systems

R3: Two tracks have been followed this year. Concerning inferences in DBN, a new inference procedure based on conditional probability have been proposed: it allows to group nodes of the DBN in non-disjoint clusters, hence not having to assume independences between any of the node. An intern from INDIA (Ayush Maheshwari) spent two months in the summer 2014 thanks to the funding of ANR STOCH-MC we are leading. He started to implement the procedure. Experiments are conducted, and a PhD student (Matthieu Pichené) has just been hired (funded by ANR STOCH-MC and Region Bretagne) to pursue the research. Concerning Markov Chains, we are close to a characterization of those Markov Chains with a regular language, which allows for their easy analysis. Simply speaking, when all the eigen values of the Markov chains are roots of real, then the language is regular (INDIA-FRANCE-SINGAPORE).

Task R4: Unification of Control Theory of Distributed Systems

A new breakthrough has been made this year. A way to produce a controller for a distributed system is to express the constraints as an MSO formula on the tree of execution of the system. It is known that MSO is undecidable on grids, which distributed process can generate – hence we cannot hope for a general result. A 20 year old conjecture is that MSO is decidable for grid free architectures, that is on systems without two long sequences of events in parallel: if there is a long sequence of actions, only a limited number of actions can be in parallel with all of them. We are writing a paper bringing a solution to this problem, solving the controller synthesis for grid free distributed systems. (FRANCE-SINGAPORE-CHINA).

Task R2: Well-structure of Session systems over infinite sets of agents

The main result achieved is an extension of a session model proposed in 2011 to design transactional systems with infinite number of agents and sessions. Unfortunately, we had to set some restrictions to the considered model, in order to keep decidability of properties such as coverability of a configuration. Coverability is the basis for most of properties one would like to verify for transactional systems. In parallel, we have developed a simple logic to reason on runs (sequences of achievable configurations) of session systems. The logic allows for the specification of business rules such as conflicts of interest, but is also seem well suited to define security properties such as information flows.

Automatic realistic distributed synthesis of Systems

One reason for bugs in web-services is their distributed nature. These systems exhibit some complex and hard to intuit behaviors. It also makes them hard to analyze. A recent trend has thus been to synthesize these distributed systems automatically from a global (and thus easier to intuit) specification, such that the implemented system would be correct by construction. As a first step, we have chosen the standard model of asynchronous automata as model of distributed systems. In a publication accepted in 2013 (see publication page on this site), we highlighted properties to make them realistic (deterministic, no dead-end, truly distributed choice of actions and of initial and final states). We ave characterized the languages that can be automatically transformed into such a realistic distributed model, together with providing the algorithm to make the transformation. Finally, we conducted experiments to show the practicability of the transformation for a number of systems.

Task R3:Approximation of Markov Chains

This year, we have extended former results on approximate analysis of Markov Chains with a negative result: The symbolic Dynamic of a Markov Chain (the set of trajectories of distributions following a Markov chain) is not regular in general. For that, we developed a new proof technique using eigen values and vectors. We demonstrate this proof technique on a simple Markov Chain with rational coefficient on 3 states, which we prove not to have a regular symbolic dynamic. First, this justifies our use of approximation. Second, this gives ideas how to find a characterization of Markov Chains which have a regular set of symbolic dynamic.

Task R3: Statistical Analysis of Hybrid Stochastic Automata

Approximated analysis is not the only technique to handle large markovian models. Statistical techniques (Monte Carlo, etc) are also useful. Having both techniques is always beneficial (comparisons, better handling of many cases with the best technique for each particular case, etc). Both techniques rely on the correct definition of a measurable probability universe. For complex quantitative systems as hybrid stochastic systems, using continuous time, derivatives, probabilities and discrete transitions, this is not a simple task. We are in the process of defining an adequate measure on the universe of behaviors of hybrid stochastic systems, which will allow for statistical methods (hypothesis testing, etc.).

Task R4 : Logic and control:

We have embedded the framework of infinite two-player turn-based games played on graphs with safety objectives in an epistemic temporal logic. This embedding was made possible thanks to two intermediate embeddings: the first is from infinite games with safety objectives to supervisory control theory and the second is from supervisory control theory to epistemic temporal logic. Thereby, we are now able to determine whether a player has a winning strategy from a given state, and in that case we can elicit and synthesize a ll his winning strategies. The originality of our results stems from the fact that they are all formulated in terms of model checking problems in our epistemic temporal logic. Our reformulation of supervisory control theory and infinite game theory in epistemic temporal logic highlights their main underlying intuitions in terms of formal expressions involving the modalities of action, time and knowledge. We believe that our results pave the way for applying the model checking techniques to supervisory control theory and infinite games. This may ease the transfer of these theories towards practical applications. The work carried out in Task R4 is reported in a Research Report (avaialble on our publication page), and is currently under submission.