|
|
Lundi 5 Novembre
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Learning to Navigate and Extract Information from Web Results |
Description: |
Ivan Vladimir MEZA In this talk I present our progress into the ECOS-NORD project between LIPN-Paris 13 and IIMAS-UNAM at Mexico. The talk focus on our experimental setup that allows to learn to navigate web results and to extract information from them. In particular, at this stage we are focus on extracting biográfical information of researchers, in order to quantify the Mexican returning diaspora. Our experimental setup is based on a reinforcement learning setup, we use a labelled data to learn the main actions on the results grid. We will show preliminary results, and newlines of experimentation. |
Heure: |
15:00 - 16:00 |
Lieu: |
Salle A303, bâtiment A, Université de Villetaneuse |
Résumé: |
State Compression Based on One-Sided Communications for Distributed Model Checking |
Description: |
Laure Petrucci We propose a distributed implementation of the collapse compression technique used by explicit state model checkers to reduce memory usage. This adapatation makes use of lock-free distributed hash tables based on one-sided communication primitives provided by libraries such as OpenSHMEM. We implemented this technique in the distributed version of the model checker Helena. We report on experiments performed on the Grid'5000 cluster with an implementation over OpenMPI. These reveal that, for some models, this distributed implementation can altogether preserve the memory reduction provided by collapse compression and reduce execution times by allowing the exchanges of compressed states between processes. |
Mardi 13 Novembre
Heure: |
12:30 - 13:30 |
Lieu: |
Salle A303, bâtiment A, Université de Villetaneuse |
Résumé: |
On importance splitting and the automation of rare event simulation |
Description: |
Carlos E. Budde In the analysis of formal models, simulation based approaches like statistical model checking offer a solution to the state space explosion that hinders verification, but may suffer from long execution times. This is exacerbated when the property value to approximate depends on an event seldom observed; in those cases rare event simulation (RES) techniques can speed up convergence by reducing the variance of the statistical estimator. However, RES techniques typically require non-trivial and domain-specific (or even model-specific) user input, which is a setback w.r.t. the push-button approach of standard model checking. In this talk I will briefly discuss methods to automate the implementation of a specific approach to RES called "importance splitting." I will overview some known implementations and discuss two algorithms recently developed to select "importance thresholds" and "splitting/effort factors," which are parameters with direct impact on the efficiency of importance splitting. A good performance of the outcomes of the algorithms proposed has been empirically demonstrated on several case studies. |
Jeudi 22 Novembre
Heure: |
10:30 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Soft modalities as prices: a game model for intuitionistic linear logic with subexponentials |
Description: |
Carlos Olarte We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game for aILL (affine intuitionistic linear logic), where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I to succeed. The game comes into full swing by using subexponentials for representing two types of options - volatile and permanent - for purchasing resources. This leads to a new type of subexponetial calculus where costs are attached to sequents. Different proofs are interpreted as more or less expensive strategies to obtain a certain resource from a bunch of resources (priced options). Finally, we generalize the concept of costs and option's prices in proofs by using a semiring structure. This general framework allows us to interpret a wider range of subexponential systems and give meaning to the use of resources in proofs in a more flexible way. |
Jeudi 29 Novembre
Heure: |
10:15 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Linear MSO and Church synthesis |
Description: |
Pierre Pradic |
|
|