Le séminaire en bref
Le séminaire 68NQRT est un séminaire commun de l'IRISA et d'Inria Rennes. Il a lieu le jeudi à 14 heures par défaut dans la salle Markov. Les thèmes du séminaire recouvrent des thèmes étudiés dans les départements « réseaux, télécommunication et services » et « langage et génie logiciel » de l'IRISA, ou des thèmes « Algorithmique, programmation, logiciels et architectures » et « Réseaux, systèmes et services, calcul distribué » d'Inria. On y trouve des exposés introductifs, avancés ou prospectifs dans les thèmes du génie logiciel, de l'informatique théorique, des mathématiques discrètes et de l'intelligence artificielle.D'après Mathematical Subject Classification:
|Q Theory of computing|
|R Discrete mathematics in relation to computer science|
|T Artificial intelligence|
jeudi 19 Janvier, 14h salle Aurigny
Optimal Assumptions for Synthesis
Controller synthesis is the process of constructing a correct system automatically from its specification. This often requires assumptions about the behaviour of the environment. It is difficult for the designer to identify the assumptions that ensures the existence of a correct controller, and doing so manually can lead to assumptions that are stronger than necessary. As a consequence the generated controllers are suboptimal in terms of generality and robustness. In this work, given a specification, we identify the weakest assumptions that ensures the existence of a controller. We also consider two important classes of assumptions: the ones that can be ensured by the environment and assumptions that speaks only about inputs of the systems. We show that optimal assumptions correspond to strongly winning strategies, admissible strategies and remorsefree strategies respectively. Based on this correspondence, we propose an algorithm for computing optimal assumptions that can be ensured by the environment.
Exposés des semaines suivantes
jeudi 26 janvier, 14h en salle Aurigny
Minimal probabilistic automata have to make irrational choices
In this talk, we answer the question of whether, given a probabilistic automaton (PA) with rational transition probabilities, there always exists a minimal equivalent PA that also has rational transition probabilities. The PA and its minimal equivalent PA accept all finite words with equal probabilities. We approach this problem by exhibiting a connection with a longstanding open question concerning nonnegative matrix factorization (NMF). NMF is the problem of decomposing a given nonnegative n×m matrix M into a product of a nonnegative n×d matrix W and a nonnegative d×m matrix H. In 1993 Cohen and Rothblum posed the problem of whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries. As a corollary we obtain a negative answer to the question on rationality of minimal probabilistic automata. This talk is based on two papers in ICALP 2016 and SODA 2017.
Mardi 31 janvier, Amphi. G, 8h45-17h15
Retransmission du séminaire Méthodes formelles du LAAS
Plus d'infos sur http://projects.laas.fr/IFSE/FMF/J7/
jeudi 9 février, 14h00
Attack Tree Analysis for Insider Threats on the IoT using Isabelle
We illustrate and classify insider threats in relation to the Internet of Things (IoT) exhibiting attack vectors for their characterisation. To model the attacks we apply a method of formal modeling of Insider Threats in the interactive theorem prover Isabelle. On the classified IoT attack examples, we show how this logical approach can be used to make the models more precise and to analyse the previously identified Insider IoT attacks using Isabelle attack trees.
jeudi 16 février, 14h00 salle Aurigny
Knowledge about the future in a strategic context
During last 10 years, several formalisms have been developed to express the capacity of agents to ensure the satisfaction of temporal properties in interaction contexts. These logics enable to write fine properties about the possible interactions between agents. Nevertheless, their relevance suffers from strong implicit assumptions about available informations for the modeled agents. On another hand, epistemic logics provide, through operator K, means to formalize the knowledge of agents. Non omniscience for an agent is characterized by her unability to distinguish between different possible states of the system. We build a logic that both enables the description of strategy contexts and integrates the agents knowledge, by use of operator K. Then we investigate the possibility of using this static characterization of knowledge for expressing the knowledge about temporal properties in a given strategy context.
jeudi 9 mars, 14h
Pierre-Yves Strub (To be confirmed)
To be Anounced
To Be Anounced
jeudi 30 mars, 14h
A counterexample to Thiagarajan's conjecture on regular event structures