This year, we progressed objectives 1 and 2, and achieved two publications [BDGGG19, ABG19].

Axis 1: Timed Systems

We progressed our work on decidability of boundedness in Free choice timed Petri nets [AHP19]. The main objective of this work is to develop efficient verification algorithms for models of communicating timed systems. This work should lead to a publication in 2020.

During the internship of S. Mittal(summer 2019) and the visit of S. Akshay (September 2019) we have progressed our joint work on timed negotiations. Negotiations are a powerful formalism to describe transactions in distributed systems. In this model, processes are independent, but synchronize at nodes (negotiation tables) to take a common decision. An advantage of this model is that it allows for polynomial verification of several properties. We have extended the model with time, and considered polynomial verification techniques. This work led to a submitted paper [AGHM19].

In Oct. 2018, we initiated a new research topic on resilience of timed system (quantify the capacity of a system to return to a normal behavior after incidents or unexpected delays). We have progressed this work, and expect a publication in 2020 [AGH19].

K. Madnani (PhD, IITB) visited the SUMO team in May-July 2019. At this occasion, we started a line of research to quantify the impact of delay attacks on real-time systems [HKM19]. These attacks are man-in-the-middle attacks where intruders want to remain stealthy, but can postpone or cancel observations to break a system or reduce its efficiency. We proposed a model for these attacks and considered decidability of attack synthesis.

Axis 2: Control of Stochastic models

A work on uniform control of populations of finite state protocols initiated last year was accepted in a journal (LMCS) [BDGGG19]. The objective of this work is to define control strategies for sets of agents with similar randomized behavior in order to reach an objective, regardless of the number of agents. We have considered classification problems for partial observation of systems depicted by hidden Markov Models. The objective is to decide, for a given set of models, which system produced a partial observation. We showed conditions allowing for a classification in PTIME. This work is accepted at FSTTCS 2019 [ABG19].

Axis 1: Timed Systems

In Oct. 2018, we have initiated a new research topic on resilience of timed system (quantify the capacity of a system to return to a normal behavior after incidents or unexpected delays). The main objective of this work is to establish a formal framework to study the effects of delays on timed systems. In particular, one wants to know whether after a perturbation causing an unexpected delay, a timed system can return to a situation without delays. For timed automata, the problem can be considered as a timed language problem, i.e. ask whether every timed word depicting a perturbed execution has a suffix that corresponds to a suffix of a timed word in the original language. Unsuprisingly, this question is undecidable in general. However,if the questionconsiders timed executions instead of timed words, the problem becomes decidable. Providing efficient algorithmsto address resilience questionscould find applications for regulation of transport systems.

A extended version of a work on free choice timed Petri nets was accepted in the Journal of Logical and Algebraic Methods in Programming. This work considers a model for concurrent communicating systems with time. We have show that firability of a transition was a decidable question. The technique used for this proof can be reused to show that firability of a transition is robust to imprecision of clocks usd in a system. This technique has practical applications, and can be used to show that some instructions in distributed programs might not be reachable if time measurement is not accurate enough.

Axis 2: Control of Stochastic models

We have extended [AGV18] the typing approach of [Tiwari04] to control stochastic systems, and more precisely Markov Decision Processes (MDPs). The control problem is to keep a distribution of the MDPinside a safe polytope. Interestingly, we get an efficient polynomial time complexity to check whether there exists a distribution,from which there exists a controller keeping the MDP in the safe polytope. This is surprising as the same question starting from a given distribution is not known to be decidable, even if the controller is fixed. Also, we have a co-NP complexity for deciding whether for every initial distribution, there is controller keeping the MDP in the safe polytope. Finally, we showed that an alternative representation of the input polytope allows us to get a polynomial time algorithm for safety from all initial distributions.