Laboratoire d'Informatique, Signaux et Systèmes de Sophia Antipolis

Lauréat catégorie recherche

DNA storage suffers from deletion, insertion, and substitution errors that may affect the sequence of nucleotides during synthesis, sequencing, and storage. Dealing with these errors is one of the main challenges in DNA storage since their presence can be detrimental to the reliability of the system. For instance, DNA sequencing often results in multiple erroneous reads of the data. Current approaches for recovering the data rely on multiple sequence alignment methods that are solely based on heuristics and do not scale well beyond small proof-of-principle experiments. Alternatively, reconstructing the data in question can be cast in the setting of trace reconstruction, which is a well-studied problem in computer science. In this talk, as a first step towards adapting trace reconstruction schemes to DNA storage, we present an efficient novel trace reconstruction scheme that provides robustness against deletions through coding-theoretic and algorithmic techniques.

These results will be presented during a seminar given on April 6th at 14h in the Conference Room (I3S-007) by Dr. Serge Kas Hanna, Senior Researcher at Aalto University.

Latin squares and hypercubes have a wide range of applications in statistics, cryptography and coding theory. In this talk, we review a construction of Latin squares based on cellular automata (CA) that was introduced by Mariot, Formenti and Leporati at AUTOMATA 2016, and we generalize it to the case of Latin hypercubes of dimension k > 2. We first show a characterization of Latin cubes generated by bipermutive CA with linear rules, where the central coefficients define an invertible Toeplitz matrix. Next, for dimension k > 3 we prove that linear bipermutive CA generating Latin hypercubes are defined by sets of invertible Toeplitz matrices with partially overlapping coefficients. In particular, we remark that the overlap relation can be described by a specific kind of regular de Bruijn graph, which allows to count and enumerate all linear CA rules generating Latin Hypercubes.

1. Pourquoi la cybersécurité des véhicules est devenue un sujet d'actualité
2. Comment pouvons-nous relever le défi
3. Prochaines étapes, recherches en cours

L'apprentissage de clauses, dans le domaine du raisonnement par contrainte, a fait des progrès très importants au cours des deux dernières décennies. C'est un composant bien connu des solveurs SAT modernes, qui est également devenu un sujet de grand intérêt pour la mise en œuvre de solveurs CP robustes. Parmi les techniques fructueuses, qui se sont révélées efficaces sur une variété de problèmes, nous trouvons l'enregistrement de nogoods (généralisés), lazy clause generation (LCG) et l'apprentissage non clausal. Jusqu'à présent, les résultats pratiques les plus probants ont été obtenus en mettant en œuvre des procédures spécifiques en fonction de la nature des contraintes (par exemple, différentes manières d'expliquer les contraintes globales dans LCG, ou diverses règles permettant de déduire des contraintes de conflit dans l'inférence non clausale).

Dans ce séminaire, nous allons dans un premier temps discuter des cœurs modernes de solveurs CP puis nous revisitons l’apprentissage de clauses pour CSP, en exploitant quelques idées intéressantes introduites dans la littérature (telles que l’enregistrement de g-nogood, LCG et l’analyse de conflits dans le contexte de graphes) ainsi que leur efficacité au sein du solveur NACRE et proposons de nouvelles techniques génériques afin de rendre l’apprentissage par clause non intrusif et efficace pour CSP.

We present a type-based analysis to ensure memory safety and object protocol completion in a Java-like language. The analysis prevents not only null pointer dereferencing and memory leaks, but also that the intended usage protocol of each object is respected and completed.

Modern society is increasingly dependent on large-scale software systems that are distributed, collaborative, and communication-centred. To verify software products for such systems, we have to make sure that the modelling languages exactly capture the system requirements on that its implementation relies. For this purpose we present synchronisation patterns that capture different degrees of synchrony in interactions and allow to classify the expressive power of modelling languages. With that we can identify process calculi (or other formalisms) that do not contain any synchronisation mechanisms and are fully distributed, we can identify hidden (and unexpected) kinds of synchronisation, and we can analyse the degree of synchronisation that can be expressed by a language.

