Maps have been a unique source of knowledge for centuries. Such historical documents provide invaluable information for analyzing complex spatial transformations over important time frames. This is particularly true for urban areas that encompass multiple interleaved research domains: humanities, social sciences, etc. The large amount and significant diversity of map sources call for automatic image processing techniques in order to extract the relevant objects as vector features. The complexity of maps (text, noise, digitization artifacts, etc.) has hindered the capacity of proposing a versatile and efficient raster-to-vector approaches for decades. In this thesis, we propose a learnable, reproducible, and reusable solution for the automatic transformation of raster maps into vector objects (building blocks, streets, rivers), focusing on the extraction of closed shapes. Our approach is built upon the complementary strengths of convolutional neural networks which excel at filtering edges while presenting poor topological properties for their outputs, and mathematical morphology, which offers solid guarantees regarding closed shape extraction while being very sensitive to noise. In order to improve the robustness of deep edge filters to noise, we review several, and propose new topology-preserving loss functions which enable to improve the topological properties of the results. We also introduce a new contrast convolution (CConv) layer to investigate how architectural changes can impact such properties. Finally, we investigate the different approaches which can be used to implement each stage, and how to combine them in the most efficient way. Thanks to a shape extraction pipeline, we propose a new alignment procedure for historical map images, and start to leverage the redundancies contained in map sheets with similar contents to propagate annotations, improve vectorization quality, and eventually detect evolution patterns for later analysis or to automatically assess vectorization quality. To evaluate the performance of all methods mentioned above, we released a new dataset of annotated historical map images. It is the first public and open dataset targeting the task of historical map vectorization. We hope that thanks to our publications, public and open releases of datasets, codes and results, our work will benefit a wide range of historical map-related applications.

We show how to efficiently solve energy Büchi problems in finite weighted automata and in one-clock weighted timed automata. Solving the former problem is our main contribution and is handled by a modified version of Bellman-Ford interleaved with Couvreur’s algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source tools TChecker and Spot.

We show how modal quantales arise as convolution algebras $Q^X$ of functions from catoids $X$, that is, multisemigroups with a source map $\ell$ and a target map $r$, into modal quantales $Q$, which can be seen as weight or value algebras. In the tradition of boolean algebras with operators we study modal correspondences between algebraic laws in $X$, $Q$ and $Q^X$. The class of catoids we introduce generalises Schweizer and Sklar’s function systems and object-free categories to a setting isomorphic to algebras of ternary relations, as they are used for boolean algebras with operators and substructural logics. Our results provide a generic construction of weighted modal quantales from such multisemigroups. It is illustrated by many examples. We also discuss how these results generalise to a setting that supports reasoning with stochastic matrices or probabilistic predicate transformers.

We establish a Myhill-Nerode type theorem for higher-dimensional automata (HDAs), stating that a language is regular precisely if it has finite prefix quotient. HDAs extend standard automata with additional structure, making it possible to distinguish between interleavings and concurrency. We also introduce deterministic HDAs and show that not all HDAs are determinizable, that is, there exist regular languages that cannot be recognised by a deterministic HDA. Using our theorem, we develop an internal characterisation of deterministic languages.

Explainable Artificial Intelligence (XAI) has received a lot of attention over the past decade, with the proposal of many methods explaining black box classifiers such as neural networks. Despite the ubiquity of recommender systems in the digital world, only few researchers have attempted to explain their functioning, whereas one major obstacle to their use is the problem of societal acceptability and trustworthiness. Indeed, recommender systems direct user choices to a large extent and their impact is important as they give access to only a small part of the range of items (e.g., products and/or services), as the submerged part of the iceberg. Consequently, they limit access to other resources. The potentially negative effects of these systems have been pointed out as phenomena like echo chambers and winner-take-all effects, because the internal logic of these systems is to likely enclose the consumer in a <i>deja vu</i> loop. Therefore, it is crucial to provide explanations of such recommender systems and to identify the user data that led the respective system to make the individual recommendations. This then makes it possible to evaluate recommender systems not only regarding their effectiveness (i.e., their capability to recommend an item that was actually chosen by the user), but also with respect to the diversity, relevance and timeliness of the active data used for the recommendation. In this paper, we propose a deep analysis of two state-of-the-art models learnt on four datasets based on the identification of the items or the sequences of items actively used by the models. Our proposed methods are based on subgroup discovery with different pattern languages (i.e., itemsets and sequences). Specifically, we provide interpretable explanations of the recommendations of the Top-N items, which are useful to compare different models. Ultimately, these can then be used to present simple and understandable patterns to explain the reasons behind a generated recommendation to the user.

