Séminaires (2007-2014)

Seminaires du pôle MDSC
(Modèles Discrets pour les Systèmes Complexes)
du laboratoire I3S
Ces séminaires sont complémentaires aux séminaires de l'équipe MC3 et de l'équipe CeP

24 mars 2015, 14h00

Patricia Reynaud-Bouret (Laboratoire Dieudonné, Nice, http://math.unice.fr/~reynaudb/)

4eme minicours de l'axe MTC-NSC

Tests statistiques : ce que ça veut dire (informellement) et comment s'en servir en neurosciences
En neurosciences (et dans beaucoup d'autres domaines), les scientifiques se posent des questions fondamentales auxquelles on ne peut répondre que par oui ou non. Par exemple, le sujet fait-il deux fois la même chose ? les différents neurones qu'on peut enregistrer au cours de cette tàche se comportent-ils de manière indépendantes ou pas ?

Pour y répondre, ils réalisent une expérience dont le résultat est aléatoire. L'aléa peut être grand ou petit. Si il est trop grand, personne ne saura conclure. Si il est très faible, on pourra voir le résultat à l'oeil nu. Si il est modéré, il faut alors une procédure statistique bien définie : le test. Mais le statisticien effectuant un test ne peut répondre simplement oui ou non : il faut qu'il quantifie simultanément l'erreur commise dû à l'aléa. Certains de ces tests sont très populaires : test du chi-deux, test du student, test d'adéquation (plus connu sous son nom anglais de "goodness-of-fit").

De manière générale, que veut dire exactement un test statistique ? Comment quantifie-t-il l'erreur sur sa réponse ? Ce n'est qu'en comprenant ces enjeux que l'on peut éviter les pièges classiques lorsqu'on réalise par exemple plusieurs tests simultanément (tests multiples).

Tout cela sera illustré sur des situations concrètes provenant de l'analyse des séries de potentiels d'action (trains de spikes) : test d'égalité des taux de décharge, test d'indépendance des trains de spikes, tests d'adéquation à un modèle.

Tous les renseignements et les videos des minicours passent (dont celui de W. Stannat) sur http://mtc-nsc.unice.fr


4 mars 2014, 15h00

Hiroshi Hosobe (Hosei University, Japan, http://www.hosobe.org/)

Relationships of Constraint Hierarchies with Local Propagation and Semiring-Based Constraint Satisfaction Problems
Constraint hierarchies provide a framework for soft constraints. In this framework, constraints are associated with hierarchical preferences called strengths, and may be relaxed if they conflict with stronger constraints. In this talk, I will present two results of my research on constraint hierarchies. The first one is their relationship with local propagation algorithms, and the second one is their relationship with semiring-based constraint satisfaction problems. These results suggest what kinds of constraint hierarchies can be solved more efficiently than others.


14 mai 2013, 10h30

Maximilien Gadouleau (Durham University, UK, http://www.dur.ac.uk/m.r.gadouleau/)

Codage réseau, entropie des graphes et réseaux booléens
Le codage réseau est un mode novateur de transmission des données dans un réseau, où les noeuds intermédiaires combinent les paquets qu'ils reoivent. Le problème de résolubilité du codage réseau est très simple en essence: étant donné un réseau, peut-on transmettre tous les paquets en un minimum de temps ? Malheureusement, ce problème est très difficile en pratique et pour cela de nombreuses techniques ont été proposées, dont celle de l'entropie des graphes. Il se trouve que calculer l'entropie d'un graphe est similaire à la recherche du nombre maximal de points fixes de réseaux booléens. Nous allons étudier les relations entre ces trois problèmes. Aucune connaissance en codage réseau n'est pré-requise.


22 novembre 2012, 10h30

Mathilde Noual (I3S, UNSA, http://perso.ens-lyon.fr/mathilde.noual/)

Mise à jour de réseaux d'automates
Cet exposé propose de s'intéresser aux événements et aux ordonnancements d'événements se produisant au sein de réseaux d'éléments conceptuels prédéterminés. Dans ces réseaux, les éléments, appellés plutôt ``automates'', s'incitent les uns les autres à changer d'état en accord avec des règles prédéfinies qui, précisément, définissent le (fonctionnement du) réseau. Lorsqu'un automate se conforme effectivement aux influences qu'il reçoit de la part des autres, on dit que son état est mis à jour. Les événement élémentaires considérés sont les changements d'états des automates. Définir un mode de mise à jour pour l'ensemble des automates d'un réseau permet de sélectionner certains événements parmi l'ensemble de ceux qui sont a priori possibles. Cela permet aussi d'organiser et d'ordonner les événements les uns par rapport aux autres de façon, par exemple, à imposer que des événements indépendants se produisent simultanément ou simplement, de manière assez rapprochée pour qu'aucun autre événement ne puisse se produire pendant leur occurrence. Informellement, les modes de mise à jour peuvent donc être interprétés comme l'expression d'influences extérieures au réseau interdisant certains changements, ou alors comme la formalisation d'une version relâchée et relative de l'écoulement de temps. Dans cet exposé, je m'attacherai à préciser comment ceux-ci influent sur le comportement des réseaux en insistant sur leur relation à la structure d'un réseau.


5 septembre 2012, 11h00

Arnaud Liefooghe (Université Lille 1, LIFL, INRIA Lille-Nord Europe, https://sites.google.com/site/arnaudliefooghe/)

Métaheuristiques pour l'optimisation combinatoire multiobjectif
De nombreux problèmes d'optimisation sont caractérisés par des espaces de recherche vastes et complexes et de multiples fonctions objectif qui doivent être prises en compte simultanément. L'énumération exhaustive de l'ensemble Pareto optimal de tels problèmes d'optimisation combinatoire multiobjectif est généralement empêchée par deux raisons principales. Premièrement, le nombre de solutions Pareto optimales croît typiquement de façon exponentielle en fonction de la taille du problème. Deuxièmement, décider si une solution appartient à cet ensemble s'avère NP complet pour la plupart des problèmes d'optimisation combinatoire. Ainsi, on doit souvent se résoudre à une approximation. Pour cela, les approches heuristiques et métaheuristiques ont reçues un intérêt grandissant ces dernières années. Au cours de l'exposé, nous nous intéresserons aux étapes de conception et d'analyse de (méta)heuristiques pour l'optimisation combinatoire multiobjectif. Dans un second temps, nous insisterons sur la question de connexité entre les solutions Pareto optimales, en particulier pour plusieurs formulations du problème de sac-à-dos bi-objectif.


7 juin 2012, 14h00

Bernard P. Zeigler (Arizona Center for Integrative Modeling and Simulation, http://www.scs.org/zeigler)

Discrete Event System Specification environment modeling, computational basis for system theory
 


24 mai 2012, 14h00

Guillaume Beslon (INSA-Lyon, LIRIS, INRIA, IXXI, http://liris.cnrs.fr/guillaume.beslon/)

Simuler l'évolution pour comprendre la complexité des organismes biologiques
L'origine de la complexité des organismes biologiques reste une question ouverte en biologie. Une des difficultés de cette question est d'ordre méthodologique puisqu'elle est quasiment impossible à approcher de façon expérimentale et que la biologie est en du coup réduite à proposer des hypothèses évolutives sur la base de l'observation des organismes contemporains. Au cours de cet exposé nous montrerons comment la biologie computationnelle peut venir au secours de la biologie expérimentale en offrant la possibilité de faire évoluer des organismes numériques, d'observer leur complexification au cours de cette évolution et d'en déduire les lois qui président à cette complexification. Nous illustrerons ce propos par le modèle computationnel "aevol", développé au sein de l'équipe Beagle à Lyon pour étudier l'évolution de la structure des génomes bactériens (http://www.aevol.fr).


5 avril 2012, 14h00

Nadjib Lazaar (INRIA-Microsof Joint Center, http://www.irisa.fr/celtique/lazaar/)

Méthodologie et outil de Test, de localisation de fautes et de
correction automatique des programmes à contraintes

Le développement des langages de modélisation des programmes à contraintes a eu un grand impact dans le monde industriel. Des langages comme OPL (Optimization Programming Language) de IBM Ilog, Comet de Dynadec, Sicstus Prolog, Gecode, ainsi que d'autres, proposent des solutions robustes aux problèmes du monde réel. De plus, ces langages commencent à être utilisés dans des applications critiques comme la gestion et le contrôle du trafic aérien (Flener et al. ,07 ; Junker & Vidal, 08), le e-commerce (Holland & O'Sollivan, 05) et le développement de programmes critiques (Collavizza et al., 08 ; Gotlieb, 09). D'autre part, il est connu que tout processus de développement logiciel effectué dans un cadre industriel inclut impérativement une phase de test, de vérification formelle et/ou de validation. Par ailleurs, les langages de programmation par contraintes (PPC) ne connaissent pas d'innovations majeures en termes de vérification et de mise au point. Ceci ouvre la voie à des recherches orientées vers les aspects génie logiciel dédiés à la PPC. Notre travail vise à poser les jalons d'une théorie du test des programmes à contraintes pour fournir des outils conceptuels et des outils pratiques d'aide à cette vérification. Notre approche repose sur des hypothèses quant au développement et au raffinement dans un langage de PPC. Il est usuel de démarrer à partir d'un modèle simple et très déclaratif, une traduction fidèle de la spécification du problème, sans accorder un intèrêt à ses performances. Par la suite, ce modèle est raffiné par l'introduction de contraintes redondantes ou reformulées, l'utilisation de structures de données optimisées, de contraintes globales, de contraintes qui cassent les symétries, etc. Nous pensons que l'essentiel des fautes introduites est compris dans ce processus de raffinement. Le travail majeur présenté ici est la définition d'un cadre de test qui établit des règles de conformité entre le modéle initial déclaratif et le programme optimisé dédié à la résolution d'instances de grande taille. Par la suite, nous proposons un cadre conceptuel pour la mise-au-point de ce type de programmes avec une méthodologie pour la localisation et la correction automatique des fautes. Nous avons développé un environnement de test, nommé CPTEST, pour valider les solutions proposées, sur des problèmes académiques du monde de la PPC ainsi qu'un problème du monde réel qui est le problème d'ordonnancement des véhicules.


28 mars 2012, 14h00

Veronica Dahl (Simon Fraser University, http://www.cs.sfu.ca/~veronica/)

Enhancing Voting and Decision-Making Power
First we propose a computational model of Informed Advice based on Constraint Handling Rules (CHR), which can recommend decisions (e.g. which companies or mutual funds to invest in) consistent with a user's stated preferences, and explain the reasons for those recommendations. We argue that this model can promote more corporate social responsibility (CSR) by providing decision-makers with structured information systems that promote principled lines of thought. Second, again based on a user's stated preferences, we propose an algorithm to automatically generate voting recommendations on corporate proxy ballots. This stands to expand the pool of decision-makers to include those shareholders that are entitled to vote, but do not participate due to information overload or under-load. In the long run, we expect that helping investors to make decisions consistent to their values will make corporations more socially responsible.


15 mars 2012, 14h00

David Hill (Université Blaise Pascal, http://www.isima.fr/~hill/)

Simulation stochastiques discrètes et spatialisées -- Applications aux Sciences de la Vie et Calcul à Haute Performance.
Pour une meilleure compréhension de notre environnement, la modélisation et la simulation des systèmes naturels passent désormais par la prise en compte des effets « spatiaux ». Outre les soucis induits par un changement climatique, cet aspect spatial constitue un problème qui n'est pas toujours traité de manière simple par des modèles purement mathématiques. Nous présenterons plusieurs applications allant de la croissance forestière à l'océanographie, en montrant l'intérêt du couplage de simulations discrètes utilisant le hasard (des simulations stochastiques) avec des systèmes d'Information Géographique (SIG). Des techniques et des outils de simulation visuelle interactive seront présentés et une présentation avancée sera faite en ce qui concerne les techniques de distribution de flux stochastiques pour les applications nécessitant du calcul parallèle à haute performance.


8 mars 2012, 15h00

Sophie Demassey (École des Mines de Nantes, http://www.emn.fr/z-info/sdemasse/)

Constraints and Automata
On one hand, Constraint Programming (CP) is a paradigm merging technologies from artificial intelligence, operations research and graph theory, for solving hard combinatorial problems. The ultimate goal -- not achieved yet -- is to offer to the users high level interfaces and elementary modeling bricks to specify the problems, and self-optimizing algorithms to solve and analyze the problems. On the other hand, Finite Automata (FA) offer concise abstractions of some discrete systems, including protocols and languages, with a collection of algorithms to process them. Not surprisingly, FA have found their place in the CP toolbox.

In this presentation, we will first recall usages of FA in CP. We will then consider the specific decision property, called the consistency problem, that emerges from these usages and the different filtering algorithms that have been proposed for solving this problem for several language classes (regular, context-free, weighted-automata). We will finally focus on the successful application of automata-based constraints to employee timetabling problems.


2 décembre 2011, 14h00

Carito Guziolowski (Université d'Heidelberg, http://www.klinikum.uni-heidelberg.de/Guziolowski-Carito.115138.0.html)

Constraint-based modeling of complex biological networks
An influence graph is an abstraction of a biological network that represents the interactions among the molecules of a system as discrete influuences: signed and oriented edges. High-throughput measurements of this system can also be discretized into natural up- or down-regulations. The Sign Consistency Model (Siegel et al., 2006) is able to confront an influence graph with the discretized measures of its molecules, by representing both information as a system of qualitative constraints. Thus, the combinatorial complexity of reasoning over a large scale regulatory network can be approached by using efficient solvers over such a system of constraints. Currently, two computational frameworks, based on the Sign Consistency Model, exist: BioQuali (Guziolowski et al., 2009) and BioASP (Gebser et al., 2010). Both address and implement computationally complex queries confronting discrete regulatory networks with experimental data. In this talk I will present this method and its application to understand skin wound healing based on the signaling pathways of the Hepatocyte Growth Factor (HGF).


19 octobre 2011, 11h00

Thomas Hugel (Université de Nice-Sophia Antipolis, I3S, http://www.pratum.org/thomas-hugel/)

Mesurer la satisfaisabilité par des poids
Nous présenterons le phénomène de transition de phase dans les problèmes de satisfaction de contraintes (CSP). Le calcul de la valeur du seuil (dans 3-SAT notamment) résiste depuis une vingtaine d'années. En particulier, nous montrerons l'intérêt de la méthode du premier moment pour majorer le seuil. Pour l'utiliser il faut compter au moins 1 pour les formules satisfaisables. Pour obtenir la valeur exacte du seuil il faudrait compter exactement 1 pour les formules satisfaisables et 0 pour les formules non satisfaisables.

Il est difficile d'obtenir un comptage aussi précis, car obtenir les solutions d'une formule donnée est NP-difficile. La manière classique de mettre en oeuvre la méthode du premier moment consiste donc à partir d'une affectation et à repérer les formules dont elle est solution. À partir de là, il est possible de considérer le voisinage immédiat de la solution. En ordonnant localement les solutions, il est possible de compter uniquement les solutions minimales pour cet ordre.

Avec Boufkhad, nous avons développé en profondeur une approche nouvelle, de pondération, qui a ses origines dans les affectations partielles valides de Maneva, Mossel & Wainwright (2007). Chaque solution reçoit un poids (calculé en fonction de ses voisines) de telle sorte que la somme totale des poids fasse au moins 1 pour les formules satisfaisables.

Notre système de poids, basé sur des graines et des répartiteurs, permet de prendre en compte des CSP quelconques ; en outre, une variante nous a permis d'alléger les poids de Maneva et al. (tout en gardant une somme globale d'au moins 1).


7 avril 2011, 15h00

Hadrien Cambazard (University College Cork, Ireland, http://4c.ucc.ie/~hcambaza/index.html)

Méthodes hybrides intégrant la Programmation par Contraintes pour deux applications : portraits de dominos et ordonnancement de collimateurs multilames
Nous aborderons dans cet exposé deux applications dans les domaines de l'éducation et la santé (radiothérapie). Les algorithmes mis au point utilisent la propagation de contraintes dans des méthodes par recherche locale et génération de colonnes. Ils améliorent les meilleures approches connues pour ces problèmes.

Un portrait de dominos est une approximation d'une image réalisée à partir des dominos d'un nombre donné de boites. Ce problème fut posé la première fois en 1981 et des portraits de dominos ont été obtenus depuis par des techniques de programmation linéaire qui restent cependant très lentes et incapables de passer à l'échelle. Nous présenterons une nouvelle approche beaucoup plus performante reposant sur la résolution de flots à coût minimum identifiés comme le coeur du problème.

L'ordonnancement de collimateurs multilames est un problème important pour un traitement efficace du cancer par radiothérapie. Nous présenterons une formulation originale du problème comme un problème de plus court chemin dans un cas restreint. Nous développons sur cette idée de nouveaux modèles linéaires et par contraintes propageant des plus courts chemins.


8 mars 2011, 11h00

Joëlle Despeyroux (INRIA-Sophia, http://www-sop.inria.fr/members/Joelle.Despeyroux/)

Premiers pas vers un "logical framework" pour la biologie cellulaire

Travail en collaboration avec Kaustuv Chaudhuri (INRIA-Saclay)
Parmi les approches qui ont obtenu un grand succès jusqu'ici, dans la modélisation et l'analyse des processus biochimiques au sein de la cellule, on note, pour l'aspect modélisation des processus, l'utilisation de langages plus ou moins dédiés, comme le pi-calcul stochastique, la machine abstraite biochimique "biocham" ou le calcul kappa. Le raisonnement sur les modèles ainsi obtenus utilise la logique temporelle pour raisonner, non directement sur ces modèles, mais sur un ensemble de traces d'exécution de programmes dans les langages choisis; les traces étant obtenues par simulation.

Nous proposons une approche connexe, mais plus unifiée: une logique ayant vocation à devenir un "logical framework" pour les systèmes biologiques, i.e. une logique permettant à la fois la modélisation et la preuve de propriétés de ces systèmes. Notre logique est une extension modale de la logique linéaire, appellée "logique linéaire hybride" ("Hyll"). La logique linéaire nous permet de spécifier les systèmes de réactions biochimiques en les voyant comme des systèmes de transitions. Les contraintes (temporelles, stochastiques, etc...) sur les transitions de ces systèmes sont spécifiées à l'aide de connecteurs "hybrides" permettant de nommer le monde courant ou d'exprimer le fait qu'une propriété est vraie dans un certain monde -le monde le plus simple utilisé étant le temps. Le cœur de Hyll est une logique ayant les propriétés requises pour pouvoir prétendre au titre de "logical framework": présentation en déduction naturelle et en séquents, avec l'élimination des coupures, des règles focales, etc (nous n'aborderons pas ces derniers points dans l'exposé).

De manière plus prospective, les preuves de propriétés des systèmes ainsi modélisés seront naturellement formalisées par des arbres de preuves (complets ou partiels) de hyll. La construction et la manipulation de ces preuves est envisageable à moyen ou long terme. Les exemples traités jusqu'ici ne sont que des exemples jouets, permettant d'illustrer la méthode proposée. Le volet "travaux futurs" contient de nombreux autres points...


4 mars 2011, 14h30

Elisabetta De Maria (INRIA-Rocquencourt, http://users.dimi.uniud.it/~elisabetta.demaria/)

Méthodes Formelles de la Logique pour la Prédiction de la Structure des Protéines, la Comparaison de Séquences et le Couplage de Modéles

Les méthodes formelles de l'Informatique sont de plus en plus appliquées à l'étude des problèmes biologiques. Dans la littérature, elles sont utilisées d'une manière extensive pour modeler et simuler des systèmes biologiques et pour exprimer des propriétés formelles de ces systèmes. Dans l'exposé je montrerai comment le model checking, la théorie des jeux et la combinaison de techniques de logique temporelle et d'apprentissage de paramètres peuvent être exploités pour développer des solutions effectives à trois classes importantes de problèmes biologiques: les problèmes du repliement et de la prédiction de la structure des protéines, le problème de la comparaison des séquences et les problèmes du couplage des modèles biologiques et de la validation du modèle résultant.

Pour ce qui concerne les problèmes du repliement et de la prédiction de la structure des protéines, nous modelons l'espace des conformations des protéines comme un système de transition fini dont les états sont toutes les conformations possibles d'une protéine et dont les transitions représentent les transformations admissibles entre conformations. Puis, nous montrons comment exprimer des propriétés intéressantes de ce système de transition avec la logique temporelle et nous utilisons la machinerie du model checking pour les vérifier automatiquement. En ce qui concerne le problème de la comparaison des séquences biologiques, nous modelons des séquences biologiques comme des structures étiquetées avec une relation d' "ordre limité" et nous définissons un critère qui permet de mesurer leur degré de similarité en fonction du nombre de tours manquants dans un jeu d'Ehrenfeucht-Fraïssé au premier ordre joué sur ces structures.

Enfin, pour ce qui est du dernier problème, nous étudions le couplage de différents modèles qui jouent un rôle dans le cycle cellulaire des mammifères et dans les thérapies du cancer. Nous montrons comment la formalisation d'observations expérimentales en logique temporelle avec contraintes numériques peut être utilisé pour valider automatiquement un modèle couplé et optimiser des paramètres inconnus par rapport aux données expérimentales. Nous illustrons cette approche basée sur les contraintes par le couplage de modèles biochimiques existants du cycle cellulaire des mammifères, de l'horloge circadienne, du système de réparation de l'ADN p53/Mdm2 et du métabolisme de l'irinotecan.


3 mars 2011, 15h00

Antoine Rollet (LaBRI, Bordeaux, http://www.labri.fr/perso/rollet/)

Un cadre formel pour la modélisation et le test de systèmes réactifs à flots de données avec contraintes de temps

Dans cet exposé, nous allons étudier comment modéliser et tester certains systèmes critiques à flot de données. Pour cela, nous allons présenter le modèle des Variable Driven Timed Automata (VDTA) qui a été développé pour ce genre de systèmes: un modèle à flot de données et temps dense. Nous allons aussi voir comment transcrire les méthodes de génération de test plus classiques (à base d'ioLTS) vers ce modèle, en définissant une nouvelle relation de conformité, en utilisant une approche à la volée (non déterministe), ou une approche par objectif de test.


14 décembre 2010, 11h00

Eric Goubault & Sylvie Putot (CEA)

Analyse statique dans les nombres flottants, et l'outil FLUCTUAT

Dans cette deuxième partie, nous présenterons la manière d'étendre l'analyse sur-approximée par méthodes zonotopiques exposée précédemment, à l'analyse de programmes manipulant des nombres en précision finie, et en particulier, dans les nombres flottants. Ce domaine d'interprétation abstraite permet également de déterminer la perte de précision quand on passe d'une sémantique réelle a une sémantique flottante, ainsi que les principales causes de cette perte. Ceci est implémente dans l'outil FLUCTUAT, qui sera présenté en cours d'exposé.


13 décembre 2010, 11h00

Eric Goubault & Sylvie Putot (CEA)

Analyse statique sur et sous-approximée dans les nombres réels

On présentera une analyse par interprétation abstraite de programmes impératifs, qui permet de déterminer précisément et efficacement des relations d'entrée sortie entre les valeurs numériques (réelles) des variables d'un programme. Cette analyse est basée sur les formes affines (ou zonotopes) et peut-être définie pour déterminer des sur-approximations, ainsi que des sous-approximations de ces relations et donc des valeurs des variables. Ceci est a la base de l'analyse faite dans l'outil FLUCTUAT, présentée dans un deuxième exposé.


19 Novembre 2010, 16h00

Laurent Trilling (IMAG-LSR, Université Grenoble I, http://www-lsr.imag.fr/users/Laurent.Trilling/)

Analyse déclarative de réseaux logiques de régulation génique basée sur la programmation logique non-monotone ASP (Answer Set Programming)

L'approche "déclarative" en modélisation consiste à formaliser toutes les connaissances disponibles pour aboutir par transformations automatiques à une représentation intentionnelle de tous les modèles cohérents, à l'opposé de l'approche classique qui procède par construction manuelle d'un seul modèle initial et modifications empiriques s'il est incohérent. Nous présenterons un outil pour analyser avec cette approche les réseaux de régulation discrets proposés par R. Thomas. Il offre plusieurs fonctionnalités, dont la vérification et la réparation d'incohérence, l'inférence automatique de propriétés et l'optimisation de modèles. Il utilise la nouvelle technologie de programmation logique ASP qui repose sur une logique non monotone, bien adaptée au cas d'informations incomplètes. Cet aspect est illustré par la notion de "défaut", tel que en général tout oiseau vole, sauf s'il s'agit d'un pingouin. Si seul l'axiome titi est un oiseau caractérise titi, alors titi vole est déductible. Mais si titi est un pingouin est aussi déductible, alors titi vole ne l'est plus. Nous montrerons comment décrire de cette façon des hypothèses biologiques vraies en général, comme les contraintes dites "d'additivité". Au l'aide de requêtes nous illustrerons d'autres avantages d'ASP, dont des capacités d'inférence de propriétés supplémentaires par rapport à la logique classique (modèles minimaux), un pouvoir d'expression supérieur à celui de la programmation logique classique (contraintes CTL), une méthodologie de révision de connaissance sans rupture des théories et des performances du même ordre que celles des solveurs SAT sans pénalisation en termes de facilité d'écriture.


1er Juillet 2010, 10h30

Patrick Amar (LRI, Université Paris Sud, http://www.lri.fr/~pa/)

Modélisation de l'auto-assemblage et du comportement de complexes macro-moléculaires

De nombreuses voies métaboliques dans les cellules mettent en évidence des réactions catalysées par des protéines (fonction enzymatique). Dans les expériences faites 'in vitro' le milieu est homogène et le volume considérablement plus grand que dans une cellule, on doit mettre de grandes quantités de réactifs pour obtenir la concentration nécessaire à l'établissement des réactions chimiques. A contrario dans une cellule, la quantité de réactifs est bien plus faible et bien que le volume soit lui aussi réduit, la concentration est trop basse pour que certaines réactions puissent avoir lieu. L'idée est que les concentrations locales sont suffisamment élevées pour les réactions se fassent.

Pour modéliser le fonctionnement de ces voies métaboliques 'in vivo' les systèmes continus à base d'équations différentielles ne sont pas bien adaptés: dans certains processus cellulaires un très petit nombre de molécules est mis en jeu et consécutivement les facteurs stochastiques sont très importants.

On a donc opté pour un modèle discret au niveau macromoléculaire (de l'ordre de grandeur d'une protéine) de type entité-centré. La cellule est représentée par un volume limité par une membrane qui contient le nombre de molécules des réactifs de la voie métabolique étudiée correspondant à ce qui existe réellement dans une cellule vivante. La cellule simulée peut contenir des compartiments, et le milieu n'est pas forcément homogène (la viscosité peut être fonction de la localisation spatiale). Le simulateur prend en entrée un fichier décrivant les réactifs: type, vitesse nominale de diffusion, etc. et les réactions: formation de complexes, échange de groupes (phospohrylation et déphospohrylation par exemple), ainsi que la cinétique de ces réactions. En cours de fonctionnement, le simulateur produit à la fois un affichage 3D de la cellule et de son contenu, en reconnaissant et affichant les complexes (agrégats de macromolécules) avec leur localisation dans la cellule, et un affichage sous forme de courbes de l'évolution des concentrations des divers produits. Un histogramme du nombre et de la taille des complexes est aussi affiché.

Le simulateur est hybride en ce sens que l'on peut choisir de représenter certaines espèces chimiques soit par des entités localisées soit par une population homogène dans un compartiment. L'intéret étant de pouvoir intégrer les très petites molécules présentes en très grand nombre et réparties de façon homogène dans le compartiment avec un faible cout en temps calcul.

L'accent est particulièrement porté sur l'étude des complexes car il est montré que les réactions peuvent être plus efficaces de plusieurs ordres de grandeur avec les chaînes enzymatiques agrégées et des réactions canalisées plutot que par libre diffusion. Cela pourrait expliquer pourquoi in-vivo certaines voies métaboliques fonctionnent avec une faible concentration de réactifs.

Des exemples de modèles de types très différents seront présentés à la fin de l'exposé pour montrer la diversité des utilisations possibles du simulateur.


29 Avril 2010, 10h00

Heike Siebert (Université libre de Berlin, http://page.mi.fu-berlin.de/hsiebert/)

Modules of Discrete Dynamical Systems

Analyzing complex networks is a difficult task, regardless of the chosen modeling formalism. For discrete models, even if the number of network components is in some manageable, we have to face the problem of analyzing dynamics in an exponentially larger state space. A well-known idea to approach this difficulty is to identify smaller building blocks of the system the study of which in isolation still renders information on the dynamics of the whole network. In this talk, we propose and illustrate an analysis approach utilizing network modularity for systems modeled with the logical formalism of R. Thomas.


28 Avril 2010, 14h00

Elisabetta de Maria (INRIA - Rocquencourt, Projet CONTRAINTES, http://users.dimi.uniud.it/~elisabetta.demaria/)

Computer Science Logic for Structure Prediction, String Comparison, and Model Coupling

Formal methods of Computer Science are more and more applied to the study of biological issues. In literature, they are extensively used to model and simulate biological systems and to express formal properties of such systems. In the talk I'll show how model checking, game theory, and the combination of temporal logic and parameter learning techniques can be exploited to develop effective solutions to three relevant classes of biological problems: the protein structure prediction and protein folding problems, the sequence comparison problems, and the problems of coupling biological models and validating the resulting model.

As for the protein structure prediction and protein folding problems, we model the space of protein conformations as a finite transition system whose states are all the possible conformations of a protein and whose transitions represent admissible transformations of conformations. Then, we show how meaningful properties of such a transition system can be expressed in temporal logic and we use the model checking machinery to algorithmically check them.

As for the sequence comparison problems, we model biological sequences as labeled structures with a limited order relation and we define a criterion which allows one to measure their degree of similarity in terms of the number of remaining rounds in an Ehrenfeucht-Fraissé game played on such structures.

Finally, as for the last issue is concerned, we study the coupling of different models playing a role in the mammalian cell cycle and in cancer therapies. We show how the formalization of experimental observations in temporal logic with numerical constraints can be used to automatically validate a coupled model and optimize unknown parameter values with respect to experimental data. We illustrate this constraint-based approach to computing with partial information, through the coupling of existing biochemical models of the mammalian cell cycle, the circadian clock, the p53/Mdm2 DNA-damage repair system, and irinotecan metabolism.


12 Février 2010, 13h00

Lisandru Muzy (Università di Corsica Pasquale Paoli, http://msdl.cs.mcgill.ca/people/muzy)

Determination of optimal structures of systems for the achievement of behaviors, in a fluctuant environment

Une réflexion est menée sur la mise au point d'algorithmes stochastiques pour l'automatisation de la sélection de composants, de leur couplage, de leur paramétrisation et de leur processus de composants. La recherche de l'espace des solutions est guidée par l'activité des composants, c'est-à-dire leur participation ou pas à des solutions satisfaisantes. Une caractéristique fondamentale de ce travail est la recherche de ''trade-off'' structurels globaux, évolutionnistes, sous la contrainte d'un environnement changeant. Un composant solution sera donc adapté à un environnement et pas à un autre. Celui-ci ne fera pas forcément localement ''le meilleur choix.'' Néanmoins, la population des composants sera adaptée aux changements d'environnement. Une analogie forte existe avec la variation de l'expression génétique des organismes, appellée plasticité phénotypique, en réponse à un environnement changeant. L'ensemble de l'approche vise à constituer un cadre de modélisation et de simulation opérationnel et réutilisable.


29 Janvier 2010, 13h30

Hadrien Jeanne (Université de Rouen)

Caractérisation des langages rationnels binaires géométriques

Les langages géométriques ont été introduits pour la première fois dans le cadre de la validation temporelle des applications temps-réel. Classiquement, cette validation peut se faire selon deux modèles, un basé sur les langages rationnels, et un sur la géométrie discrète. Les langages géométriques se présentent comme un lien entre ces deux modèles. Le cas rationnel est particuliérement intéressant au vu de son implémentation, ce qui a motivé la recherche d'un algorithme efficace. Nous avons donc développé un algorithme polynomial permettant de déterminer si un langage rationnel binaire est géométrique. Nous présentons dans cet exposé le cas des langages prolongeables.


2 Décembre à 2009; 14h00

Lakhdar Saïs (http://www.cril.univ-artois.fr/~sais/)

Beyond classical clause learning

In this talk we present several contributions to Conflict Driven Clause Learning (CDCL), which is one of the key components of modern SAT solvers. First, we propose an extended notion of implication graph containing additional arcs, called inverse arcs. These are obtained by taking into account the satisfied clauses of the formula, which are usually ignored by conflict analysis. Secondly, we present an original adaptation of conflict analysis for dynamic clauses subsumption. Our last contribution demonstrates that clause learning can be exploited at each step of the search process, even if a conflict do not occurs. This last contribution aims to derive new but more powerful reasons leading to the implication of a given literal. For all these contributions, we discuss their possible integration to modern SAT solvers.


13 Novembre 2009 à 14h00

Morgan Magnin (École centrale de Nantes, Laboratoire IRCCyN, équipe MOVES, http://www.irccyn.ec-nantes.fr/~magnin/)

Modèles pour l'inférence des paramètres temporels et stochastiques des réseaux de régulation biologiques

Cet exposé se situe dans le cadre de l'analyse des réseaux de régulation biologiques. Ces systèmes d'une grande complexité nécessitent d'être abstraits sous la forme d'un modèle mathématique pour être étudiés. Les modèles résultants font généralement intervenir un grand nombre de variables (correspondant à des seuils d'activation ou d'inhibition d'un gène, ou représentant des temps de franchissement de ces seuils, etc.) qui sont considérées comme des paramètres car leurs valeurs ne sont pas connues précisément, mais indirectement (relations entre des paramètres, plages de valeur, variations suivant certaines lois de probabilités,...).

L'originalité de notre approche réside dans la prise en compte des aspects temporels dans les modélisations grâce, notamment, au recours au pi-calcul stochastique [1] (et notamment au framework que nous avons introduit : le process hitting [2]). Étant donnée une observation expérimentale sur le système réel, notre objectif est de l'exprimer sous la forme d'une propriété dans une logique appropriée et de vérifier que le modèle la satisfait. Nous nous intéressons ici au problème d'inférence des paramètres temporels, c'est-à-dire la recherche de valeurs de paramètres satisfaisant un ensemble de propriétés données.

De manière plus prospective, nous cherchons actuellement à établir la complémentarité des modèles exprimés en process hitting et de ceux proposés sous la forme d'autres modèles, à l'instar des réseaux de Petri (notamment leurs extensions temporelles et/ou paramétriques). Nous justifierons cette approche en présentant les principaux résultats que nous avons obtenus pour la vérification de propriétés temporelles exprimées en logique TCTL sur des réseaux de Petri à chronomètres [3].

[1] Corrado Priami. Stochastic Pi-Calculus. The Computer Journal, 38(7) :578-589, 1995. [2] Loïc Paulevé, Morgan Magnin, and Olivier Roux. Refiningg Dynamics of Gene Regulatory Networks in a Stochastic pi-Calculus Framework. Research Report hal-00397235, June 2009. [3] Morgan Magnin, Didier Lime, and Olivier (H.) Roux. Symbolic state space of stopwatch Petri nets with discrete-time semantics. In The 29th International Conference on Application and Theory of Petri Nets and other models of concurrency (ICATPN 2008), volume 5062 of Lecture Notes in Computer Science, pages 307-326, Xi'an, China, June 2008. Springer.


6 Novembre 2009 à 14h00

Claude Le Pape

Problèmes d'optimisations dans le domaine de l'énergie

The conjunction of high energy costs and environmental concerns suggests both the definition of new classes of optimization problems and, most often, the extension of well-known problems through the introduction of multi-scales approaches and additional optimization criteria such as the total amount of energy used in the accomplishment of a set of functions, the cost of this energy, the corresponding carbon footprint, etc. Although in many cases simple measures are sufficient to trigger significant progress, the effective definition of operational optimization problems is key to setting goals, searching for solutions, and evaluating progress, in a wide variety of domains, such as the design of complex systems, planning and scheduling with peak-smoothing incentives, real-time control of efficient trade-offs between energy consumption and user comfort, etc. Beyond these operational (and somewhat local) concerns, global perspectives on the evolution of energy production and consumption at national and international levels are necessary to direct research and development toward the resolution of the most important problems. For example, the MARKAL model, developed over a period of almost two decades by the Energy Technology Systems Analysis Programme (ETSAP) of the International Energy Agency, can be used to evaluate the potential impact of measures aimed at reducing carbon dioxide emissions. Interestingly enough, such a model can be applied to all sorts of operational energy optimization solutions, provided estimates on the cost and impact of these solutions are available, as exemplified by the recent application (by Schneider Electric and Ecole des Mines de Paris) of MARKAL to expected results of the HOMES collaborative project on energy efficiency solutions for building and residential markets. (Common work with Vincent Mazauric and academic partners)

Bio: Claude Le Pape is in Schneider Electric in charge of coordinating the evaluation of new technologies, the recognition of research and development experts, and the management of research and development partnerships. He received a PhD in Computer Science from University Paris XI and a Management Degree from "College des Ingénieurs" in 1988. From 1989 to 2007, he was successively postdoctoral student at Stanford University, consultant and software developer at ILOG S.A., senior researcher at Bouygues S.A., and R&D team leader at Bouygues Telecom and ILOG S.A. He participated to several European research projects and to the development of many optimization software tools and industrial applications in various domains, including mixture design, inventory management, long-term personnel planning, construction site scheduling, and manufacturing scheduling.


16 Avril 2009 à 14h30

Sihem Mesnager (Département de Mathématiques, Université Paris VIII et XIII LAGA (Laboratoire Analyse, Géométrie et Applications), équipe MTII ( Mathématiques pour le Traitement de l'Information et de l'Image ), web)

Nouvelle classe de fonctions courbes en représentation polynomiale

Une fonction Booléenne est dite courbe si sa non-linéarité est maximale. Cela correspond à être à distance maximale pour la distance de Hamming de l'ensemble des fonctions booléennes affines, ou encore le code de Reed-Muller d'ordre 1. Les fonctions courbes n'existent qu'en dimension paire. Elles ont été largement étudiées en raison de leurs propriétés algébriques et combinatoires intéressantes ainsi qu'en en raison de leurs multiples applications et jouent un rôle important en cryptographie ainsi qu'en théorie des codes.

Classifier les fonctions courbes semblant sans espoir à ce jour, il a été proposé dans la littérature de nombreuses constructions de fonctions courbes définies sur le corps de Galois à 2^n éléments (n pair). Les constructions proposées sont principalement des fonctions courbes monomiales (c'est a dire dont l'expression est une la trace sur le corps fini à 2^n éléments d'une fonction puissance) . On ne connait que tres peu d'exemples de fonctions courbes non monomiales.

Dans cet exposé, je rappellerai d'abord l'importance des fonctions courbes en cryptographie symétrique et je présenterai l'état de l'art du domaine . Ensuite, je donnerai des résultats nouveaux à savoir une nouvelle famille infinie de fonctions courbes non monomiale (de degré algébrique optimal) définies sur le corps fini a 2^n éléments dont l'expression est la somme d'une trace sur le corps fini à 2^n éléments d'une fonction puissance d'exposant de Dillon (à savoir 2^{n/2}-1) et d'une fonction trace sur le corps fini à 4 éléments d'une fonction puissance dont l'exposant est ( 2^n-1)/3. Plus précisément, j'expliquerai que l'étude du caractère "courbe" d'une fonction de telle famille dépend de la parité de n/2 et je donnerai une caractérisation explicite pour le caractère "courbe" en termes de sommes de Kloosterman en s'appuyant sur les resulats récents de Charpin, Helleseth et Zinoviev sur les sommes de Kloosterman et les sommes cubiques.


9 Avril 2009 à 14h30

Laurent Vuillon (LAMA, Chambéry, web)

Combinatoire des mots et conjecture de Fraenkel

Ce séminaire donnera les liens entre un problème de recouvrement des entiers et la combinatoire des mots afin d'étudier la conjecture de Fraenkel. Cette conjecture a été formulée dans le cadre de la théorie des nombres il y a maintenant plus de 30 ans. Elle prétend que pour k > 2 entier fixé, il y a une unique façon de recouvrir les entiers par $k$ suites de Beatty avec des fréquences deux à deux distinctes. Ce problème peut être exprimé en termes de combinatoire des mots de la façon suivante : pour un alphabet à k lettres, il existe une unique suite équilibrée avec des fréquences de lettres deux à deux distinctes qui est exactement la suite de Fraenkel notée $(F r_k )^omega$ où F r_k = F r_{k’¡Ý1} k F r_{k’¡Ý1}, avec F r_3 = 1213121. Cette conjecture est prouvée pour k = 3, 4, 5, 6 d'après les travaux de Altman, Gaujal, Hordijk et Tijdeman ainsi que dans d'autres cas particuliers. Dans ce séminaire, nous présenterons donc une synthèse sur ce sujet et la résolution de la conjecture dans un cas particulier.


13 Mars 2009 à 10h30

Gabriele Fici (Dipartimento di Informaticae Applicazioni, University of Salerno, http://www.dia.unisa.it/dottorandi/fici/)

Combinatoire des mots et structures de données

Il existe beaucoup de structures de données pour représenter un texte. Dans la recherche de motifs on utilise largement l'automate des suffixes, c.à.d. l'automate déterministe minimal qui accepte les suffixes d'un mot. On se pose le problème de relier la structure de l'automate des suffixes d'un mot aux propriétés combinatoires du mot. Par exemple on sait que la classe des mots binaires dont l'automate des suffixes est de complexité minimale coïncide avec la classe des préfixes des mots sturmiens standards. Dans cet exposé on s'occupera des propriétés combinatoires des mots qui peuvent être lues sur le graphe de l'automate des suffixes, et, symétriquement, on verra comment ce graphe est déterminé par certains paramètres combinatoires du mot.


19 février 2009 à 15h30

Michael Weiss (FISLAB, Univ. Milano Bicocca)

Pavages, universalité et calculs

La notion de pavage du plan est présente dans de nombreuses disciplines, dont les mathématiques, la physique, la chimie ou encore l'informatique. Le modèle utilisé ici est basé sur des carrés de taille unitaire dont les bords sont colorés. Deux tuiles peuvent s'assembler si leur côté commun ont la même couleur. Malgré sa simplicité, ce modèle peut simuler n'importe quelles autres notions de pavage du plan et depuis Berger en 64, nous savons que ce modèle peut aussi simuler du calcul Turing. Notre approche des pavages se fait donc d'un point de vue calculabilité en essayant d'établir des outils forts de calculabilité propres aux pavages et ainsi comprendre mieux le calcul qui se développe dans les structures naturelles géométriques. Nous nous intéresserons entre autres à deux notions de bases: dans un premier temps nous définirons les outils nous permettant d'obtenir des notions d'universalités propres aux pavages, et dans un deuxième temps, nous établirons un équivalent au théorème classique du point fixe de Kleene pour les pavages, et nous montrerons ses applications.


13 février 2009 à 14h

Sylvain Sené (INSA-Lyon,Laboratoire LIRIS, Équipe Turing, http://perso.ens-lyon.fr/sylvain.sene/)

Robustesse environnementale dans les réseaux de régulation: théorie et application en biologie.

Nous allons nous intéresser à l'influence des conditions de bords dans les réseaux d'automates booléens à seuil, objets mathématiques utilisés pour la modélisation des réseaux de régulation biologique. L'objectif est de montrer que les bords (qui peuvent représenter des potentiels électriques externes dans les réseaux de neurones et des flux d'hormones ou encore des micro-ARN dans les réseaux de régulation génétique) sont des éléments qui peuvent changer radicalement le comportement dynamique de tels réseaux, aussi bien dans le cas de réseaux théoriques tels que les automates cellulaires que dans celui des réseaux biologiques réels. La démarche scientifique proposée est de se focaliser dans un premier temps sur des réseaux dits "parfaits", énormément contraints sur la nature des interactions et la topologie de manière à obtenir des résultats théoriques sur Z^d. Ensuite, en relâchant progressivement les contraintes, nous mettrons en évidence, par simulation, des domaines d'influence des conditions de bord pour des réseaux plus complexes sur Z^2. Enfin, pour faire un pas de plus en direction de la biologie, nous verrons que les conditions de bord jouent un rôle dans les réseaux réels. Nous présenterons alors une méthode générique d'étude de la robustesse environnementale des systèmes dynamiques réels (basée sur la notion de bassin d'attraction). Nous terminerons en présentant les résultats que cette méthode permet d'obtenir, dans le contexte des réseaux de régulation génétique, à propos de la morphogenèse florale de la plante Arabidopsis thaliana.


12 février 2009 à 15h

Marion Le Gonidec (Université de Liège)

Mots infinis et ensembles d'entiers reconnus par automates dénombrables

Dans cet exposé, nous introduisons une classe de mots infinis engendrés par des automates dénombrables. Nous présentons des résultats structurels et des résultats de complexité pour cette famille. L'étude de ces mots nous a également amené à nous intéresser à la structure des ensembles d'entiers engendrés par automates finis ou dénombrables. Nous introduirons 2 familles distinctes de tels ensembles d'entiers. Les résultats obtenus sur ces familles mettront en lumière des phénomènes spécifiques au cas fini ou qui s'étendent (plus ou moins bien) au cas dénombrable.


20 novembre 2008 à 14h

Janine Guespin-Michel (Université de Rouen)

Le point de vue de la complexité en biologie

Etudier les organismes vivants comme des systèmes complexes, c'est adopter un point de vue dynamique qui a ses avantages et ses exigences. Cette thèse sera illustrée par des exemples simples.


21 octobre 2008 à 1h

Frederic Havet (INRIA Sophia Antipolis, Projet MASCOTTE, http://www-sop.inria.fr/sloop/personnel/Frederic.Havet/)

Graphes orientés n-universels

Il existe de nombreux rapports entre les orientations et colorations d'un graphes. Un des premières est le théorème de Gallai-Roy (1967) qui établit que tout graphe orienté de nombre chromatique n contient un chemin direct (tous les arcs dans le même sens) de longueur au moins n-1. De manière plus générale, on peut se demander quels sont les graphes orientés n-universels c'est-à-dire contenus dans tous les graphes orientés n-chromatiques. Nous ferons un survol des résultats et conjectures concernant ces graphes.


16 mai 2008 à 14h

Madalena Chaves (INRIA Sophia Antipolis, Projet COMORE, http://www-sop.inria.fr/comore/Personnel/Madalena.Chaves/ )

Boolean models and piecewise linear systems for robustness analysis of genetic networks

Boolean models provide a good description of the network structure of a system, but do not give much information on its temporal dynamics. Introducing asynchronous updates or using piecewise linear systems it is possible to analyze various questions related to the robustness of the system with respect to fluctuations in the environment. As an example, Drosophila's segment polarity network and its expression patterns will be studied.


18 avril 2008

Eric Goles (Université Adolfo Ibanez, Santiago, Chili / Institute for Complex Systems, Cerro Artilleria, Chili)

Comparaison de la dynamique des réseaux booléens sur différents modes d'itération

Étant donné un réseau booléen fini, on choisit un mode d'actualisation du réseau: synchrone, séquentiel, par bloques, etc. Il est clair que les points fixes sont invariants vis à vis du mode d'itération, mais ce n'est pas pareil pour les cycles. On va présenter des résultats qui permettent de mieux comprendre l'apparition (ou la disparition) des cycles, et aussi la notion de "filtre" qui permet, étant donné un réseau initial qui a au moins un point fixe, d'obtenir un réseau avec les mêmes points fixes mais sans aucun cycle. Ce type de résultat est intéressant pour la modélisation des réseaux d'interaction génétique.


13 mars 2008

Christian Michel (Equipe de Bioinformatique Théorique du Laboratoire LSIIT, CNRS et Université Louis Pasteur de Strasbourg, http://dpt-info.u-strasbg.fr/~michel/ )

Codes circulaires dans les gènes

La recherche d'un code circulaire dans les gènes est un problème biologique qui a été posé il y a plus de 50 ans. Le concept de comma-free code (code circulaire particulier) a été introduit par Crick et al. en 1957 pour expliquer comment la lecture d'une suite de nucléotides de 3 en 3 pouvait coder les 20 acides aminés constituant les protéines. Les 2 problèmes posés étaient: comment associer un codon (trinucléotide en phase de lecture) par acide aminé et comment choisir la phase de lecture ? La solution pour trouver ces 20 codons consistait à exclure les codons AAA, CCC, GGG, TTT auxquels une phase unique ne peut pas être associée, et à grouper les 60 codons restants en 20 classes de 3 codons obtenus par permutation circulaire. Cependant, le choix d'un tel ensemble de 20 codons qui aurait cette propriété de retrouver automatiquement et localement la phase de lecture, était infaisable en raison de la combinatoire explosive (3^20 soit environ 3.5 milliards de choix possibles). De plus, les découvertes que le codon TTT (un codon exclu dans un comma-free code) code la phénylalanine (Nirenberg et Matthaei, 1961) et que les gènes commencent par le même codon ATG, ont conduit à abandonner le concept de comma-free code.

De façon tout à faite inattendue, nous avons identifié plusieurs codes circulaires dans les gènes de divers génomes. Ainsi, les gènes seraient composés de 2 types codes: des codes génétiques, le plus important étant le code génétique universel, pour traduire les codons en acides aminés et des codes circulaires pour retrouver les phases de lecture des gènes.

Dans cet exposé, nous présentons les principaux résultats obtenus depuis plus d'une dizaine d'années sur ces codes dans les gènes: définitions, méthodes d'identification (automate à pétales), méthodes statistiques de recherche de codes dans les gènes, propriétés en biologie (phase de lecture et gènes à décalage), propriétés en évolution (modèles stochastiques d'évolution linéaire et non-linéaire) et propriétés en théorie des codes (concept de collier identifiant des hiérarchies dans les codes).


12 février 2008

Adrien Richard (Laboratoire I3S, CNRS et Université de Nice-Sophia Antipolis, http://www.i3s.unice.fr/~richard/ )

Circuits positifs et nombre maximum de points fixes dans les réseaux booléens

On représente la structure des réseaux booléens par un graphe d'interaction: les sommets sont les composantes du réseau, et il y a un arc positif (négatif) d'une composante à une autre si la première active (inhibe) la seconde. On donne ensuite une borne sur le nombre de points fixes qui ne dépend que des circuits positifs présents dans le graphe d'interaction (un circuit est positif s'il contient un nombre pair d'inhibitions). Pour établir cette borne, on utilise une version booléenne de la conjecture de Thomas démontrée par Remy: la présence d'un circuit positif est nécessaire pour le présence de plusieurs états stables. Une extension de la borne au cas multivalué est évoquée.


14 janvier 2008

Luigi Liquori (INRIA Nice-Sophia Antipolis, http://www-sop.inria.fr/members/Luigi.Liquori/index.html )

Logical Networks: Toward foundation for Self-organizing Overlay Networks and Programmable Overlay Computing Systems, joint work with Michel Cosnard.

We propose logical networks as the foundations for programmable overlay networks and overlay computing systems. Such overlays are built over a large number of distributed computational agents, virtually organized in colonies, and ruled by a leader (broker) who is elected democratically (vox populi) or imposed by system administrators (vox dei). Every individual asks the broker to log in the colony by declaring the resources that can be offered (with variable guarantees). Once logged in, an individual can ask the broker for other resources. Colonies can recursively be considered as evolved agents who can log in an outermost colony governed by another super-leader. Communications and routing intra-colonies goes through a broker-2-broker PKI-based negotiation. Every broker routes intra- and inter- service requests by filtering its resource routing table, and then forwarding the request first inside its colony, and second outside, via the proper super-leader (thus applying an endogenous-first-estrogen-last strategy). Theoretically, queries are formulae in first-order logic equipped with a small program used to orchestrate and synchronize atomic formulae. When the client individual receives notification of all (or part of) the requested resources, then the real resource exchange is performed directly by the server(s) individuals, without any further mediation of the broker, in a pure peer-to-peer fashion. The proposed overlay promotes an intermittent participation in the colony, since peers can appear, disappear, and organize themselves dynamically. This implies that the routing process may lead to failures, because some individuals have quit, or are temporarily unavailable, or they were logged out manu militari by the broker due to their poor performance or greediness. We aim to design, validate through simulation, and implement these foundations in a programmable overlay network computer system, called ARIGATONI.

http://www-sop.inria.fr/mascotte/Luigi.Liquori/ARIGATONI/index.html


13 décembre 2007

Jean-François Couchot (Université de Franche-Compté, http://lifc.univ-fcomte.fr/~couchot )

Efficiently dealing with SMT-LIB provers in software verification

Polymorphism has become a common way of designing short and reusable programs. Such a convenience is valuable in logic as well. However, top shelf automated theorem provers such as SMT-LIB ones do not handle polymorphism. To this end, in the first part of the talk, I'll present a reduction of polymorphism in many-sorted first order logics.

Nevertheless, the approach is not efficient enough when applied on verifying absence of threat in industrial C programs: it remains some Verification Conditions (VCs) that cannot be decided by any SMT-LIB prover, mainly due to their size. In the second part of the talk, I'll present a strategy to select relevant hypotheses in each VC. The relevance of an hypothesis is the combination of separated dependency analysis obtained by some graph traversals.

Corresponding implementations are presented in the framework of the Why/Caduceus toolkit. Approaches are applied on benchmark containing one industrial program from Dassault Aviation.


28 novembre 2007

Gabriel Fici (Laboratoire I3S, UMR6070 du CNRS, Université de Nice-Sophia Antipolis)

Marked Systems and Circular Splicing

Splicing systems are generative devices of formal languages, introduced by Head in 1987 to model biological phenomena on linear and circular DNA molecules. We introduce a special class of finite circular splicing systems named marked systems. We prove that a marked system S generates a regular circular language if and only if S satisfies a special (decidable) property. As a consequence, we show that we can decide whether a regular circular language is generated by a marked system and we characterize the structure of these regular languages.