Associated team D.S.T : Research Themes

This associated team is a tripartite collaboration between two projects at INRIA Rennes (S4 & Distribcom), the National University of Singapore (NUS), and two institutes in Chennai (INDIA), the Chennai Mathematical Institute (CMI) and the Institute of Mathematical Sciences (IMS). The objective of the DST project is to study distributed systems, supervision and time issues with the help of concurrency models. The two main themes of the project are supervision, and quantitative/timed aspects of systems. The supervision theme will focus on distributed scheduling policies of distributed systems to ensure satisfaction of some properties (preservation of some bound on communication channels, for instance), diagnosis, and distributed control techniques. The second theme on time aspects of distributed systems will focus on the analysis of qualitative and quantitative properties of timed systems and models. The quantitative approaches will rely on network calculus applied to multimode Real Time Calculus, and the timed models studied during the collaboration will be inspired from timed scenarios. We expect some interactions between the two themes, that is improve timed characteristics (throughput, …) using supervision techniques, or conversely use some knowledge of time in a system to perform more accurate diagnosis and supervision.

Theme 1 : Supervision and Control

We want to address two main themes: the first one is supervisory control, i.e. calculus of a controller or a set of controllers supervising a system, so that the monitored system satisfies some given properties. The second one is scheduling, that is finding adequate order for the activation of autonomous component such that some objectives are always fulfilled.

Supervisory control : The idea in supervisory control is to guide a system so that it reaches a goal or stays in a legal set of behaviors. The technique used is to compute a machine (also called a controller) that can observe the system, and forbid some actions to its components. Control has been well studied since [RW89], but in a centralized setting, that is observation and control of the system is done by a single centralized controller. The new challenges are now to consider the problem in a distributed world, that is control a system via a set of local and independent controllers, each of them with a partial observation of the whole system. Distributed control has been shown undecidable in the general case [Tripakis01], but distributed solutions can be implemented, either with some restrictions to the architecture (allowed observations, controlled actions, etc), on the control objectives, or when distributed supervisors are allowed to communicate. Several objectives have been identified :

Distributed control with tagged messages: we propose to investigate the particular case of distributed control, where communication among distributed controllers can only take place whenever the system under control communicates (that is by piggy-backing some control information on the message of the system), and the control objective are the fair scheduling of a set of distinguished transitions of the plant and the boundedness of all communication buffers.
Distributed control with minimal messages: as already mentioned, distributed control is undecidable, but can find a solution when the distributed supervisors are allowed to communicate. However, these communications should not impose time penalties, or be too verbose if the communication network used between the supervisors is the same as the network used by the supervised system. Another research direction is then the development of distributed control and diagnosis synthesis techniques minimizing, for a given set of ultimately periodic trajectories, the amount of information that has to be exchanged between the supervisors. In particular, the paradigm of distributed games could be used to generate the controllers.
Control with true concurrency models: very often, control objectives are given under the form of a finite state machine, the main objective being to maintain the behaviors of a system (also given as a finite state machine) inside this regular description. The controllers are usually computed using complementation and products of the finite state machines. A challenging idea is to transpose this control problem to true concurrency models. A step in this direction was proposed for asynchronous transition systems in [MTY05]. One may for instance want to control a plant such that it stays in a MSC language, or conversely an MSC description (preferably a specification that can be implemented) so that it stays in some regular language. This involves at the same time some control and some scheduling among processes. Some work has been initiated on this topic by Laurie Ricker and Benoit Caillaud. However, these techniques will clearly have limitations, as specifications given under the form of Message Sequence Charts, for instance, are not regular languages, and hence products or complementations are not necessarily computable.
Distributed control with games: the distributed control problem can also be addressed using distributed games [WM03]. Two-player games consitute a useful theoretical tool for the study of centralized synthesis problems. Analogously, in the context of distributed synthesis, we can use the model of distributed games, or of games with imperfect information. However in general distributed games are neither determined nor algorithmically solvable. Restricting the modes of communications between players to obtain tractable subclasses of games is challenging and holds prospects for new questions in distributed control to be addressed.

Scheduling: Scheduling can be considered as a weakened version of supervisory control, and consists in specifying parts of a system separately, and ensure some good properties by activating processes in the system according to a given strategy. Controllers can forbid actions to reach a goal, scheduling policies can only postpone them. Good scheduling policies for distributed embedded applications are required to meet hard real time constraints and for optimizing the use of computational resources. We want to produce distributed scheduling policies, that is, scheduling should result from local monitors. In a recent work, [DGTY08], we have studied the quasi-static scheduling problem (QSS) in which (uncontrollable) control flow branchings can influence scheduling decisions at run time. By definition of QSS, this scheduling is given globaly. The QSS problem has been introduced by people from Cadence (Kondratyev et al.) to optimize circuits obtained from asynchronous specifications. The idea was that asynchronous specifications are easier to give, since they are compositional. However, some hard work has to be performed to turn automatically these specifications into circuits. The major lock is that without restriction, the asynchrony among components often leads to communication channels being unbounded, with the consequence that the system can not be implemented. One thus needs some smart policy in order to keep every choice of each device feasible, while keeping the channels bounded. The only parameter the implementation can play with is thus time: it cannot forbid actions, but it can postpone them. That is, what one is looking for is a scheduling policy. The abstract task model that we studied consists of a network of sequential processes that communicate via point-to-point buffers. In each round, a task is activated by a request from the environment. When the task has finished computing the required responses, it reaches a pre-determined configuration and is ready to receive a new request from the environment. For such systems, we have proved that determining existence of quasi-static scheduling policies is undecidable. However, the problem is decidable for the important sub-class of "data branching" systems in which control flow branchings are due exclusively to data-dependent internal choices made by the sequential components, and not because of choice between which channels to receive from. The challenge is now to restate the quasi-static scheduling problem as a local monitor problem. This would improve the solution in two ways. First, obtaining a scheduling policy guarantees that it can be implemented in a distributed way. Second, one might obtain decidability for all systems, and not only for data branching systems. It may seem paradoxical, since there are fewer systems which can be scheduled by distributed monitors than systems which are quasi static schedulable. However, those systems which are schedulable globally but not with distributed monitors seem to be the source of undecidability of QSS for general systems (ie non data branching).

