Mardi 6 Janvier
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Généralisation des nombres et polynômes de Bernoulli aux cas multiples |
Description: |
Olivier Bouillot |
Mercredi 7 Janvier
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Generalized paper-folding sequences |
Description: |
Johan Nilsson |
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Extracting information from text: Language Understanding and Sentiment analysis |
Description: |
Emilio Sanchis |
Mardi 13 Janvier
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Generalized paper-folding sequences |
Description: |
Johan Nilsson |
Mercredi 14 Janvier
Heure: |
15:30 - 16:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Cost Linear Temporal Logic for Verification |
Description: |
Maximilien Colange Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties.
We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata. |
Vendredi 16 Janvier
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Approche philologique des langages de programmation |
Description: |
Baptiste Mélès La théorie des langages de programmation s'appuie généralement sur des langages de programmation théoriques lambda-calcul, machines de Turing, et leurs variantes que l'on suppose représenter fidèlement à compilation près ! les propriétés des langages de programmation de la « vraie vie », si l'on entend par là ceux que les programmeurs utilisent pour écrire des programmes utiles au quotidien : C, C++, Perl, etc.
Or nous allons voir que les langages de programmation de la vraie vie possèdent bien des propriétés dont nul ne voudrait dans un langage théorique, et que la compilation écrase : des commandes inutiles, des redondances, des résidus purement historiques... Qui plus est, loin d'être un fait simplement négatif, ces propriétés constituent une bonne part de leur expressivité du point de vue du programmeur, et sont autant de points communs avec les langues naturelles. Nous verrons ainsi que des outils linguistiques et philologiques peuvent être mobilisés pour décrire une « sémantique du programmeur », qui échappe pour une bonne part aussi bien aux sémantiques courantes des langages de programmation qu'aux tentatives de description formelle de l'expressivité des langages de programmation. |
Lundi 19 Janvier
Heure: |
13:30 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
A Text Analytic Approach to Historical Legal Records |
Description: |
Adam Zachary Wyner The council registers of Aberdeen, Scotland are the earliest and most complete body of town (or burgh) council records in Scotland, running nearly continuously from 1398 to the present; they are hand written in Latin and (largely) Middle Scots. Few cities in the United Kingdom or in Western Europe rival Aberdeen's burgh registers in historical depth and completeness. In July 2013, UNESCO UK recognised the register volumes from 1398 to 1509 as being of outstanding historical importance to the UK. The registers offer a detailed view into the legal aspects of life in one of Scotland's principal burghs, providing a view into administrative, legal, and commercial activities as well as daily life. The registers include information about a range of matters, from the elections of office bearers, property transfers, regulations of trade and prices, references to crimes and subsequent punishment, to matters of public health, credit and debt, cargoes of foreign vessels, tax and rental o f burgh lands, and woods and fishings. Thus the entries present the burgh's relationships with the countryside and countries around the North Sea.
This talk discusses the results of a text analytic project developed around 100 transcribed pages of these records from the period 1530-1531. We worked with the General Architecture for Text Engineering (GATE) text analytic tool. In the project, we created a large, rich, and varied range of semantic annotations such as individual's names, locations, various materials of trade, legal concepts, translation, offices, social status, documents, shipping terminology, and many others. The annotations can be examined either in situ or as complex semantic queries.
With this application, users can hover over the text and receive a translation into English, making the text accessible to a large audience. Legal historians can query and study the text in novel and illuminating ways, for example, rapidly examining the use of particular terminology or patterns over the whole corpus. Moreover, legal historians can scale up their textual studies - while the particular tool was developed for only 100 pages, it can be applied to larger corpus of related material of some 600 pages. The tool is also highly extensible, allowing for modification of the current analysis as well as the addition of other material that may be beyond the scope of the Aberdeen registers.
We outline the project objectives, present the text analytic tool, show the range of annotations, provide some sample results of queries, relate our work to other projects, and sketch future work. Broadly, the paper and project contribute to the application of language technologies for cultural heritage and the humanities. More specifically, the research provides a text analytic approach to studying the evolution of legal concepts and their application over time, providing legal historians with the means to gain fresh insights to historical and contemporary legal systems. |
Mardi 20 Janvier
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Statistical physics and combinatorics |
Description: |
Francesco Caltagirone |
Mercredi 21 Janvier
Heure: |
14:00 - 15:00 |
Lieu: |
Amphi A |
Résumé: |
Quantum Computing: From physics to computational systems |
Description: |
Andrea Masini |
Jeudi 22 Janvier
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Specification and verification of Time Petri Nets with Coq |
Description: |
Amal Chamakh Model checking and theorem proving, have long reached their limitation as general-purpose techniques, and most of the research now is concentrated on efficient specialization of both approaches to relatively narrow problem domains. The state space explosion problem leaves little hope for automatic finite-state verification techniques like model checking to remain practical, especially when designs become parameterized. The use of theorem proving techniques is inevitable to cope with the new verification challenges. "Pure" theorem proving, on the other hand, can also be quite tedious and impractical for complex designs. Ideally, one would like to find an efficient combination of model checking and theorem proving, and the quest for such a combination has long been one of the major challenges in the field of formal verification. In this paper, we address the combination of model checking and theorem proving approaches in order to specify and to model check Time Petri Nets (TPN) model-based systems. In particular, we show how a TPN is specified using the Coq proof assistant, and how the fireability/unfireability of a timed sequence of transitions can be proved. This allows, for instance, to prove the reachability of a given state by the firing of a given timed/untimed trace or to prove that a counter-example supplied by a given (untimed) model checker is a real counterexample of a timed system. %First, we provide a formalization of the net model in COQ via the parsing of its Petri Net Markup Language (PNML) description. Then the COQ proof assistant is used to prove the firability (or the opposite) of traces given by model checking as a counter-example when a propriety being checked is found to be non-valid, hence, states reachability is proved. |
Vendredi 23 Janvier
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
An Introduction to Higher-Dimensional Rewriting Theory |
Description: |
Samuel Mimram À venir. |
Lundi 26 Janvier
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Apprentissage faiblement supervise d'un etiqueteur morpho-syntaxique par transfert cross-lingue |
Description: |
Guillaume Wisniewski Les méthodes de transfert cross-lingue permettent partiellement de pallier l'absence de corpus annotés, en particulier dans le cas de langues peu dotées en ressources linguistiques. Le transfert d'étiquettes morpho-syntaxiques depuis une langue riche en ressources, complété et corrigé par un dictionnaire associant à chaque mot un ensemble d'étiquettes autorisées, ne fournit cependant qu'une information de supervision incomplète. Dans ce travail, nous reformulons ce problème dans le cadre de l'apprentissage ambigu et proposons une nouvelle méthode pour apprendre un analyseur de manière faiblement supervisée à partir d'un modèle à base d'historique. L'évaluation de cette approche montre une amélioration sensible des performances par rapport aux méthodes de l'état de l'art. |
Mardi 27 Janvier
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Soutenance de thèse (AOC-RCLN) |
Description: |
Nada Mimouni |
Vendredi 30 Janvier
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Une introduction à la théorie de Squier |
Description: |
Yves Guiraud Un monoïde ayant une présentation par un système de réécriture convergent fini a un problème du mot décidable. Dans les années 1980, Jantzen s'interroge sur la réciproque : un monoïde ayant un problème du mot décidable admet-il toujours une présentation par un système de réécriture convergent fini ? Squier a répondu négativement à cette question en reliant des propriétés algorithmiques des systèmes de réécriture, comme la terminaison et la confluence, à des invariants algébriques, comme l'homologie ou l'homotopie.
Dans cet exposé, je présenterai le résultat initial de Squier, dans le formalisme de la réécriture de dimension supérieure. Puis, nous verrons comment le travail de Squier permet aujourd'hui d'utiliser la réécriture comme méthode constructive pour calculer des invariants de structures algébriques. |
Heure: |
14:00 - 14:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Cost Linear Temporal Logic for Verification |
Description: |
Maximilien Colange Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties.
We focus on an extension of Linear Temporal Logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This logics can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. We also propose a CEGAR-like approach to answer compute the bounds of the values reached by the automata. |
Heure: |
14:40 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Vérification de Spécifications EB-3 à l'aide de Techniques de Model Checking |
Description: |
Dimitrio Vekris EB-3 est un langage de spécification développé pour la spécification des systèmes d'information. Le noyau du langage EB-3 comprend des spécifications d'algèbre de processus afin de décrire le comportement des entités du système et des fonctions d'attributs qui sont des fonctions récursives dont l'évaluation se fait sur la trace d'exécution du système décrivant les attributs des entités. La vérification de propriétés temporelles en EB-3 est un sujet de grande importance pour des utilisateurs de EB-3. Dans cet exposé, on se focalise sur les propriétés de vivacité concernant des systèmes d'information exprimant l'éventualité que certaines actions puissent s'exécuter. La vérification des propriétés de vivacité se fait à l'aide de model checking.
En se basant sur une sémantique opérationnelle de EB-3, selon laquelle les fonctions d'attributs sont évaluées pendant l'exécution du programme puis stockées, on définit une traduction automatique de EB-3 vers LNT, qui est un langage simultané enrichi d'une algèbre de processus. Notre traduction assure la correspondance un à un entre les états et les transitions des systèmes étiquetés de transition correspondent respectivement à des spécifications EB-3 et LNT. Ensuite, on automatise la traduction grâce à l'outil EB3toLNT fournissant aux utilisateurs de EB-3 tous les outils de vérification fonctionnelle disponible dans CADP. |
Mardi 3 Février
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Graph polynomials and relations with physics |
Description: |
Adrian Tanasa In the first part of the talk I will introduce the Tuttepolynomial of graphs and explicitly show its relation withpolynomials appearing in the so-called parametric representation ofintegrands canonically associated to graphs in quantum field theory.In the second part of the talk I will show a new proof of thecelebrated property of universality of the Tutte polynomial of graphs(or matroids), proof which does not require the usual edge inductionarguments. Finally, I will present how this proof generalizes for theuniversality property of the Bollobas-Riordan polynomial of ribbongraphs (or embedded graphs). |
Mardi 10 Février
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Énumérer les cartes farcies de toute topologie (avec un soupçon de combinatoire analytique) |
Description: |
Gaëtan Borot Les cartes sont des surfaces discrètes construites en recollant lelong de leurs bords des polygônes - l'exemple le plus simple étant lestriangulations. En tant que surfaces orientables, leur topologie estcaractérisée par le nombre de bords n, et le nombre d'anses g. Si l'onse donne un poids de Boltzmann t_k pour chaque k-gone, l'énumérationdes cartes à un bord et de genre 0 est un problème très bien étudié.Ici, je considèrerai le problème plus général d'énumérer les cartesfarcies: ce sont les surfaces obtenues en a) piochant dans une boîte àoutils pouvant contenir des surfaces à bords polygonaux et detopologie quelconque ; b) en recollant ces morceaux élémentaires lelong de leurs bords ; c) pondérant l'énumération par des poids deBoltzmann dépendant du genre et de la longueur des bords de chaquemorceau élémentaire. J'expliquerai notamment qu'il existe unerécurrence universelle sur la caractéristique d'Euler totale 2 - 2g -n, qui réduit le problème d'énumération en toute topologie à celui desdisques (n = 1, g = 0) et des cylindres (n = 2,g = 0). |
Vendredi 13 Février
Heure: |
11:30 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Model checking en logique de dépendance |
Description: |
Nicolas de Rugy-Altherre La logique de dépendance et ses variantes (indépendance et inclusion) ont été introduites par Vänäänen il y a quelques années pour parler de façon "propre" de dépendance en logique. Je présenterai cette logique et ses résultats principaux en complexité. |
Mardi 17 Février
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Problèmes de satisfaction de contraintes et graphes inhomogènes |
Description: |
Élie de Panafieu |
Jeudi 19 Février
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Modelling Timed Concurrent Systems Using Activity Diagram Patterns |
Description: |
Étienne André UML is the de facto standard for modelling concurrent systems in the industry. Activity diagrams allow designers to model workflows or business processes. Unfortunately, their informal semantics prevents the use of automated verification techniques. In this paper, we first propose activity diagram patterns for modelling timed concurrent systems; we then devise a modular mechanism to compose timed diagram fragments into a UML activity diagram that also allows for refinement, and we formalise the semantics of our patterns using time Petri nets. Our approach guides the modeller task% (helping to avoid common mistakes), and allows for automated verification.
Joint work with Christine Choppy and Thierry Noulamo |
Vendredi 20 Février
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Coherence spaces for computable analysis |
Description: |
Kazushige Terui Abstract: There have been two mainstream approaches in computable analysis: the type-two theory of effectivity (TTE) and the theory of domain representations. This paper proposes an intermediary approach based on coherence spaces, which is as concrete as TTE and as structured as domain theory.
We import various concepts from TTE such as admissibility, and provide admissible representations for the real line, Euclidean spaces and function spaces over them. This allows us to represent, for instance, a real continuous function by a stable map. A natural question is then what linear maps correspond to in terms of analysis. Our answer is that they correspond to uniformly continuous functions. This leads to an internal expression of Heine's theorem (every continuous function on a compact interval of the real line is uniformly continuous) as the existence of a certain map from a stable function space to a linear function space.
We finally illustrate an application of coherence spaces as a type system for lambda calculus, which allows us to verify local properties of real functions.
This is a joint work with Kei Matsumoto. |
Mardi 24 Février
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Profile of random trees |
Description: |
Michael Drmota |
Mercredi 25 Février
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Quasi-random properties of subsequences of sequences generated by finite automata |
Description: |
Michael Drmota Automatic sequences T(n) are the output sequence of a finite automaton, wherethe input is the q-adic digital representation of n. The most prominent exampleis the Thue-Morse sequence t(n) (that is also the fixed point of the substitution0 -> 01, 1 -> 10). Automatic sequences have been studied in many diff erent contextsfrom combinatorics to algebra, number theory, harmonic analysis, geometryand dynamical systems. For example, they have a linear subword complexity andthey are almost periodic.Since the subword complexity is linear the entropy of the related dynamical system is zero. This also means thatthey do not behave like a random sequence. However, the situation changes drastically whenone uses proper subsequences of automatic sequences, for example the subsequence along primes orsquares. It is conjectured that the resulting sequences are normal sequences so thatthey behave like random sequences (=quasi random sequences).Recently this property was proved (together with C. Mauduit and J. Rivat)for the Thue-Morse sequence along the subsequence of squares - and it turns out that thispropery extends to several other automatic sequences and also to subsequences of the form[n^c], where 1 < c < 4/3. Thus such subsequences of automatic sequences give rise toa completely new class of pseudo random sequences that can be computed very efficiently. |
Heure: |
14:00 - 15:00 |
Lieu: |
Amphi A |
Résumé: |
Quasi-Random Properties of Subsequences of Sequences Generated by Finite Automata |
Description: |
Michael Drmota Automatic sequences T(n) are the output sequence of a finite automaton, where the input is the q-adic digital representation of n. The most prominent example is the Thue-Morse sequence t(n) (that is also the fixed point of the substitution 0 -> 01, 1 -> 10). Automatic sequences have been studied in many diff erent contexts from combinatorics to algebra, number theory, harmonic analysis, geometry and dynamical systems. For example, they have a linear subword complexity and they are almost periodic.
Since the subword complexity is linear the entropy of the related dynamical system is zero. This also means that they do not behave like a random sequence. However, the situation changes drastically when one uses proper subsequences of automatic sequences, for example the subsequence along primes or squares. It is conjectured that the resulting sequences are normal sequences so that they behave like random sequences (=quasi random sequences). Recently this property was proved (together with C. Mauduit and J. Rivat) for the Thue-Morse sequence along the subsequence of squares - and it turns out that this propery extends to several other automatic sequences and also to subsequences of the form [n^c], where 1 < c < 4/3. Thus such subsequences of automatic sequences give rise to a completely new class of pseudo random sequences that can be computed very efficiently. |
Vendredi 27 Février
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Linear numeral systems |
Description: |
Ian Mackie We take a fresh look at an old problem of representing natural numbers in the lambda-calculus. Our interest is in finding representations where we can compute efficiently (and where possible, in constant time) the following functions: successor, predecessor, addition, subtraction and test for zero. Surprisingly, we find a solution in the linear lambda-calculus, where copying and erasing are not permitted. |
Lundi 2 Mars
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Open questions on Dynamic Semantic Annotation |
Description: |
Ivan GARRIDO MARQUEZ Semantic annotation provides a powerful advantage for several applications requiring text analysis. Semantic annotation requires the presence of a semantic model to link the elements of the text to their semantic representation. An a priori built ontology requires to be maintained, adapted and to grow to keep its usefulness. When this update is made along the annotation process, by exploiting the annotated text to enrich the model we can discuss a dynamicity of the annotation. We can identify two processes closely related with this dynamicity, the knowledge acquisition and the annotation process itself. On this talk we will try present an overview on this processes and how they have been approached before. |
Mardi 3 Mars
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Généralisation des nombres et polynômes de Bernoulli aux cas multiples |
Description: |
Olivier Bouillot Les nombres et polynômes de Bernoulli sont des objets classiques qui apparaissent respectivement lors du prolongement analytique des fonctions zêta de Riemann et de Hurwitz aux entiers négatifs.En lien avec la généralisation multiple de ces fonctions, les multizêtas et multizêtas de Hurwitz, nous allons généraliser les nombres et polynômes de Bernoulli au cas multiple.Bien qu'il n'y a pas unicité d'une telle généralisation, nous introduirons un exemple explicite et satisfaisant où nombres de propriétés importantes des polynômes de Bernoulli se transmettent au cas multiple.Au passage, cela permet de répondre à une question sur la renormalisation des multizêtas aux entiers négatifs. |
Mercredi 4 Mars
Heure: |
09:30 - 10:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
On an Extension of Freeze LTL with Ordered Attributes |
Description: |
Normann Decker We present an extension of Freeze LTL, a temporal logic equipped with registers, over data words. Each position in a (multi-attributed) data word carries a letter from a finite alphabet and assigns a data value to a fixed, finite set of attributes. While reasoning on collections of data values is valuable for expressing correctness properties of executions of dynamic programs the satisfiability problem of Freeze LTL is undecidable if more than one register is available or tuples of data values can be stored and compared arbitrarily. Our extension therefore allows for specifying a dependency relation on attributes. These dependencies introduce a restricted, yet flexible way of storing and comparing collections of attribute values. This new dimension of flexibility is orthogonal to, e.g., the number of registers or the available temporal operators. In this setting we characterise precisely the type of dependency relations that maintain decidability of the logic. To this end, we employ reductions from and to nested counter systems. Moreover, by a complexity theoretic characterisations we can show that our extension is strict and induces a semantic hierarchy of logical fragments. |
Vendredi 6 Mars
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
The Plotkin's call-by-value lambda-calculus from a linear-logical viewpoint |
Description: |
Giulio Guerrieri We translate the terms of ordinary lambda-calculus into proof-nets accordingly the Girard's call-by-value "boring'' encoding of intuitionistic implication A->B = !A-o!B. We show that (1) the Plotkin's call-by-value beta-reduction is (bi)simulated in proof-nets via cut-elimination; (2) there is a sequentialization theorem that characterizes all and only the proof-nets which are translations of some lambda-term; (3) the equivalence relation on lambda-terms which identifies lambda-terms having the same translation in proof-nets is the call-by-value counterpart of Regnier's sigma-equivalence and is not included in Plotkin's call-by-value beta-equivalence. The semantics of lambda-terms is preserved by our call-by-value sigma-equivalence. Adding an oriented version of the call-by-value sigma-rules to the call-by-value beta-reduction (and keeping the same syntax of ordinary lambda-calculus) we preserve confluence and we get a call-by-value operational characterization of solvable and potential valuable terms (this is not possible in original Plotkin's call-by-value lambda-calculus). Moreover, we give a semantic characterization of solvable and potential valuable terms in a relational model, based on Linear Logic, satisfying the Taylor expansion formula. As a technical tool, we also use a resource-sensitive calculus in which the elements of the model are definable. |
Lundi 9 Mars
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Sequence Classification Based on Delta-Free Sequential Patterns |
Description: |
Pierre Holat Sequential pattern mining is one of the most studied and challenging tasks in data mining. However, the extension of well-known methods from many other classical patterns to sequences is not a trivial task. This talk presents a study of the notion of delta-freeness for sequences. While this notion has extensively been discussed for itemsets, the work described in this talk is the first to extend it to sequences. In this work, we define an efficient algorithm devoted to the extraction of delta-free sequential patterns. Furthermore, we show the advantage of the delta-free sequences and highlight their importance when building sequence classifiers, and we show how they can be used to address the feature selection problem in statistical classifiers, as well as to build symbolic classifiers which optimizes both accuracy and earliness of predictions. |
Mardi 10 Mars
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Multiband Robust Optimization: theory and applications |
Description: |
Fabio D'Andreagiovanni Over the last years, Robust Optimization (RO) has emerged as an effective and efficient methodology to tackle data uncertainty in real-world optimization problems. RO takes into account data uncertainty in the shape of hard constraints that restrict the feasible set and maintain only robust solutions, i.e. solutions that remain feasible even when the values of the input data change. In this talk, we provide an overview of our research about theory and applications of RO. Specifically, we present Multiband Robustness, a new model for RO that we recently proposed to generalize and refine the classical Gamma-robustness model by Bertsimas and Sim. The main aim of our new model is to provide a refined representation of arbitrary non- symmetric distributions of the uncertainty, that are commonly present in real-world applications. Such refined representation grants a reduction in conservatism of robust solutions, while maintaining the accessibility and computational tractability that have been a key factor of success of Gamma-robustness. We also provide an overview of applications of the Multiband model to real-world problems that we have considered in past and ongoing research and industrial projects. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Une généralisation des mots de Christoffel en dimension d. |
Description: |
Sébastien Labbé In this work, we extend the definition of Christoffel words todirected subgraphs of the hypercubic lattice in arbitrary dimensionthat wecall Christoffel graphs. Christoffel graphs when $d=2$ correspond towell-known Christoffel words.We show that Christoffel graphs have similar properties to those ofChristoffel words: symmetry of their central part and conjugation withtheirreversal. Our main result extends Pirillo's theorem (characterization ofChristoffel words which asserts that a word $amb$ is a Christoffelword if andonly if it is conjugate to $bma$) in arbitrary dimension.In the generalization, the map $ambmapsto bma$ is seen as a flipoperation ongraphs embedded in $mathbb{Z}^d$ and the conjugation is a translation.We show that a fully periodic subgraph of the hypercubic lattice is atranslate of its flip if and only if it is a Christoffel graph.This is joint work with Christophe Reutenauer.Preprint is available at http://arxiv.org/abs/1404.4021. |
Jeudi 12 Mars
Heure: |
12:15 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Extraction de motifs graduels pour le résumé de données numériques |
Description: |
Amal Oudni Les résumés linguistiques constituent une représentation linguistique décrivant un ensemble de données numériques en phrases simples, compréhensibles et facilement interprétables. Cet exposé se concentre sur les résumés linguistiques sous une forme particulière, appelée motifs graduels, exprimant des corrélations de co-variations des valeurs des attributs : on peut les illustrer pa r un exemple du type « plus l'âge du père est avancé à la naissance des enfants, plus le risque d'autisme chez les enfants augmente ».
Lors de mon exposé, je présenterai trois types de contextualisation de ces motifs graduels. Dans un premier temps, je décrirai le problème de motifs graduels contradictoires et une nouvelle approche permettant déviter toute ambiguïté entre motifs validés. Je présenterai ensuite la caractérisation des motifs graduels qui permet de faciliter l'interprétation des motifs générés en grand nombre en introduisant une nouvelle clause linguistiquement introduite par l'expression « surtout si ». Je terminerai par la présentation dune contextualisation qualifiant le mode de dépendances graduelles, en introduisant la notion d'accélération par rapport aux autres attributs.
Pour chacune des formes de motifs enrichis extraits, je présenterai une formalisation de la sémantique et l'interprétation souhaitées, des mesures de qualité pour évaluer et quantifier la validité des motifs proposés, ainsi que des algorithmes efficaces d'extraction automatique de ces motifs maximisant les critères de qualité définis. |
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Building Bridges Between Sets of Partial Orders |
Description: |
Hernán Ponce de León Partial orders are a fundamental mathematical structure capable of representing concurrency and causality on a set of atomic events. In many applications it is essential to consider multiple partial orders, each representing a particular behavioral scenario or an operating mode of a modeled system.
In this talk I will present two mathematical formalisms capable of the compressed representation of sets of partial orders: Labeled Event Structures (LESs) and Conditional Partial Order Graphs (CPOGs). I will demonstrate their advantages and disadvantages and propose efficient algorithms for transforming of a set of partial orders from a given compressed representation in one formalism into an equivalent representation in another formalism without the explicit enumeration of each scenario. These algorithms make use of an intermediate mathematical formalism, which we call Conditional Labeled Event Structures (CLESs), that combines the advantages of LESs and CPOGs.
This is joint work with Andrey Mokhov (Newcastle University) |
Vendredi 13 Mars
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Functors are Type Refinement Systems |
Description: |
Noam Zeilberger The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. In this joint work with Paul-André Melliès we propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact *any* functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors.
In the talk I want to motivate and introduce this general framework (which can also be seen as providing a categorical analysis of _refinement types_), and as a larger example give a sketch of how the framework can be used to formalize an elegant proof of a coherence theorem by John Reynolds. If time permits, I will also describe some of the natural questions raised by this perspective that are the subject of ongoing research. |
Mardi 17 Mars
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
ALEA, au CIRM (16-20 mars) |
Description: |
Journées ALEA |
Jeudi 19 Mars
Heure: |
12:15 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Calcul efficace de la stabilité des concepts formels |
Description: |
Sadok BEN YAHIA Dans l'ère des données massives, l'alliance de la qualité avec l'efficience pour la sélection des concepts formels « intéressants » serait une condition sine qua non. Dans ce cadre, la mesure de stabilité, de concepts formels, indiquerait dans quelle mesure l'intension de ce concept est liée à la présence d'objets particuliers dans son extension. Un concept stable possède, ainsi, une existence d'autant plus « réelle » que son intension ne dérive pas fortuitement d'une description bruitée de ses objets. Ainsi, les concepts stables sont très intéressants à localiser dans beaucoup de domaines puisqu'ils sont résistants au bruit, e.g., détection de communautés stables, classification par des classes monothétiques/ polythétiques.
Cependant, le calcul de la stabilité serait très couteux, ie., exponentiel en fonction de la taille de l'extension du concept. En effet, il faudrait explorer l'espace de tous les sous-ensembles de l'extension à la recherche qui restent fidèles à l'intension du concept formel.
Dans ce séminaire, nous passons en revue les très peu nombreux travaux qui se sont intéressés au calcul de la stabilité des concepts formels (organisés sous forme de treillis ou non). Ensuite, nous présentons des travaux récents sur l'exploitation des propriétés de monotonie et d'anti-monotonies des éléments clés dans l'espace de recherche. Ainsi, la saturation des cliques maximales non génératrices permet de traiter des espaces avoisinant les 215000. Nous montrons aussi que les identités d'inclusion/ exclusion servent au calcul efficace des stabilités des concepts formels organisés sous la forme d'un treillis. |
Heure: |
14:30 - 15:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Effective verification of low-level software with nested interrupts |
Description: |
Lihao Liang Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent advances in the encoding of the execution traces of interacting, concurrent threads. We assess the performance of our method on benchmarks drawn from embedded systems code and device drivers, and experimentally compare it to conventional formal approaches that use source-to-source transformations. Our experimental results show that our method significantly outperforms conventional techniques. To the best of our knowledge, our technique is the first to demonstrate effective formal verification of low-level embedded software with nested interrupts.
Joint work with Daniel Kroening, Tom Melham, Peter Schrammel and Michael Tautschnig |
Vendredi 20 Mars
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
An infinitary model of linear logic |
Description: |
Charles Grellois We construct an infinitary variant of the relational model of linear logic, where the exponential modality is interpreted as the set of finite or countable multisets. We explain how to interpret in this model the fixpoint operator Y as a Conway operator alternatively defined in an inductive or a coinductive way. We then extend the relational semantics with a notion of color or priority in the sense of parity games. This extension enables us to define a new fixpoint operator Y combining both inductive and coinductive policies. We conclude by sketching the connection between the resulting model of lambda-calculus with recursion and higher-order model-checking. |
Mardi 24 Mars
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Unit Commitment problems: approaches and solution algorithms |
Description: |
Claudio Gentile The Unit Commitment is a the problem to manage a set of power generating units of different types over a short time horizon. Unit Commitment is formulated as a Mixed Integer Nonlinear Programming problem. It requires special techniques to handle both the large size of the instances to be solved and the nonlinearity of the objective function. Two main approaches have been used in its solution: the Lagrangian Relaxation coupled with primal heuristics and MILP approximations. We discuss some new advancements for both approaches. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Automates d'arbres |
Description: |
Gwendal Collet |
Mercredi 25 Mars
Heure: |
14:00 - 15:00 |
Lieu: |
Amphi A |
Résumé: |
Extending Petri Nets with Object-Orientation |
Description: |
Charles Lakos This seminar will introduce the formalism of Petri Nets and their use in modelling and analysing concurrent systems. It will briefly mention some of the extensions of Petri Nets to achieve greater descriptive comfort. It will then report on work over a number of years to extend Petri Nets with Object-Oriented features, thereby making it easier to define polymorphic modules and to capture incremental development. The seminar will also describe the properties of such nets and the analysis possibilities. |
|
|