Publications

In Pattern Recognition

Abstract Interactive image segmentation is an important application in computer vision for selecting objects of interest in images. Several interactive segmentation methods are based on distance transform algorithms. However, the most known distance transform, geodesic distance, is sensitive to noise in the image and to seed placement. Recently, the Dahu pseudo-distance, a continuous version of the minimum barrier distance (MBD), is proved to be more powerful than the geodesic distance in noisy and blurred images.

A Myhill-Nerode theorem for higher-dimensional automata

By Uli Fahrenberg, Krzysztof Ziemiański

2023-03-01

In Application and theory of petri nets and concurrency (PETRI NETS)

Abstract 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.

Catoids and modal convolution algebras

By Uli Fahrenberg, Christian Johansen, Georg Struth, Krzysztof Ziemiański

2023-03-01

In Algebra Universalis

Abstract 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.

Energy problems in finite and timed automata with Büchi conditions

By Sven Dziadek, Uli Fahrenberg, Philipp Schlehuber-Caissier

2023-03-01

In International symposium on formal methods (FM)

Abstract 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.

Modern vectorization and alignement of historical maps: An application to paris atlas (1789-1950)

By Yizi Chen

2023-03-01

In

Abstract 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.

Optimization of the product configuration system of renault

By Hao Xu, Souheib Baarir, Tewfik Ziadi, Yves Bossu Siham Essodaigui, Lom Messan Hillah

2023-03-01

In SAC ’23: The 38th ACM/SIGAPP symposium on applied computing

Abstract

Towards better heuristics for solving bounded model checking problems

By Anissa Kheireddine, Étienne Renault, Souheib Baarir

2023-03-01

In Constraints

Abstract 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.

Go2Pins: A framework for the LTL verification of Go programs (extended version)

By Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault

2023-02-01

In International Journal on Software Tools for Technology Transfer (STTT)

Abstract 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.

CosySEL: Improving SAT solving using local symmetries

By S. Saouli, S. Baarir, C. Dutheillet, J. Devriendt

2023-01-01

In 24th international conference on verification, model checking, and abstract interpretation

Abstract Many satisfiability problems exhibit symmetry properties. Thus, the development of symmetry exploitation techniques seems a natural way to try to improve the efficiency of solvers by preventing them from exploring isomorphic parts of the search space. These techniques can be classified into two categories: dynamic and static symmetry breaking. Static approaches have often appeared to be more effective than dynamic ones. But although these approaches can be considered as complementary, very few works have tried to combine them.

Forecasting electricity prices: An optimize then predict-based approach

By Léonard Tschora, Erwan Pierre, Marc Plantevit, Céline Robardet

2023-01-01

In Advances in intelligent data analysis XXI

Abstract We are interested in electricity price forecasting at the European scale. The electricity market is ruled by price regulation mechanisms that make it possible to adjust production to demand, as electricity is difficult to store. These mechanisms ensure the highest price for producers, the lowest price for consumers and a zero energy balance by setting day-ahead prices, i.e. prices for the next 24h. Most studies have focused on learning increasingly sophisticated models to predict the next day’s 24 hourly prices for a given zone.

The Dahu graph-cut for interactive segmentation on 2D/3D images

A Myhill-Nerode theorem for higher-dimensional automata

Catoids and modal convolution algebras

Energy problems in finite and timed automata with Büchi conditions

Modern vectorization and alignement of historical maps: An application to paris atlas (1789-1950)

Optimization of the product configuration system of renault

Towards better heuristics for solving bounded model checking problems

Go2Pins: A framework for the LTL verification of Go programs (extended version)

CosySEL: Improving SAT solving using local symmetries

Forecasting electricity prices: An optimize then predict-based approach

Search

Tags