Publications

Type-checking heterogeneous sequences in a simple embeddable type system

Abstract

Heterogeneously typed sequences are supported in a wide range of programming languages, both dynamically and statically typed. These sequences often exhibit type patterns such as repetition, alternation, and optionality. The programmer needs a mechanism to declare and query adherence to this regularity. The theory of finite automata over finite alphabets was conceived for characterizing patterns in so-called regular languages, but does not exactly meet this challenge, because the set of potential elements of the sequences is infinite. In this article, we present a generalization of regular expressions called rational type expressions as a means of declaring regular patterns in heterogeneous sequences. We present procedures for constructing and manipulating symbolic finite automata, a generalization of classical finite automata, using a portable, simple, embeddable, type system. For type systems with subtyping, the subtype relation and type vacuity cannot always be computed programmatically. We provide a working, sound solution for constructing finite automata for type-based regular expressions even in cases where the subtype decidability relations is not computable retrospectively, but can be ensured by construction. We demonstrate the generality and portability of the system by providing implementations in Common Lisp, Clojure, Scala, and Python.

Continue reading

$\omega$-regular energy problems

Abstract

We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a Büchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm 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 platforms TChecker and Spot.

Continue reading

Bisimulations and logics for higher-dimensional automata

Abstract

Continue reading

Dense in situ underwater 3D reconstruction by aggregation of successive partial local clouds

Abstract

Assessing the completeness of an underwater 3D reconstruction on-site is crucial as it allows for rescheduling acquisitions, which capture missing data during a mission, avoiding additional costs of a subsequent mission. This assessment needs to rely on a dense point cloud since a sparse cloud lacks detail and a triangulated model can hide gaps. The challenge is to generate a dense cloud with field-deployable tools. Traditional dense reconstruction methods can take several dozen hours on low-capacity systems like laptops or embedded units. To speed up this process, we propose building the dense cloud incrementally within an SfM framework while incorporating data redundancy management to eliminate recalculations and filtering already-processed data. The method evaluates overlap area limits and computes depths by propagating the matching around SeaPoints—the keypoints we design for identifying reliable areas regardless of the quality of the processed underwater images. This produces local partial dense clouds, which are aggregated into a common frame via the SfM pipeline to produce the global dense cloud. Compared to the production of complete dense local clouds, this approach reduces the computation time by about 70 percent while maintaining a comparable final density. The underlying prospect of this work is to enable real-time completeness estimation directly on board, allowing for the dynamic re-planning of the acquisition trajectory.

Continue reading

Kleene theorem for higher-dimensional automata

Abstract

Continue reading

PeGazUs: A knowledge graph based approach to build urban perpetual gazetteers

Abstract

Continue reading

A simple yet effective interpretable bayesian personalized ranking for cognitive diagnosis

Abstract

In the field of education, the automatic assessment of student profiles has become a crucial objective, driven by the rapid expansion of online tutoring systems and computerized adaptive testing. These technologies aim to democratize education and enhance student assessment by providing detailed insights into student profiles, which are essential for accurately predicting the outcomes of exercises, such as solving various types of mathematical equations. We aim to develop a model capable of predicting responses to a large set of questions within the Multi-Target Prediction framework while ensuring that this model is explainable, allowing us to quantify student performance in specific knowledge areas. Existing cognitive diagnosis algorithms often struggle to meet the dual requirement of accurately predicting exercise outcomes and maintaining interpretability. To address this challenge, we propose an alternative to the complexity of current advanced machine learning models. Instead, we introduce a direct yet highly effective Bayesian Personalized Ranking algorithm, called CD-BPR, which incorporates interpretability as a core learning objective. Extensive experiments demonstrate that CD-BPR not only performs better in predicting exercise outcomes but also provides superior interpretability of estimated student profiles, thus fulfilling both key requirements.

Continue reading

Attention-based cloth manipulation from model-free topological representation

Abstract

The robotic manipulation of deformable objects, such as clothes and fabric, is known as a complex task from both the perception and planning perspectives. Indeed, the stochastic nature of the underlying environment dynamics makes it an interesting research field for statistical learning approaches and neural policies. In this work, we introduce a novel attention- based neural architecture capable of solving a smoothing task for such objects by means of a single robotic arm. To train our network, we leverage an oracle policy, executed in simulation, which uses the topological description of a mesh of points for representing the object to smooth. In a second step, we transfer the resulting behavior in the real world with imitation learning using the cloth point cloud as decision support, which is captured from a single RGBD camera placed egocentrically on the wrist of the arm. This approach allows fast training of the real-world manipulation neural policy while not requiring scene reconstruction at test time, but solely a point cloud acquired from a single RGBD camera. Our resulting policy first predicts the desired point to choose from the given point cloud and then the correct displacement to achieve a smoothed cloth. Experimentally, we first assess our results in a simulation environment by comparing them with an existing heuristic policy, as well as several baseline attention architectures. Then, we validate the performance of our approach in a real-world scenario

Continue reading

Logic and languages of higher-dimensional automata

Abstract

In this paper we study finite higher-dimensional automata (HDAs) from the logical point of view. Languages of HDAs are sets of finite bounded-width interval pomsets with interfaces (iiPoms$\le k$) closed under order extension. We prove that languages of HDAs are MSO-definable. For the converse, we show that the order extensions of MSO-definable sets of iiPoms$\le k$ are languages of HDAs. Furthermore, both constructions are effective. As a consequence, unlike the case of all pomsets, the order extension of any MSO-definable set of iiPoms$\le k$ is MSO-definable.

Continue reading

On robustness for the skolem, positivity and ultimate positivity problems

Abstract

The Skolem problem is a long-standing open problem in linear dynamical systems: can a linear recurrence sequence (LRS) ever reach 0 from a given initial config- uration? Similarly, the positivity problem asks whether the LRS stays positive from an initial configuration. Deciding Skolem (or positivity) has been open for half a century: the best known decidability results are for LRS with special properties (e.g., low order recurrences). On the other hand, these problems are much easier for “uninitialised”uninitialised variants, where the initial configuration is not fixed but can vary arbitrarily: checking if there is an initial configuration from which the LRS stays positive can be decided by polynomial time algorithms (Tiwari in 2004, Braverman in 2006).In this paper, we consider problems that lie between the initialised and uninitialised variants. More precisely, we ask if 0 (resp. negative numbers) can be avoided from every initial configuration in a neighbourhood of a given initial configuration. This can be considered as a robust variant of the Skolem (resp. positivity) problem. We show that these problems lie at the frontier of decidability: if the neighbourhood is given as part of the input, then robust Skolem and robust positivity are Diophantine hard, i.e., solving either would entail major breakthroughs in Diophantine approximations, as happens for (non-robust) positivity. Interestingly, this is the first Diophantine hardness result on a variant of the Skolem problem. On the other hand, if one asks whether such a neighbourhood exists, then the problems turn out to be decidable in their full generality, with PSPACE complexity. Our analysis is based on the set of initial configurations such that positivity holds, which leads to new insights into these difficult problems, and interesting geometrical interpretations.Our techniques also allow us to tackle robustness for ultimate positivity, which asks whether there is a bound on the number of steps after which the LRS remains positive. There are two natural robust variants depending on whether we ask for a “uniform”uniform bound on this number of steps, independent of the starting configuration in the neighbourhood. We show that for the uniform variant, results are similar to positivity. On the other hand, for the non-uniform variant, robust ultimate positivity has different properties when the neighbourhood is open and when it is closed. When it is open, the problem turns out to be tractable, even when the neighbourhood is given as part of the input.

Continue reading