This paper presents a new way to improve the performance of the SAT-based bounded model checking problem on sequential and parallel procedures by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approaches with two new heuristics for sequential procedures: Structure-based and Linear Programming heuristics. We extend these study and applied the above methodology on parallel approaches, especially to refine the sharing measure which shows promising results.

The problem of configuring a variability model is widespread in many different domains. Renault has developed its technology internally to model vehicle diversity. This technology relies on the approach known as knowledge compilation to explore the configurations space. However, the growing variability and complexity of the vehicles’ range hardens the space representation problem and impacts performance requirements. This paper tackles these issues by exploiting symmetries that represent isomorphic parts in the configurations space. A new method describes how these symmetries are exploited and integrated. The extensive experiments we conducted on datasets from the automobile manufacturer show our approach’s robustness and effectiveness: the achieved gain is a reduction of 52.13% in space representation on average.

We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin and Spot. Go2Pins is an effort to promote the integration of both formal verification and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware verification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. Moreover, in order to efficiently handle recursive programs, we introduce PSLRec, a formalism that augments PSL without changing the complexity of the underlying verification process.

Sans nier les risques de dépendance associés à la pratique des jeux d’argent, notre étude se fonde sur une enquête par questionnaire ethnographique menée auprès de joueurs amateurs de poker ayant une pratique relativement intensive mais limitée du jeu. à travers une analyse approfondie des données de cette enquête, nous avons d’abord cherché à mesurer l’intensité puis l’évolution de leur pratique en termes de mises, en ligne ou en live. Puis, nous avons confronté leur investissement à l’intérieur du jeu aux conditions d’existence et aux ressources dont ils disposent en dehors du jeu, au regard de leur genre, de leur diplôme et de leur catégorie socioprofessionnelle. Observant des disparités importantes dès leur initiation au jeu, nous avons alors découvert que les joueurs interrogés avaient progressivement tendance à réguler leur engagement monétaire en fonction de leurs conditions d’existence et des habitudes de mises de leur communauté de pratique.

Que se passe-t-il dans les toilettes des établissements scolaires, de l’école maternelle au lycée ? À partir d’enquêtes qualitatives, ce livre apporte un éclairage inédit sur le vécu des enfants et des jeunes dans ces "petits coins" de l’école et ce qu’il s’y joue, notamment en termes de relation adultes/enfants, de construction d’un rapport à soi, aux autres et de genre. Selon qu’ils sont "filles" ou "garons", "grands" ou "petits", comment les enfants se représentent-ils les toilettes scolaires et quels usages en ont-ils ? Comment investissent-ils (ou pas) ces lieux ? à mesure qu’ils grandissent, que les portes se ferment, que des murs s’élèvent et que la possibilité leur est offert de se retrouver seuls à l’abri du regard des autres, comment les enfants occupent-ils ces espaces collectifs et individuels, clos et ouverts ? Comment ceux-ci contribuent-ils à construire des corps, dans leur rapport à l’intimité et à l’autre, en tant que fille ou garon ? Comment les enfants et les jeunes s’y rencontrent-ils et quelles sociabilités peuvent-ils y développer à l’abri du regard des adultes ? La question du genre se révèle bien évidement centrale, dans ce lieu qui, à partir de l’école élémentaire, devient le seul espace "non mixte" dans la plupart des établissements scolaires mixtes.