Separation logic is an extension of Hoare’s proof system which supports a local way of reasoning about programs that mutate memory. This talk starts with a short introduction on Hoare's calculus. We then discuss why this formalism lacks modularity and switch our attention to propositional separation logic (Reynolds, LICS'02). We take this opportunity to revisit one major result on propositional separation logic (Lozes, SPACE'04) and then briefly explain how it can be extended to a logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. The satisfiability problem of this logic is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard (Mansutti, FSTTCS'18).

SAT est le premier problème à avoir été montré NP-Complet, ce qui lui procure une place particulière d’un point de vue théorique. Néanmoins, ce problème qui consiste à vérifier la satisfaisabilité d’une formule de la logique propositionnelle, est surtout populaire de part ses applications pratique (vérification formelle, planification, …). L’engouement pour ce langage vient du fait de l'avènement de solveur très efficace permettant de résoudre des problèmes contenant des millions de variables et de clauses, ce qui permet d’attaquer des problèmes industriels. Cette efficacité a largement été éprouvée puisqu’il n’est pas rare que pour résoudre un problème NP-Complet la démarche qui est usitée consiste bien souvent à transformer ce problème en SAT (CSP, Argumentation Abstraite, ...). Les dernières avancées réalisées dans le cadre de la résolution pratique du problème SAT ont rejailli bien au delà de ses frontières. Ainsi, à l’heure actuelle, de nombreux problèmes dont la classe de complexité est supérieure à NP peuvent être traités de manière pratique (QBF, Logique Modal, …). Pour la plupart, leur résolution consiste à appeler un solveur SAT sur plusieurs instances analogues. Ce type de résolution, appelé résolution incrémentale de SAT, est en passe de devenir l’état de l’art dans bien des domaines. Ainsi, il devient nécessaire de concevoir les nouveaux démonstrateurs SAT afin de prendre en considération ce nouveau paradigme d’utilisation. Une application qui tire largement avantage de l’utilisation typique des démonstrateurs SAT incrémentaux est la recherche de noyaux (coeurs) minimaux inconsistants (MUS). Ici nous présenterons l’état de l’art des approches permettant l’extraction de tels ensembles et en quoi il est important de considérer des solveurs dédiés à cette tâche.

An introduction to process algebra and session types

We prove that the generating function of a language accepted by a one-way deterministic one-reversal counter machine without negative cycles is holonomic. The result is achieved by solving a particular case of a conjecture that states that LDFCM is included in RCM. Here, RCM is a class of languages that has been recently introduced and that admits some interesting properties, namely it contains only some particular languages with holonomic generating function.

We study the problem of efficiently computing journeys in timetable
networks (i.e. public transport).
We present the CSA algorithm as well as the CSAccel which is an
accelerated version of the CSA using a multi-level geographical
partitioning (multi-level overlay graphs).
CSA is a non graph based algorithm that boasts the best performance for
solving the earliest arrival and profile problems in timetable networks.
It uses only the smallest elements of the timetable network, a
connection, and manages to efficiently answer queries made by users.
It is in use in multiple cities (Antibes, Grasse, ...) as well as
multiple massive networks (Nouvelle-Aquitaine, ...) by the company
Instant System.
Because the algorithm is used in real time by a multitude of users
decreasing query times thereby reducing the server load is something all
companies wish for.
At the cost of preproccesing we can use the CSAccel, it can reduce query
times by up to a factor of 5-6 compared to the CSA by partitioning the
graph and only using a portion of the connections.
But the preprocessing doesn't allow frequent updates of the connections,
which is a problem when using real time data, and the specific
partitioning doesn't allow a use in purely urban graphs.

