Hugo Bazille

Logic and languages of higher-dimensional automata

By Amazigh Amrane, Hugo Bazille, Uli Fahrenberg, Marie Fortin

2024-10-10

In Proceedings of the 28th international conference on developments in language theory (DLT’24)

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

By Sundararaman Akshay, Hugo Bazille, Blaise Genest, Mihir Vahanwala

2024-10-10

In Logical Methods in Computer Science

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

Presenting interval pomsets with interfaces

By Amazigh Amrane, Hugo Bazille, Emily Clement, Uli Fahrenberg, Krzysztof Ziemianski

2024-10-10

In Proceedings of the 21st international conference on relational and algebraic methods in computer science (RAMiCS’24)

Abstract

Interval-order partially ordered multisets with interfaces (ipomsets) have shown to be a versatile model for executions of concur- rent systems in which both precedence and concurrency need to be taken into account. In this paper, we develop a presentation of ipomsets as generated by a graph of certain discrete ipomsets (starters and terminators) under the relation which composes subsequent starters and subsequent ter- minators. Using this presentation, we show that also subsumptions are generated by elementary relations. We develop a similar correspondence on the automata side, relating higher-dimensional automata, which gen- erate ipomsets, and ST-automata, which generate step sequences, and their respective languages.

Continue reading

Closure and decision properties for higher-dimensional automata

By Amazigh Amrane, Hugo Bazille, Uli Fahrenberg, Krzysztof Ziemiański

2023-12-01

In 20th international colloquium on theoretical aspects of computing (ICTAC’23)

Abstract

Continue reading

Languages of higher-dimensional timed automata

By Amazigh Amrane, Hugo Bazille, Emily Clement, Uli Fahrenberg

2023-05-22

In Proceedings of the 45th international conference on application and theory of petri nets and concurrency (PN’24)

Abstract

We present a new language semantics for real-time concurrency. Its operational models are higher-dimensional timed automata (HDTAs), a generalization of both higher-dimensional automata and timed automata. We define languages of HDTAs as sets of interval-timed pomsets with interfaces. As an application, we show that language inclusion of HDTAs is undecidable. On the other hand, using a region construction we can show that untimings of HDTA languages have enough regularity so that untimed language inclusion is decidable.

Continue reading

On robustness for the Skolem and positivity problems

By S. Akshay, Hugo Bazille, Blaise Genest, Mihir Vahanwala

2022-07-07

In 39th international symposium on theoretical aspects of computer science STACS

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 configuration? 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 “uninitialized” 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).

Continue reading