Theme 2 : Time

The second theme addressed by the DST project is time in distributed systems. We want to address time from three points of view. The first one is the study of quantitative aspects, using techniques such as (Max,+) algebra, and the network calculus, for which both Distribcom and NUS have strong competences. The second aspect is the modelling power of timed model: several members of Distribcom and of CMI are very involved in research around Message Sequence Charts, a true concurrency model based on composition of partial orders. This model has been extended with time recently, and raises new challenges. The third aspect is the use of time as additional information for supervision.

· Quantitative aspects : an important aspect in the analysis of systems is the study of the worst-case bounds for their performances. Some performance oriented models such as Network Calculus have already been proposed for static analysis. Within this setting, a system is seen as interconnected servers that treat incoming requests according to a service policy. However, with this model, the parameters of a system never change: arrival and service policies of servers do not evolve with time. Some models where these parameters can change have been proposed, such as event count automata and multimode Real time calculus. Event-count automata count the number of events that can happen at each time. In each state, the number of events is lower and upper bounded. Transitions are conditioned to some guards on counters, and when a transition is fired, some counters can be reset. These models are equivalent to timed-automata, and hence their analysis can lead to state-space explosion. During the CASDS collaboration, we have studied an intermediate model called the "multimode Real Time Calculus": arrival processes obey to some Network Calculus constraints, but these constraints can change from time to time. This is modeled by two finite automata (an arrival automaton and a service automaton), whose states can change with transitions between states caused by different signals. In the arrival automaton, an arrival curve is associated to each state, as well as a time interval where the state can change. Moreover, transitions can be guarded by some predicates depending on the parameters of the systems (fill-level for example). The service automaton is defined similarly, with service functions. We have first tried to find some efficient ways of analysing these multimode systems. Two models can be efficiently analysed: when the arrival and service automata are synchronous (the automata change their state exactly at the same time) and when they are totally asynchronous (one can find an equivalent arrival curve and an equivalent service curve). We plan to continue the work on this kind of model, and extend the analysis to cases where automata are not purely synchronous or purely asynchronous, but rather a mix of both models. The solution to find efficient analysis techniques could be to mix the two approaches used in the synchronous and asynchronous cases.

· Timed concurrent models and their properties: We propose to study properties of timed concurrent models, and more precisely of timed scenarios. A recent extension that adds time constraints to Message Sequence Charts (MSCs) have been proposed [AMN07]. This new model also brings several new challenges. For instance, checking time constraints on timed MSCs is an undecidable problem in general, and a solution have been proposed for the class of regular MSC languages. An interesting challenge is to study if timed constraints checking applies to other MSCs outside this class. The difficulty is to find a way to verify these constraints over a regular set of representants. However, in the general case, unbounded MSCs with generic constraints can be used to encode two counter machines, leading to undecidability. Another question is whether the timing constraints imposed on an MSC make executions channel-bounded. In general, this question is also undecidable, but there could be a solution for a restricted class of constraints. Note that timed scenarios are seen as a starting point, but that several other true concurrency models might be studied, such as communicating automata, traces….

· Channels with losses : nowadays, MSCs only describe messages that are lost + found, or necessarily received. However, in realistic communication protocols, messages that arrive too late can also be declared obsolete. According to the MSC terminology, such messages are received. An interesting question is then to consider messages that are sent, and forgotten if not received in time. This model also differs from models with lossy channels, as losses here do not depend on a probability, but rather on time thresholds. Such model has never been proposed, but we have the intuition that this extension could be done using the extended MSCs of Martin Leucker [Leucker02].

· Timed diagnosis : So far, very few work address diagnosis with time [Chatain06]. By diagnosis, we mean the following problem. A distributed system is equipped by sensors (either material part or code instrumentation) that send some observations to a supervisor. These observations are collected to form a partial view of an execution of the system. The question addressed by diagnosis is, from a given observation O of the system and a model M, find every explanation of the observation compatible with O. Several approaches have been proposed, using automata or Petri nets as models. Thomas Chatain has proposed a technique based on Timed Petri nets unfoldings. In a recent work, we have proposed an untimed scenario-based approach [HGG06]. The interest of this approach is to compute a finite representation of all possible explanations for an observation under the form of a High-level MSC. An interesting extension to this work would be now to consider diagnosis from scenarios with time, that is use the information on the execution dates of some events in the observation and the time constraints in the scenario model to refine diagnosis.

In addition to these two main themes, we expect some cross-theme works. For instance, we are interested in supervision techniques that would allow to maintain a given quality of service. Using quantitative information on the model may also be useful to get more efficient algorithms for control and to have a more accurate view of the behaviors of the systems.