Within a decade, the use of SAT related technologies moved from a confidential interest among specialists to a popular tool for solving discrete combinatorial problems. Improvements in the practical resolution of SAT is driven by applications: Bounded Model Checking in Electronic Design Automation has been a major component for the success of SAT engines for solving "real" combinatorial problems at the end of the 90s, Bioinformatic and Software engineering are currently two areas where SAT engines receive a lot of interest.
In this talk, we will focus on the theory behind modern SAT solvers tailored to solve "real" combinatorial problems, and discuss their application to the bounded model checking problem. The talk will introduce the generic SAT engine architecture used in all the so-called "CDCL SAT solvers" inherited from the original MiniSAT (www.minisat.se) and see how its development has been driven by the Bounded Model Checking problem.

Computation over floating-point numbers induces errors due to rounding. Those errors are at the root of many problems, such as the precision or the stability of computation. Numerous works, which are based on an overestimation of actual errors, try to address similar issues. However, they do not provide critical information to reason on those errors, for example, by computing input values that exercise a given error.
We introduce a new constraint solver aimed at analysing the round-off errors that occur in floating-point computations. Such a solver allows reasoning on round-off errors by means of constraints on ranges of error values. This new solver is built by incorporating in a solver for constraints over the floating-point numbers the domain of errors which is dual to the domain of values. Both domains, the domain of values and the domain of errors, are associated with each variable of the problem. Additionally, we introduce projection functions that filter these domains as well as the mechanisms required for the analysis of errors.

La PPC permet de formaliser et résoudre des problèmes fortement combinatoires, dont le temps de calcul évolue en pratique exponentiellement. Les méthodes développées aujourd'hui résolvent efficacement de nombreux problèmes industriels de grande taille dans des solveurs génériques. Cependant, les solveurs restent dédiés à un seul type de variables : réelles ou entières, et résoudre des problèmes mixtes discrets-continus suppose des transformations ad hoc. Dans un autre domaine, l'IntAbs permet de prouver des propriétés sur des programmes, en étudiant une abstraction de leur sémantique concrète, constituée des traces des variables au cours d'une exécution. Plusieurs représentations de ces abstractions, appelées domaines abstraits, ont été proposées. Traitées de façon générique dans les analyseurs, elles peuvent mélanger les types entiers, réels et booléens, ou encore représenter des relations entre variables. En partant du constat qu'en PPC et en IntAbs, des sur-approximations d'un ensemble désiré sont calculées, la notion de domaines abstraits en IntAbs a été redéfinie en PPC afin de construire une méthode de résolution traitant indifféremment les entiers et les réels. Cette généralisation permet d'intégrer à la PPC des domaines relationnels, comme les octogones déjà utilisés en IntAbs. En exploitant l'information spécifique aux octogones pour guider la recherche de solutions, de bonnes performances on été obtenues sur les problèmes continus. Dans un deuxième temps, une méthode générique de résolution de contraintes a été définie avec des outils d'IntAbs, afin d'intégrer les domaines abstraits existants. Le prototype, AbSolute, peut ainsi résoudre des problèmes mixtes et utiliser les domaines relationnels implémentés.
 

Partial singleton weak path-consistency is essential for tackling challenging fundamental reasoning problems associated with qualitative constraints networks. Briefly put, partial singleton weak path-consistency ensures that each base relation of each of the constraints of a qualitative constraint network can define a singleton relation in its corresponding partially weakly path-consistent subnetwork. In this talk, we propose a stronger local consistency that couples partial singleton weak path-consistency with the idea of collectively deleting certain unfeasible base relations by exploiting singleton checks. We then propose an algorithm for enforcing this new consistency and a lazy variant of that algorithm for approximating the new consistency, both of which outperform the respective algorithm for enforcing partial singleton weak path-consistency in a given qualitative constraint network . With respect to the lazy algorithmic variant in particular, we show that it runs up to 5 times faster than our original exhaustive algorithm whilst exhibiting very similar pruning capability. We formally prove certain properties of our new local consistency and our algorithms, and motivate their usefulness through demonstrative examples and a thorough experimental evaluation with random qualitative constraint networks of the Interval Algebra and the Region Connection Calculus from the phase transition region of two different generation models. Finally, we provide evidence of the crucial role of the new consistency in tackling the minimal labeling problem of a qualitative constraint network, which is the problem of finding the strongest implied constraints of that network.
 

