CMF 08 au LABRI !

Mode d'emploi:
1- s'identifier en suivant ParametresUtilisateur puis Nom=cmf Mot de Passe =cmfcmf
2- suivre "Proposer un Exposé", double click sur la page
3- éditer
4- donner la réponse à l'énigme en bas à gauche (ex: 2+ 7 = 9), puis clicker "enregistrer"

(A editer)....

---

CMF 07 au LORIA !

Complexity in learning from examples (Olivier Teytaud)

We survey various models of complexity in learning from examples, including Valiant's PAC-model
and the VC-dimension.
We then focus on the active learning frameworks (user-chosen examples, labelled by an oracle),
and study (i) the randomness requirement (ii) convergence rates with "randomized" quasi-randomization.

50 ans de problèmes de spectres en logique (Malika More)

En logique, le spectre d'une propriété est l'ensemble des nombres d'éléments des objets finis qui possèdent cette propriété. Depuis les années 1950, la notion de spectre a été étudiée selon plusieurs approches successives. Dans cet exposé historique, je présenterai un tour d'horizon des questions principales et des résultats les plus importants du domaine, en insistant sur les liens avec des questions d'informatique fondamentale moderne.

Réduction non-bornée de la longueur de preuves en déduction modulo (Guillaume Burel)

En 1973, Parikh a démontré un théorème d'accélération conjecturé par
Gödel 37 ans auparavant, qui dit qu'il existe des formules de
l'arithmétique qui sont toutes démontrables en arithmétique du première
ordre, mais dont la preuve la plus courte en arithmétique du second
ordre est arbitrairement plus courte que n'importe quelle preuve au
premier ordre. D'un autre côté, la résolution d'ordre supérieur peut
être simulée pas à pas en utilisant une méthode de surréduction et de
résolution du premier ordre basée sur la déduction modulo, dont le
paradigme est de séparer la déduction et le calcul pour rendre les
preuves plus lisibles et plus courtes.

Premièrement, nous démontrons qu'une preuve dans l'arithmétique
d'ordre $i+1$ peut être transformée linéairement en une preuve dans
l'arithmétique d'ordre $i$ modulo un système de réécriture fini,
terminant et confluent. Nous montrons également qu'il existe un gain de
preuve non borné entre l'arithmétique d'ordre $i$ modulo ce système et
l'arithmétique d'ordre $i$ sans modulo. Tout ceci nous permet d'affirmer
que le gain sur la taille des preuve conjecturé par Gödel ne provient
pas de la déduction, mais peut être exprimé en tant que calcul simple,
ce qui justifie l'utilisation de la déduction modulo comme un outil du
premier ordre efficace pour simuler l'ordre supérieur.

Calculer en parallèlle sans horloge : automates cellulaires asynchrones (Nazim Fates)

A la différence des modèles "classiques" de l'informatique qui sont dans leur grande majorité séquentiels, les automates cellulaires sont définis comme des systèmes massivement parallèles où le temps, l'espace et l'état des composants élémentaires sont discrets. Ces systèmes ont la particularité de bien faire émerger la problématique des liens entre descriptions "microscopiques" et "macroscopiques" : en règle générale le problème qui consiste à prédire le comportement global à partir de la connaissance de la règle locale d'interaction est difficile (voire plus).

Mon exposé se concentrera sur les familles d'automates cellulaires "élémentaires" où chaque cellule n'a que deux états. Je montrerai la richesse des comportements observables dans le cas "classique" synchrone où toutes les transitions sont appliquées en même temps. Dans un deuxième temps, afin de se rapprocher d'une modélisation de phénomènes asynchrones (naturels ou artificiels), j'examinerai ce qu'il se produit quand les transitions deviennent stochastiques. Quels sont les effets d'une telle modification de la mise à jour? Quels sont les règles qui "résistent" partiellement ou totalement à cette modification? Quels sont les outils mathématiques et algorithmiques qui permettent de quantifier les changements de comportement?

Recursion Theorems as a foundation of computer virology (Jean-Yves Marion)

We are concerned with theoretical aspects of computer viruses. For
this, we suggest a new definition of viruses which is clearly based on
the iteration theorem and above all on Kleene’s recursion theorem. We
show that we capture in a natural way previous definitions, and in
particular the one of Adleman. We establish generic virus
constructions and we illustrate them by various examples. We show
results on virus detection. Lastly, we make some experimentations.

Autour de problèmes de pavage dans le plan hyperbolique, une approche algorithmique (Maurice Margenstern)

Détails à venir.

