Dissecting ltlsynt
In Formal Methods in System Design
Abstract
ltlsynt is a tool for synthesizing a reactive circuit satisfying a specification expressed as an LTL formula. ltlsynt generally follows a textbook approach: the LTL specification is translated into a parity game whose winning strategy can be seen as a Mealy machine modeling a valid controller. This article details each step of this approach, and presents various refinements integrated over the years. Some of these refinements are unique to ltlsynt: for instance, ltlsynt supports multiple ways to encode a Mealy machine as an AIG circuit, features multiple simplification algorithms for the intermediate Mealy machine, and bypasses the usual game-theoretic approach for some subclasses of LTL formulas in favor of more direct constructions.
Experimenting with additive margins for contrastive self-supervised speaker verification
In Proceedings of the 24rd annual conference of the international speech communication association (interspeech 2023)
Abstract
Discrete Morse functions and watersheds
In Journal of Mathematical Imaging and Vision
Abstract
Any watershed, when defined on a stack on a normal pseudomanifold of dimension $d$, is a pure $(d-1)$-subcomplex that satisfies a drop-of-water principle. In this paper, we introduce Morse stacks, a class of functions that are equivalent to discrete Morse functions. We show that the watershed of a Morse stack on a normal pseudomanifold is uniquely defined, and can be obtained with a linear-time algorithm relying on a sequence of collapses. Last, we prove that such a watershed is the cut of the unique minimum spanning forest, rooted in the minima of the Morse stack, of the facet graph of the pseudomanifold.
Introducing PC $n$-manifolds and $P$-well-composedness in partially ordered sets
In Journal of Mathematical Imaging and Vision
Abstract
In discrete topology, discrete surfaces are well-known for their strong topological and regularity properties. Their definition is recursive, and checking if a poset is a discrete surface is tractable. Their applications are numerous: when domain unicoherence is ensured, they lead access to the tree of shapes, and then to filtering in the shape space (shapings); they also lead to Laplacian zero-crossing extraction, to brain tumor segmentation, and many other applications related to mathematical morphology. They have many advantages in digital geometry and digital topology since discrete surfaces do not have any pinches (and then the underlying polyhedron of their geometric realization can be parameterized). However, contrary to topological manifolds known in continuous topology, discrete surfaces do not have any boundary, which is not always realizable in practice (finite hyper-rectangles cannot be discrete surfaces due to their non-empty boundary). For this reason, we propose the three following contributions: (1) we introduce a new definition of boundary, called border, based on the definition of discrete surfaces, and which allows us to delimit any partially ordered set whenever it is not embedded in a greater ambient space, (2) we introduce $P$-well-composedness similar to well-composedness in the sense of Alexandrov but based on borders, (3) we propose new (possibly geometrical) structures called (smooth) $n$-PCM’s which represent almost the same regularity as discrete surfaces and that are tractable thanks to their recursive definition, and (4) we prove several fundamental theorems relative to PCM’s and their relations with discrete surfaces. We deeply believe that these new $n$-dimensional structures are promising for the discrete topology and digital geometry fields.
TTProfiler: Types and terms profile building for online cultural heritage knowledge graphs
In J. Comput. Cult. Herit.
Abstract
As more and more knowledge graphs (KG) are published on the Web, there is a need for tools that show their content. This implies showing the schema-level patterns instantiated in the graph, but also the terms used to qualify its entities. In this article, we present a new profiling tool that we call TTprofiler. It shows the predicates that relate types in the KG, and also the terms present in this KG, because of their paramount importance in most KGs, especially in the Cultural Heritage (CH) domain. We recall the role of terminologies and how they are implemented and used on the Web, we give the algorithm for building a TT profile from an online KG’s Endpoint, and we report on experiments performed over a set of Cultural Heritage Web KGs. A tool for visualizing TT profiles is also provided.
The Mealy-machine reduction functions of Spot
In Science of Computer Programming
Abstract
We present functions for reducing Mealy machines, initially detailed in our FORTE’22 article. These functions are now integrated into Spot 2.11.2, where they are used as part of the ltlsynt tool for reactive synthesis. Of course, since Spot is a library, these functions can also be used on their own, and we provide Python bindings for easy experiments. The reproducible capsule benchmarks these functions on Mealy machines from various sources, and compare them to the MeMin tool.
Création d’un graphe de connaissances géohistorique à partir d’annuaires du commerce parisien du 19 ème siècle: Application aux métiers de la photographie
In 34es journées francophones d’ingénierie des connaissances (IC 2023) @ plate-forme intelligence artificielle (PFIA 2023)
Abstract
Les annuaires professionnels anciens, édités à un rythme soutenu dans de nombreuses villes européennes tout au long des XIXe et XXe si‘ecles, forment un corpus de sources unique par son volume et la possibilité qu’ils donnent de suivre les transformations urbaines à travers le prisme des activités professionnelles des habitants, de l’échelle individuelle jusqu’à celle de la ville enti‘ere. L’analyse spatiotemporelle d’un type de commerces au travers des entrées d’annuaires demande cependant un travail considérable de recensement, de transcription et de recoupement manuels. Pour pallier cette difficulté, cet article propose une approche automatique pour construire et visualiser un graphe de connaissances géohistorique des commerces figurant dans des annuaires anciens. L’approche est testée sur des annuaires du commerce parisien du XIXe si‘ecle allant de 1799 à 1908, sur le cas des métiers de la photographie.
On the historical evolution of the performance versus cost ratio of Raspberry Pi computers
In Conférence francophone d’informatique en parallélisme, architecture et système (compas 2023)
Abstract
This article aims to analyze the historical evolution of the cost/performance ratio of the Raspberry Pi family of computers, given their representativeness in the field of single-board computers. While comparing the cost/performance ratio of different models of single-board computers is not a new idea, there are no studies focused on evaluating the performance evolution and associated costs of all generations of the Raspberry Pi B line. Our analysis considered all generations of Raspberry Pi B line available on the market until 2023, and we adjusted computer prices based on the 2012 dollar value, the year of the first Raspberry Pi’s launch. The results indicate a clear trend of increasing performance over time, accompanied by a tendency for the price paid for performance to decrease. This reduction becomes even more pronounced when considering the depreciation of the dollar compared to its value in 2012.
Security threats, countermeasures, and challenges of digital supply chains
In ACM Computing Surveys
Abstract
The rapid growth of Information Communication Technologies (ICT) has impacted many fields. In this context, the supply chain has also quickly evolved toward the digital supply chain where digital and electronic technologies have been integrated into every aspect of its end-to-end process. This evolution provides numerous beneits such as proit maximization, loss reduction, and the optimization of supply chain lead times. However, the use of such technologies has also considerably opened up various security threats and risks which have widened the attack surface on the entire end-to-end supply chain. We present a holistic survey on supply chain security. We discuss the different security issues and attacks that target the diferent supply chain technologies. Then, we discuss various countermeasures and security solutions proposed by academic and industry researchers to mitigate the identiied threats. Finally, we provide some recommendations and best practices that can be adopted to achieve a secure supply chain.