Introduction à l'interpretation abstraite

Introduction au working group et présentation de langages à pile visible

Formal verification has become increasingly important because of the kinds of guarantees
that it can provide for software systems. Verification of models of biological and medical
systems is a promising application of formal verification. Human neural networks have
recently been emulated and studied as a biological system. Some recent research has been
done on modelling some crucial neuronal circuits and using model checking techniques to
verify their temporal properties. In large case studies, model checkers often cannot prove
the given property at the desired level of generality. In this paper, we provide a model using
the Coq proof assistant and prove properties concerning the dynamic behavior of some
basic neuronal structures. Understanding the behavior of these modules is crucial because
they constitute the elementary bricks of bigger neuronal circuits. By using a proof assistant,
we guarantee that the properties are true for any input values, any length of input, and
any amount of time. With such a model, there is the potential to detect inactive regions of the
human brain and to treat mental disorders. Furthermore, our approach can be generalized to the
verification of other kinds of networks, such as regulatory, metabolic, or environmental networks.

Disponibles sur la page de l’école : http://univ-cotedazur.fr/events/ecole-de-cybersecurite

Résumes disponibles à la page:
https://www.i3s.unice.fr/fr/node/519

• 14h : Présentation du projet, J.-C Régin
• 14h15 : Adaptable Processes, C. De Giusto.
• 14h45 : A Logical Framework for Systems Biology and Biomedicine, J. Despeyroux.
• 15h15 pause café.
• 15h45 : Modeling and Verifying Dynamic Properties of Biological Neural Networks in Coq, E. De Maria.
• 16h20 : Synchronisabilité de Machines à Etats Communicantes, L. Laversa.
• 16h40 : Weighted Circuit Constraint, N. Isoart.
• 17h00 : Notions essentielles en Optimisation Multicritère, S. Dersarkissian.

This talk concerns formal models for the analysis of communication-centric software systems with declarative and reactive behaviors. We focus on session-based concurrency, the interaction model induced by session types, which uses (variants of) the pi-calculus as specification languages. While well-established, such process models are not expressive enough to specify declarative and reactive behaviors common in emerging communication-centric software systems. Here we propose the synchronous reactive programming paradigm (SRP) as a uniform foundation for session-based concurrency. We present correct encodings of session-based calculi into ReactiveML, a synchronous reactive programming language.

11.00-12.00
Réné Lozi (Laboratoire JAD)
Titre: Diverses méthodes de construction de générateurs de nombres pseudo aléatoires à partir d’itérations de fonctions non-linéaires ou linéaires par morceaux.
Abstract: Depuis les années 70, l’utilisation de calculs par ordinateurs a relancé l’étude d’itérations de fonctions non-linéaires comme la fonction logistique ou linéaires par morceaux comme la fonction tente (ces études remontaient aux travaux de Julia et Fatou au début du XXème siècle). Ceci a conduit au concept de « chaos », terme introduit par J. Yorke, et à la définition « d’attracteurs étranges ». De nos jours de nombreux auteurs utilisent abusivement les nombres générés par ces itérations à partir d’une donnée initiale (nombres chaotiques), comme s’ils avaient toutes les propriétés des nombres pseudo aléatoires. D’autres auteurs proposent des combinaisons de ces itérations ou d’autres applications d’un espace de dimension n vers lui-même dans le même but. Mais la construction de générateurs de nombres pseudo-aléatoires à partir de nombres chaotiques doit répondre à plusieurs contraintes qui ne sont pas toutes respectées par ces combinaisons. Nous explorons plusieurs méthodes de construction qui se révèlent efficaces pour la construction de CPRNG (chaotic pseudo random number generators) et qui ont des propriétés leur permettant d’être employés en cryptographie. Nous nous interrogeons aussi sur la fiabilité des tests NIST utilisés pour vérifier la nature aléatoire de séries de nombres.