Symétrie de l'information et bornes inférieures non-uniformes (Sylvain Perifel)

Le théorème de hiérarchie en temps montre qu'il existe des problèmes décidables en temps exponentiel n'ayant pas d'algorithme polynomial. En revanche, la question de savoir s'ils peuvent tous être décidés par des circuits de taille polynomiale est encore ouverte. Dans cet exposé, nous verrons comment répondre à cette question sous une hypothèse de complexité de Kolmogorov, à savoir la symétrie de l'information en temps polynomial.

Pour s'échauffer, dans un premier temps nous montrerons le résultat inconditionnel suivant : pour toute constante c, il existe des problèmes décidables en temps exponentiel mais pas par des circuits de taille n^c. Puis nous verrons comment modifier la construction pour que l'hypothèse de symétrie de l'information permette une diagonalisation sur tous les circuits de taille polynomiale.

Constraint Satisfaction over Infinite Domains: Finite Model Theory meets Classical Model Theory (Manuel Bodirsky)

The descriptive complexity of constraint satisfaction problems (CSPs)
over finite domains is an important topic in finite model theory. CSPs provide natural computational problems for many complexity classes in descriptive complexity; on the other hand, tools from finite model theory (Datalog, pebble-games, finite-variable logics, fragments of second-order logic, etc) have been very successful to describe the computational complexity of CSPs.

Many CSPs can not be formulated with finite domains: this
is the case for most of the CSPs in temporal and spatial reasoning, computational linguistics, phylogenetic reconstruction,
or CSPs that are in SNP. To study the computational complexity
of these CSPs over infinite domains, concepts from classical model theory become relevant (preservation theorems, omega-categoricity,
amalgamation, Ramsey theory). In this talk, I will discuss some of the meeting points of finite and infinite model theory in constraint satisfaction complexity.

Autour de la complexité de l'énumération de requêtes (Arnaud Durand)

Détails à venir.

FO+TC versus MSO sur les arbres. (Luc Segoufin)

Dans cet exposé on va considérer l'extension de la logique du premier ordre avec un opérateur de clotûre transitive "unaire", notée FO+TC par la suite. Sur toute structure (finie) on observera que FO+TC est toujours moins expressif que MSO. Sur les mots il est facile de coder tout automate fini à l'aide d'une formule de FO+TC, donc FO+TC=MSO. On va donc s'intéresser au cas des arbres. On introduira alors deux familles naturelles d'automate d'arbres dont on comparera le pouvoir d'expression avec celui de FO+TC. À l'aide de ces automates on montrera que FO+TC est strictement moins expressif que MSO sur les arbres.

On the complexity of temporal reasoning about sequences of memory states (Stéphane Demri)

In order to verify programs with pointer variables, we introduce a temporal
logic whose underlying assertion language is the quantifier-free
fragment of separation logic and the temporal logic on the top of it is the
standard linear-time temporal logic LTL.
We analyze the computational complexity of various model-checking and
satisfiability problems, considering various fragments of separation logic
(including pointer arithmetic), various classes of models (with or without
constant heap), and the influence of fixing the initial memory state.
Our main decidability result is the PSPACE-completeness of the
satisfiability problems on the record fragment and
on a classical fragment allowing pointer arithmetic.
Undecidability results are established for various problems by reducing standard
problems for Minsky machines, and underline the tightness of our decidability
results.

This is a joint work with R. Brochenin (LSV) and E. Lozes (LSV).

Verification Problems for Programs with Singly-Linked Lists (Radu Iosif)

We address the verification problem of programs manipulating one-selector linked data structures. We propose a new automated approach for checking safety and termination for these programs. Our approach is based on using counter automata as accurate abstract models: control states correspond to abstract heap graphs where list segments without sharing are collapsed, and counters are used to keep track of the number of elements in these segments. This allows to apply automatic analysis techniques and tools for counter automata in order to verify list programs. We show the effectiveness of our approach, in particular by verifying automatically termination of some sorting programs.

In the second part of the talk, we analyze the complexity of checking safety and termination properties,
for a very simple, yet non-trivial, class of programs with singly-linked list data structures.
Since, in general, programs with lists are known to have the power of Turing machines, we
restrict the control structure, by forbidding nested loops and destructive updates.
Surprisingly, even with these simplifying conditions, programs working on heaps with more
than one cycle are undecidable, whereas decidability can be established when the input
heap may have at most one loop. The proofs for both the undecidability and the decidability
results rely on non-trivial number-theoretic results.

Joint work with Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Tomas Vojnar and Pierre Moro.

