arXiv subjects

Emily Clement

Publications and source records attributed to Emily Clement.

7 recordsLinked to original sources

arXiv2025

B\"uchi-Elgot-Trakhtenbrot Theorem for Higher-Dimensional Automata

In this paper we explore languages of higher-dimensional automata (HDAs) from an algebraic and logical point of view. Such languages are sets of finite width-bounded interval pomsets with interfaces (ipomsets) closed under order extension. We show that ipomsets can be represented as equivalence classes of words over a particular alphabet, called step sequences. We introduce an automaton model that recognize such languages. Doing so allows us to lift the classical B\"uchi-Elgot-Trakhtenbrot Theorem to languages of HDAs: we prove that a set of interval ipomsets is the language of an HDA if and only if it is simultaneously MSO-definable, of bounded width, and closed under order refinement.

cs.FL↗

arXiv2025

Property FA for random $\ell$-gonal groups

In the binomial $\ell$-gonal model for random groups, where the random relations all have fixed length $\ell\geq 3$ and the number of generators goes to infinity, we establish a double threshold near density $d=\frac{1}{\ell}$ where the group goes from being free to having Serre's property FA. As a consequence, random $\ell$-gonal groups at densities $\frac{1}{\ell} < d< \frac{1}{2}$ have boundaries homeomorphic to the Menger sponge, and $\frac{1}{\ell}$ is also the threshold for finiteness of $\mathrm{Out}(G)$. We also see that the thresholds for property FA and Kazhdan's property (T) differ when $\ell \geq 4$. Our methods are inspired by work of Antoniuk-Luczak-\'Swi\k{a}tkowski and Dahmani-Guirardel-Przytycki.

math.GR↗

arXiv2024

Kamp Theorem for Pomset Languages of Higher Dimensional Automata

Temporal logics are a powerful tool to specify properties of computational systems. For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages. In the case of words, Kamp's theorem states that First Order (FO) logic is as expressive as Linear Temporal Logic (LTL). In this paper, we extend this result to pomsets. To do so, we first investigate the class of pomset languages that are definable in FO. As expected, this is a strict subclass of MSO-definable languages. Then, we define a Linear Temporal Logic for pomsets, and show that it is equivalent to FO.

cs.FL↗

arXiv2024

Presenting Interval Pomsets with Interfaces

Interval-order partially ordered multisets with interfaces (ipomsets) have shown to be a versatile model for executions of concurrent 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 terminators. 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 generate ipomsets, and ST-automata, which generate step sequences, and their respective languages.

cs.FL↗

arXiv2024

Higher-Dimensional Timed Automata for Real-Time Concurrency

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. In real-time concurrent systems, both concurrency of events and timing and duration of events are of interest. Thus, HDTAs combine the non-interleaving concurrency model of higher-dimensional automata with the real-time modeling, using clocks, of timed automata. We define languages of HDTAs as sets of interval-timed pomsets with interfaces. 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. On a more practical note, we give new insights on when practical applications, like checking reachability, might benefit from using HDTAs instead of classical timed automata.

cs.FL↗

arXiv2023

Layered controller synthesis for dynamic multi-agent systems

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.

cs.AI↗

arXiv2020

Computing maximally-permissive strategies in acyclic timed automata

Timed automata are a convenient mathematical model for modelling and reasoning about real-time systems. While they provide a powerful way of representing timing aspects of such systems, timed automata assume arbitrary precision and zero-delay actions; in particular, a state might be declared reachable in a timed automaton, but impossible to reach in the physical system it models. In this paper, we consider permissive strategies as a way to overcome this problem: such strategies propose intervals of delays instead of single delays, and aim at reaching a target state whichever delay actually takes place. We develop an algorithm for computing the optimal permissiveness (and an associated maximally-permissive strategy) in acyclic timed automata and games.

cs.FL↗