14.00-15.00
Christophe Guyeux (Institut FEMTO-ST)
Titre: Les itérations chaotiques : étude et applications
Abstract: Les itérations chaotiques désignent une collection de systèmes dynamiques discrets issus de travaux théoriques sur le calcul haute performance. Dans le cadre du calcul asynchrone, ils permettaient d'obtenir des résultats de convergence. Or, depuis une dizaine d'années, ces systèmes dynamiques sont dorénavant étudiés pour le « désordre » qu'ils peuvent générer, mesuré avec des outils topologiques ou issus de la théorie de la mesure. Les applications visées ont trait à la sécurité informatique, notamment à la génération de nombres pseudo-aléatoires, aux fonctions de hachage, et aux techniques de chiffrement symétrique. L'objet de cet exposé est de présenter ces itérations chaotiques, les résultats théoriques obtenus les concernant, et les conséquences au niveau des applications.

15.00-15.30
Bruno Martin (I3S)
Titre: Randomness with CA
Abstract: S. Wolfram first proposed to use cellular automata’s rule 30 as a random sequence generator in 1986. It is now well known that rule 30 (as any rule taken out from elementary cellular automata) is not suitable as a good pseudo-random generator. We will describe two main approaches to use cellular automata to generate stronger pseudo-random sequences. The former uses non-uniform cellular automata that combine different rules with various techniques to generate randomness. The latter proposes to enlarge the rule’s radius and takes advantage of Boolean functions theory to provide random sequences. Both approaches give pseudo-random generators that can successfully pass tests of randomness and can be used as a lightweight and high range pseudo-random generator.

A recent conjecture states that all the languages accepted by deterministic reversal bounded counter machines are also contained in a new class of languages called RCM, which admits many interesting properties. In particular all the languages in RCM have holomic generating functions. We show that the conjecture is true for the one counter case ans also for some classes of languages defined in terms of deterministic reversal bounded 1-counter machines.

Les Automates Cellulaires (AC) ont été étudié depuis longtemps comme moyen possible pour construire des primitives cryptographiques. En fait, il y a deux raisons pour utiliser les AC dans la cryptographie: en premier lieu, la complexité qui émerge de la dynamique des certains AC peut être exploitée pour concevoir des systèmes de cryptage qui satisfont des propriétés cryptographiques fortes. En plus, en étant un modèle computationnelle massivement parallèle, les AC sont particulièrement intéressants pour implémenter des algorithmes cryptographiques en hardware de manière efficiente. Aujourd'hui, il y a des chiffrements par blocs qui utilisent des S-boxes basées sur les AC, comme la transformation χ de KECCAK qui a été sélectionnée par le NIST pour le standard SHA-3 de fonctions d'hachage.

Dans cette exposé je vais présenter ma recherche de doctorat sur les applications des AC à la cryptographie. En particulier, je vais introduire deux lignes de recherche principales. La première ligne concerne l'étude des propriétés cryptographiques des AC, en les considérant comme un particulier genre de fonctions booléennes. Dans cette partie, je montrerai des bornes théoriques sur les propriétés qui peuvent être obtenues par les AC, ainsi que des résultats expérimentales sur l'optimisation des règles locales des AC avec des Algorithmes Évolutionnaires (AE). La deuxième ligne de recherche se concentre sur les Schémas de Partage de Secret (SPS) basés sur les AC. Dans cette partie, je vais présenter une caractérisation théorique des SPS engendres par les AC en termes de carrés latin orthogonaux (CLO), aussi que comment on peut construire ces CLO avec les AE.

On considère un système dynamique topologique. L'ensemble limite générique est le plus petit fermé qui a un bassin d'attraction résiduel. On étudie quelques unes de ses propriétés topologiques, et les liens avec l'équicontinuité et la sensibilité. On insistera sur l'exemple des automates cellulaires, pour lesquels l'ensemble limite générique est contenu dans tous les attracteurs sous-décalages.

