Logo IRISA logo Inria

Prochain Exposé

jeudi 18 janvier, 14h en salle Minquiers

Engel Lefaucheux

Probabilistic Disclosure: Maximisation vs. Minimisation.

We consider opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret, the ε-disclosure variant corresponding to the execution being secret with probability greater than 1 − ε. In a probabilistic and non deterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). We address quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) related to both forms of disclosure for a fixed or finite horizon. For all problems, we characterise their decidability status and their complexity. We discover a surprising asymmetry: on the one hand optimal strategies may be chosen among deterministic ones in maximisation problems, while it is not the case for minimisation. On the other hand, for the questions addressed here, more minimisation problems than maximisation ones are decidable.

Exposés des semaines suivantes

jeudi 25 janvier, 14h en salle Minquiers

Francois Schwarzentruber

Knowledge-Based Policies for Qualitative Decentralized POMDPs

Qualitative Decentralized Partially Observable Markov Decision Problems (QDec-POMDPs) constitute a very general class of decision problems. They involve multiple agents, decentralized execution, sequential decision, partial observability, and uncertainty. Typically, joint policies, which prescribe to each agent an action to take depending on its full history of (local) actions and observations, are huge, which makes it difficult to store them onboard, at execution time, and also hampers the computation of joint plans.
We propose and investigate a new representation for joint policies in QDec-POMDPs, which we call Multi-Agent Knowledge-Based Programs (MAKBPs), and which uses epistemic logic for compactly representing conditions on histories. Contrary to standard representations, executing an MAKBP requires reasoning at execution time, but we show that MAKBPs can be exponentially more succinct than any reactive representation.

jeudi 1er fevrier, 14h en salle Minquiers

Nicolas Markey

Variations on the semantics of Strategy Logic

Several extensions of the temporal logic ATL have been defined and studied over the last 10 years in order to express non-zero-sum properties of multiple-player games played on graphs. Strategy Logic (SL) is a prominent example in which strategies are handled explicitly: SL allows to quantify over strategies, to assign them to players, and to express LTL properties over the resulting plays. This makes the logic very expressive, but was proved to preserve decidability of model checking. After presenting the classical setting of Strategy Logic, I will introduce natural variations on the semantics of SL, and show how they impact its expressiveness and model-checking algorithms. This talk is based on joint works with Patricia Bouyer, Patrick Gardy, and François Laroussinie.

jeudi 8 fevrier, 14h en salle Minquiers

Alain Girault

Dynamic Speed Scaling Minimizing Expected Energy Consumption for Real-Time Tasks

Ce travail propose d’utiliser la technique des processus de décision markovien (PDM) pour calculer la politique optimale en-ligne de choix de vitesses afin de minimiser l’énergie consommée par un processeur exécutant un ensemble de tâches avec des contraintes temps-réel. La politique est calculée avant l’exécution du système temps réel (hors ligne), mais utilisée en ligne. Cette méthode est efficace et proche de la solution optimale hors-ligne et elle est plus performante que les solutions en-ligne qui ne prennent pas en compte les informations statistiques sur les tâches futures.

jeudi 15 fevrier, 14h en salle Minquiers

Antoine Girard

Timing contracts for embedded control systems

Physical systems equipped with embedded controllers are becoming pervasive (smart buildings, intelligent cars, drones, robots, etc.), thus increasing the need for high-confidence analysis and design tools that are able to handle tight interactions between the physical and digital worlds. In this context, contract-based approaches have been identified as a promising direction for cyber-physical systems design. For instance, for embedded controller implementation, timing contract specify the constraints on the time instants at which certain operations are performed such as sampling, actuation or computation. Under such contracts, the control engineers are responsible for designing a control law that is robust to all possible timing variation specified in the contract while the software engineers can focus on implementing the proposed control law so as to satisfy the timing contract. In this talk, we propose techniques that are useful within this framework. In the first part of the talk, we will consider the problem of stability verification: given models of the physical plant and of the controller and a timing contract, verify that the resulting dynamical system is stable. We propose an approach based on the notion of reachable set, and which builds on efficient over-approximation algorithms developed over the past decade. We then tackle the problem of timing contract synthesis: given models of the physical plant and of the controller, determine a set of timing contracts that guarantee stability of the resulting system. In the second part of the talk, will consider the problem of schedulability: given several controllers, each with a timing contract, to be implemented on a common computational platform, synthesize a dynamic scheduler allocating the shared computational resources, which guarantees that the timing contracts of all controllers are satisfied. We propose an approach based on timed games, whose solution provides a suitable schedule.

jeudi 22 fevrier, 14h en salle Minquiers

Serge Haddad

Réseaux de Petri discrets et continus : apports réciproques

Dans les années 80, les réseaux de Petri continus (RdPC) ont été introduits d'une part pour remédier à l'explosion combinatoire des réseaux de Petri discrets (RdP) et d'autre part pour modéliser le comportement de systèmes physiques dont l'état est spécifié par des variables continues. Depuis cette époque, différents travaux ont établi que la complexité de la vérification de propriétés comportementales se réduit en passant du modèle discret au modèle continu. Cet exposé consistera en trois parties. Tout d'abord je détaillerai un algorithme polynomial pour l'accessibilité dans les RdPC et survolerai les autres algorithmes polynomiaux pour RdPC. Je montrerai aussi que l'accessibilité est PTIME-complète tandis que l'absence de blocage est coNP-complète. J'étudierai ensuite l'application de ces procédures au problème de couverture des RdP. La couverture est particulièrement appropriée à l'étude de programmes concurrents à mémoire partagée. Cependant sa complexité élevée (EXPSPACE-complète) limite son utilisation pour des problèmes de taille industrielle. Aussi je développerai une nouvelle approche appliquant la couverture des RdPC comme méthode d'élagage d'un algorithme de couverture en arrière. Le point crucial est ici un codage efficace de l'algorithme polynomial en une formule d'un SMT solveur. Finalement je montrerai que ce codage peut aussi être appliqué au problème d'inclusion d'ensembles d'accessibilité de RdPC réduisant ainsi la complexité de EXPTIME à coNP. J'établirai aussi que cette procédure est optimale, i.e. le problème est coNP-complet.

Séminaire autour des thèmes 68NQRT