Publications

Interactive and real-time typesetting for demonstration and experimentation: <span style="font-variant:small-caps;">ETAP</span>

Abstract

In general, typesetting experimentation is not a very practical thing to do. WYSIWYG typesetting systems are very reactive but do not offer highly configurable algorithms, and TeX, with its separate development / compilation / visualization phases, is not as interactive as its WYSIWYG competitors. Being able to experiment with typesetting algorithms interactively and in real-time is nevertheless desirable, for instance for demonstration purposes, or for rapid prototyping and debugging of new ideas. We present ETAP (Experimental Typesetting Algorithms Platform), a tool written to ease typesetting experimentation and demonstration. ETAP currently provides several paragraph justification algorithms, all with many configuration options such as kerning, ligatures, flexible spaces, sloppiness, hyphenation, etc. The resulting paragraph is displayed with many visual hints as well, such as paragraph, character, and line boxes, baselines, over/underfullness hints, hyphenation clues, etc. All these parameters, along with the desired paragraph width, are adjustable interactively through a GUI, and the resulting paragraph is displayed and updated in real-time. But ETAP can also be used without, or in conjunction with the GUI, as a scriptable application. In particular, it is able to generate all sorts of statistical reports or charts on the behavior of the various algorithms, for instance, the number of over/underfull boxes per paragraph width, the average compression or stretch ratio per line, whatever else you want. This allows you to quickly demonstrate or evaluate the comparative behavior or merits of the provided algorithms, or whichever you may want to add to the pool.

Continue reading

Layered controller synthesis for dynamic multi-agent systems

Abstract

In this paper we present a layered approach for multi-agent control problem, decomposed into three stages, each building upon the results of the previous one. First, a high-level plan for a coarse abstraction of the system is computed, relying on parametric timed automata augmented with stopwatches as they allow to efficiently model simplified dynamics of such systems. In the second stage, the high-level plan, based on SMT-formulation, mainly handles the combinatorial aspects of the problem, provides a more dynamically accurate solution. These stages are collectively referred to as the SWA-SMT solver. They are correct by construction but lack a crucial feature: they cannot be executed in real time. To overcome this, we use SWA-SMT solutions as the initial training dataset for our last stage, which aims at obtaining a neural network control policy. We use reinforcement learning to train the policy, and show that the initial dataset is crucial for the overall success of the method.

Continue reading

Open Access to Data about Silk Heritage: A Case Study in Digital Information Sustainability

Abstract

This article builds on work conducted and lessons learned within SILKNOW, a research project that aimed at enhancing the preservation and digital dissemination of silk heritage. Taking the project and this heritage typology as a case study in the digital transformation of cultural heritage institutions, it illustrates specific challenges that these institutions must face and demonstrates a few innovative answers to meet those challenges. The methodology combines approaches typical of the humanities and others usual in ICT, being inductive regarding materials and methods (consisting of a detailed review of existing online repositories and research projects devoted to textile heritage) and descriptive for the results and discussion (which explain at length the development of some tools and resources that responded to the needs detected in the previous analysis). The article reports on the state of the art and recent developments in the field of textile heritage, the tools implemented to allow the semantic access and text analysis of descriptive records associated with silk fabrics, and the spatiotemporal visualization of that information. Finally, it argues that institutional policies, namely the creation and free dissemination of open data related to cultural heritage are just as important as technical developments, showing why any future effort in these areas should take data sustainability, both in its technical and in institutional aspects, into account, since it is the most responsible and reasonable approach in terms of efficient resource allocation.

Continue reading

To cache or not to cache making pkg_add faster

Abstract

Continue reading

Dissecting ltlsynt

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.

Continue reading

Experimenting with additive margins for contrastive self-supervised speaker verification

Abstract

Continue reading

Discrete Morse functions and watersheds

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.

Continue reading

Introducing PC $n$-manifolds and $P$-well-composedness in partially ordered sets

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.

Continue reading

TTProfiler: Types and terms profile building for online cultural heritage knowledge graphs

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.

Continue reading

The Mealy-machine reduction functions of Spot

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.

Continue reading