gSession types are a formalism to model structured communication-based programming. A session type describes communication by specifying the type and direction of data exchanged between two parties. We show that session types are encodable in more primitive and foundational pi-calculus types. Besides providing an expressivity result, the encoding: (i) removes redundancies in the syntax of session types, and (ii) yields standard properties of session types as straightforward corollaries, exploiting the corresponding properties of standard typed pi-calculus. The robustness of the encoding is tested on a few extensions of session types, including subtyping, polymorphism, and higher-order communications. In this talk we present the encoding, some of its applications and recent developments.

Programme complet de la journée sur la page web.

The exchanges between the cells and their microenvironment are essential to the development and tissue homeostasis, they coordinate all cellular activities and are at the heart of physiological processes such as immune response and wound healing. Information is captured to the cell surface, transmitted and interpreted within the cell. Perturbation in the processing of information leads to many diseases including autoimmune diseases, fibrosis and cancer.
In that context, my group is studying the role of extracellular matrix remodeling in liver fibrosis and cancer. This process involves complex signaling processes which are orchestrated by the transforming growth factor TGF-beta. During last ten years, we have developed different integrative and modeling approaches to decipher the complexity of molecular events associated with this process. From static and integrative view to dynamic analyses, from quantitative to qualitative models, I will illustrate how modeling approaches can help to understand complex systems.

The role of software in information systems is becoming increasingly
important, which further requires the construction of reliable
software. However, it is still difficult to develop software without
faults. We are tackling this problem by using constraint programming.
In this talk, we will discuss three such approaches. First, we will
discuss constraint-based methods of fault localization for imperative
programs. Such methods typically encode imperative programs (in,
e.g., C) into constraint problems, and find plausible locations of
faults by solving the constraint problems. Second, we will discuss
soft constraints. In constraint-based fault localization, a faulty
program results in an over-constrained problem, in which some of the
constraints are handled as "soft" constraints that can be relaxed. We
show that different ways of handling soft constraints can affect
results of fault localization. Finally, we will present our new
project on fault localization for reactive systems. We are extending
constraint-based fault localization to the treatment of reactive
systems with connected components that react to events.

Kamel Mohamed FARAOUN, professeur à l’université de Sidi Bel Abbès, Algérie présentera ses travaux de recherche en vue d’une
collaboration potentielle.
Ceux-ci portent sur les systèmes dynamiques chaotiques et leurs
applications à la cryptographie ainsi que sur certains mécanismes de
sécurité à base de couplages bilinéaires sur des courbes elliptiques.

