Emily Clement

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

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

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