Relational semantics and finite models of separation logics. (Dominique Larchey)

In this talk we consider BI Logic and some of their variants like
Boolean BI Logic (BBI) or BI's Pointer Logic (PL) from a semantic perspective. These logics arise as logical bases of some recent separation logics used for reasoning about mutable data structures. First we discuss new results and open questions for BBI about models
and provability that are obtained from alternative semantic
foundations based on relational semantics. We complete the study with
similar results or questions for similar logics like BI or PL. Then starting from a relational semantics for BBI, which can also be
viewed as a non-deterministic monoidal semantics, we show that
BBI includes some S4-like modalities and deduce new (surprising)
results: faithful embeddings of S4 modal logic, and then of
intuitionistic logic (IL) into BBI, despite of the classical nature of its additive connectives. Consequences on proof search and
countermodel generation in these logics will be discussed.
This is a joint work with D. Galmiche and D. Méry.

Approximate Equivalence of Transduction (Adrien Vieilleribière)

With regard to the development of xslt, we are concerned with the computational aspects of the equivalence of structures transformations.
First, several models of transduction of words and trees are surveyed. The equivalence problem appears to be computationally hard, and even undecidable when the transformations are not deterministic.
Therefore, we introduce a relaxation of this problem based on the edit distance with moves.
In this new framework, two transformations are epsilon-equivalent if for all couple of structures (I,J) in the relation defined by a transduction, one can find I’ epsilon-close to I and J’ epsilon-close to J such that (I’,J’) is in the relation defined by the other transduction.
How to solve this approximate equivalence problem?
By means of an embedding based on the statistical representation of data, a solution for these non deterministic transductions is obtained.

Convexité, Théorèmes min-max et Symétries (Vincent Nesme)

Quand la solution d'un problème symétrique est-elle elle-même symétrique ? Quand peut-on inverser min et max dans un problème d'optimisation ? La programmation linèire et la programmation semi-définie fournissent des exemples de dualité, mais que faire, par exemple, lorsque le domaine de définition de la fonction étudiée n'est pas convexe ? J'aborderai ces questions en faisant appel à des résultats probalement moins connus du grand public que le théorème minimax de von Neumann, et en fournissant des exemples variés, notamment du côté du calcul quantique.

Méthode structurelle pour décider si une relation rationnelle est k-valuée

Les transducteurs sont des automates dont les transitions sont étiquetés par une couple de mots, représentant une entrée et une sortie, et réalisent des relations entre des mots connues comme "relations rationnelles". Nous retrouvons les premières investigations de ce type de machine dans l'aurore de la Théorie des Automates, et aujourd'hui son étude est une partie fondamentale dans ce domaine.

Le problème de décider si un transducteur réalise une fonction figure parmi les résultats de décidabilité le plus classiques pour ces automates. Une première réponse a été donnée par Schützenberger en 1976, avec un argument combinatoire dont la complexité est exponentielle dans le nombre d'états du transducteur consideré. Le problème a éte repris par d'autres auteurs a partir des annés 1990 dans une ligne plus structurelle, où la décidabilité est une conséquence de constructions avec des automates. Il en résulte des algorithmes dont les complexités sont polynomiales.

Une généralisation naturelle de ce problème est celui de décider si un transducteur réalise une relation dont l'image de chaque mot d'entrée est un ensemble de au plus k mots, pour un entier k donné - une telle relation est appelé "relation rationnelle k-valuée". Une réponse positive a été donnée par Gurari et Ibarra en 1983, en réduisant le problème au problème de tester le vide pour une classe d'automates à compteurs
dont la décidabilité en complexité polynomiale était connue. L'ordre exacte de cette complexité a resté toutefois difficile a estimer.

Nous allons présenter dans cet exposé l'une des approches structurelles pour le problème de décider si un transducteur réalise une fonction, donnée par Béal et al: la construction du carré du transducteur et de son produit par une action décrivant les différences de sorties dans les chemins de cette structure. Ensuite, nous allons montrer comment cette construction peut être étendue - en faisant le produit (k+1) fois du transducteur par lui même - pour tester si un transducteur est k-valué. Comme conséquence, nous avons un algorithme dont la complexité (polynomiale) peut être calculée avec plus de précision, et semble être meilleure que celle obtenue par Gurari et Ibarra.

Travail en collaboration avec Jacques Sakarovitch.

Complexity of Default Logic on Generalized Conjunctive Queries (Miki Hermann)

Details to be announced.

Next talk

---

Pour connaitre les régles de contribution cliquez ici .

programmes