Le problème d'universalité pour une classe de modèles de calcul consiste à trouver un objet, dit universel, qui peut répliquer l'action de n'importe quel autre objet de cette classe, la simulation pouvant éventuellement se faire à un codage près. D'une façon plus formelle, si A_0 est un élément universel dans la classe \C, alors, pour tout autre élément A\in \C, il est vrai que A(x) = f( A_0 ( ) ), où h est la fonction d'encodage de l'entrée, f est la fonction de décodage de la sortie, g est la fonction qui énumère les éléments de \C (par exemple, l'énumération de Gödel), et est une fonction d'appariement, c'est-à-dire une fonction qui associe un nombre unique à toute paire (x,y). Nous nous concentrons sur le problème d'universalité pour les systèmes de réécriture de multiensembles, des systèmes formels qui permettent de représenter les réactions chimiques. Pour des raisons historiques, nous décrivons nos résultats sous la forme des réseaux de Petri avec des arcs inhibiteurs, un modèle équivalent à la réécriture de multiensembles. Nous définissons la taille d'un réseau comme un vecteur comprenant le nombre de places, de transitions, d'arcs inhibiteurs, ainsi que le nombre maximal d'arcs incidents à une transition (le degré maximal de transitions). Nous proposons ensuite des techniques de minimisation de chacun de ces paramètres, tout en mettant en évidence certains compromis.

Un mot infini x est auto-mélangeant s’il admet les décompositions : $x=prod_{i=1}^infty U_iV_i=prod_{i=1}^infty U_i=prod_{i=1}^infty V_i$, avec U_i,V_i mots finis. Autrement dit, x est une produit de mélange de deux copies de x. Nous montrons que beaucoup de mots importants et bien connus sont auto-mélangeants : cela inclut le mot de Thue-Morse et tous les mots Sturmiens qui ne sont pas de Lyndon. Nous trouvons des conditions nécessaires pour l'auto-mélange en prouvons que certains mots (par exemple, la suite de pliage de papier et les mots de Lyndon) ne sont pas auto-mélangeants. Comme une conséquence de notre caractérisation des mots Sturmiens auto-mélangeants, nous déduisons une preuve courte du théorème de Yasutomi sur la classification des mots Sturmiens purement morphiques. De plus, nous apportons une réponse positive à la question de T. Harju sur des mots auto-mélangeants sans carré et nous étudions l'auto-mélange dans les sous-shifts.

On s'intéresse au parallèle entre 2 problèmes sur des modèles distincts d'automates. D'une part, les automates de Mealy (transducteurs lettre à lettre complets) qui produisent des semi-groupes engendrés par les transformations sur les mots infinis associées aux états. En 2013, Gillibert a montré que le problème de la finitude de ces semi-groupes était indécidable. En revanche la question est ouverte dans le cas où l'automate de Mealy produit un groupe. D'autre part, les automates cellulaires unidirectionnels pour lesquels la question de la décidabilité de la périodicité est ouverte. On peut montrer l'équivalence de ces problèmes. On fera un pas vers une preuve d'indécidabilité en montrant qu'il est possible de simuler du calcul Turing dans un automate cellulaire unidirectionnel réversible, rendant ainsi des problèmes de prédiction indécidables ainsi que la question de la périodicité partant d'une configuration donnée finie.

L'objectif sera cette fois-ci de focaliser sur les systèmes dynamiques et les chaînes de Markov à temps continu.

Introduction to the theory of Markov Chains

In theses lectures I will review the theory of discrete time Markov
Chains. After discussing basic facts of the theory (Markov property,
Strong Markov property, recurrence, transcience, irreducibility ...) I
will discuss the ergodic theorem, the convergence of the MC to its
stationary states (spectral gap, entropy) and the theory of large
deviations for MC. I will also discuss the extension of the theory in
the continuous time setting.
 

We consider a bijection between the set of parallelogram polyominoes of size n and a suitable set of pairs of linear partitions. This lets us exploit a simple granular dynamical system in order to design an algorithm which generates all parallelogram polyominoes of size n in constant amortized time.

We deal with the exhaustive generation of the set of reachable states of particular discrete dynamical systems which model the behaviour of sand piles and ice piles.

A widespread approach to software service analysis uses session types.
Very different type theories for binary and multiparty protocols have
been developed; establishing precise connections between them remains
an open problem.

In this talk, I will present the first formal relation between two
existing theories of binary and multiparty session types: a binary
system rooted in linear logic, and a multiparty system based on
automata theory.

Our results enable the analysis of multiparty protocols using a (much
simpler) type theory for binary protocols, ensuring protocol fidelity
and deadlock-freedom.

Dans le cadre de l'ANR COVERIF, nous vous convions à un Workshop autour de la vérification de programmes avec des calculs sur les flottants organisés par le projet CeV de l'équipe MDSC de l'I3S. La vérification de ces programmes soulève des problèmes qui relèvent tant des réels que des flottants. Les problématiques des flottants, des réels, des techniques de vérification et de leurs interactions seront présentées par quatre orateurs reconnus pour la qualité de leurs contributions dans ces thèmes.

Conley theory studies qualitative features of dynamical systems by means of topological invariants of isolated invariant sets. Since the invariants are stable under perturbations and computable from a finite sample, they provide a tool for rigorous, qualitative numerical analysis of dynamical systems.

In this talk, after a brief introduction to Conley theory, I will present its recent extension to combinatorial multivector fields, a generalization of the concept introduced by R. Forman in his discrete (combinatorial) Morse theory. I will also show some numerical examples indicating potential applications in the study of sampled dynamical systems.

Reaction systems are a new mathematical formalism inspired by the living cell and driven by only two basic mechanisms: facilitation and inhibition. As a modeling framework, they differ from the traditional approaches based on ODEs and CTMCs in two fundamental aspects: their qualitative character and the non-permanency of resources. In this article we introduce to reaction systems several notions of central interest in biomodeling: mass conservation, invariants, steady states, stationary processes, elementary fluxes, and periodicity.  We prove that the decision problems related to these properties span a number of complexity classes from P to NP- and coNP-complete to PSPACE-complete.

In this seminar, we use the paradigm of Granular Computing (briefly GrC) in some mathematical contexts as linear algebra, matroid theory, graph and hypergraph theory. By doing this, we want to create a new link between discrete mathematics and computer science. The aim of this investigation is twofold: to find new properties of the mathematical objects at issue and, on the other hand, to improve the techniques of GrC. To this regard, we can interpret a graph as an information system and we can translate the indiscernibility relation in terms of Erdos-Renyi symmetry. A complete study of an information system can be achieved by the Granular Partition Lattice, thanks to which we can understand how indiscernibility varies depending on the avalaible knowledge. Hence, we can study information systems by means of linear algebra and lattice theory. Moreover, we also associate an entropy function measuring the uniformity of the distribution of the objects in the blocks of all indiscernibility partitions. This function allows us to develop a temporal perspective of the dynamical evolution of graphs.

De nombreux phénomènes, tels que le codage de réseau, les réseaux de neurones, les réseaux de gènes etc. peuvent être modélisés par des systèmes dynamiques finis. L'étude, et en particulier la maximisation, du nombre de points fixes des systèmes dynamiques finis est un problème très important pour ces applications. L'entropie d'un graphe a été introduite pour obtenir des bornes supérieures sur le nombre de points fixes, qui peuvent être exprimées comme de solutions optimales de programmes linéaires. Cet exposé est une invitation à la recherche dans ce domaine : après une description de l'entropie des graphes, nous illustrerons le potentiel de cet approche par des exemples et nous suggérerons des pistes pour la développer.

We propose a novel approach for the formal verification of biological systems based on the use of a modal linear logic. We show how such a logic can be used, with worlds as instants of time, as an unified framework to encode both biological systems and temporal properties of their dynamic behaviour. To illustrate our methodology, we consider a model of the P53/Mdm2 DNA-damage repair mechanism. We prove several properties that are important for such a model to satisfy and serve to illustrate the promise of our approach. We formalize the proofs of these properties in the Coq Proof Assistant, with the help of a Lambda Prolog prover for partial automation of the proofs.

La modélisation qualitative des réseaux de régulation biologique a connu ses début grâce aux travaux de Kauffman (1969) puis de Thomas (1973) qui ont posé les bases de la modélisation discrète sous forme de graphes. Ceux-ci permettent de grandement réduire la complexité de l'analyse des comportements du système modélisé par rapport aux modèles traditionnels basés sur des équations différentielles. Cependant, la taille de ces réseaux, construits sur la base d'observations expérimentales, a aussi explosé, ce qui a posé à nouveau la question de leur analyse dynamique. Durant ce séminaire, je présenterai le modèle de Thomas, très répandu au sein de la communauté, et je montrerai comment des travaux successifs ont permis d'étendre l'expressivité, mais aussi les capacités d'analyse, de ce type de modèles. Je détaillerai ainsi mes travaux portant sur l'analyse de la dynamique par interprétation abstraite, qui permet d'obtenir des résultats d'atteignabilité sur de grands modèles en très peu de temps. Je présenterai aussi mes travaux consistant à utiliser le µ-calcul polyadique pour effectuer de la recherche de propriétés dynamiques plus complexes sur ces mêmes modèles.