Publications

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

By Didier Verna

2023-09-01

In TUGboat

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.

Continue reading

Layered controller synthesis for dynamic multi-agent systems

By Emily Clement, Nicolas Perrin-Gilbert, Philipp Schlehuber-Caissier

2023-09-01

In Proceedings of the 21st international conference on formal modeling and analysis of timed systems (FORMATS’23)

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.

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

Discrete Morse functions and watersheds

By Gilles Bertrand, Nicolas Boutry, Laurent Najman

2023-08-10

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.

Continue reading

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

By Nicolas Boutry

2023-08-01

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.

Continue reading

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

By Lamine Diop, Béatrice Markhoff, Arnaud Soulet

2023-07-15

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.

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

On the historical evolution of the performance versus cost ratio of raspberry pi computers

By David Beserra, Nida Meddouri, Célia Restes, Anys Nait Zerrad, Basma Bouharicha, Aurore Duvernoy

2023-07-01

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.

Continue reading

Structural and spectral analysis of dynamic graphs for attack detection

By Majed Jaber, Nicolas Boutry, Pierre Parrend

2023-07-01

In Rencontre des jeunes chercheurs en inteligence artificielle (RJCIA-2023)

Abstract At this time, cyberattacks represent a constant threat. Many approaches exist for detecting suspicious behaviors, but very few of them seem to benefit from the huge potential of mathematical approaches like spectral graph analysis, known to be able to extract topological features of a graph using its Laplacian spectrum. For this reason, we consider our network as a dynamic graph composed of nodes (representing the devices) and of edges (representing the requests), and we compute its Laplacian spectrum across time.

Continue reading