Section: New Results

Automata, Games and Logics for Supervisory Control and System Synthesis

Participants : Philippe Darondeau, Bastien Maubert, Sophie Pinchinat.

Distributed Control of Discrete Event Systems: A First Step

To initiate a discussion on the modeling requirements for distributed control of discrete-event systems, a partially-automated region-based methodology is presented in [23] . The methodology is illustrated via a well-known example from distributed computing: the dining philosophers.

Enforcing Opacity of Regular Predicates on Modal Transition Systems

In [22] we considered the following problem: Given a labelled transition system $LTS$ partially observed by an attacker, and a regular predicate $Sec$ over the runs of $LTS$, enforcing opacity of the secret $Sec$ in $LTS$ means computing a supervisory controller $K$ such that an attacker who observes a run of $K/LTS$ cannot ascertain that the trace of this run belongs to $Sec$ based on the knowledge of $LTS$ and $K$. We then lifted the problem from a single labelled transition system $LTS$ to the class of all labelled transition systems specified by a modal transition system $MTS$. The lifted problem is to compute the maximally permissive controller $K$ such that $Sec$ is opaque in $K/LTS$ for every labelled transition system $LTS$ which is a model of $MTS$. The situations of the attacker and of the controller are dissymmetric: at run time, the attacker may fully know $LTS$ and $K$ whereas the controller knows only $MTS$ and the sequence of actions executed so far by the unknown $LTS$. We addressed the problem in two cases. Let ${\Sigma }_a$ denote the set of actions that can be observed by the attacker, and let ${\Sigma }_c$ and ${\Sigma }_o$ denote the sets of actions that can be controlled and observed by the controller, respectively. We provided optimal and regular controllers that enforce the opacity of regular secrets when ${\Sigma }_c\subseteq {\Sigma }_o\subseteq {\Sigma }_a=\Sigma$. We also provided optimal and regular controllers that enforce the opacity of regular upper-closed secrets ($Sec=Sec.{\Sigma }^{*}$) when ${\Sigma }_a\subseteq {\Sigma }_c\subseteq {\Sigma }_o=\Sigma$.

Analysis of partially observed recursive tile systems

The analysis of discrete event systems under partial observation is an important topic, with major applications such as the detection of information flow and the diagnosis of faulty behaviors. In [19] , we consider recursive tile systems, which are infinite systems generated by a finite collection of finite tiles, a simplified variant of deterministic graph grammars. Recursive tile systems are expressive enough to capture classical models of recursive systems, such as the pushdown systems and the recursive state machines. They are infinite-state in general and therefore standard powerset constructions for monitoring do not always apply. We exhibit computable conditions on recursive tile systems and present non-trivial constructions that yield effective computation of the monitors. We apply these results to the classic problems of opacity and diagnosability.

Uniform Strategies

In [29] , we consider turn-based game arenas for which we investigate uniformity properties of strategies. These properties involve bundles of plays, that arise from some semantical motive. Typically, we can represent constraints on allowed strategies, such as being observation-based. We propose a formal language to specify uniformity properties and demonstrate its relevance by rephrasing various known problems from the liter- ature. Note that the ability to correlate different plays cannot be achieved by any branching-time logic if not equipped with an additional modality, so-called R in this contribution. We also study an automated procedure to synthesize strategies subject to a uniformity property, which strictly extends exitsting results based on, say standard temporal logics. We exhibit a generic solution for the synthesis problem provided the bundles of plays rely on any binary relation definable by a finite state transducer. This solution yields a non-elementary procedure.

Emptiness Of Alternating Parity Tree Automata Using Games With Imperfect Information

In [30] , we focus on the emptiness problem for alternating parity tree automata. The usual technique to tackle this problem first removes alternation, going to non-determinism, and then checks emptiness by reduction to a two-player perfect-information parity game. In this note, we give an alternative roadmap to this problem by providing a direct reduction to the emptiness problem to solving an imperfect-information two-player parity game.

On timed alternating simulation for concurrent timed games

We address in [12] the problem of alternating simulation refinement for concurrent timed games (TG). We show that checking timed alternating simulation between TG is Exptime -complete, and provide a logical characterization of this preorder in terms of a meaningful fragment of a new logic, TAMTL${}^{*}$. TAMTL${}^{*}$ is an action-based timed extension of standard alternating-time temporal logic ATL${}^{*}$, which allows to quantify over strategies where the designated coalition of players is not responsible for blocking time. While for full TAMTL${}^{*}$, model-checking TG is undecidable, we show that for its fragment TAMTL, corresponding to the timed version of ATL, the problem is instead decidable and in Exptime .