We present an algorithm to learn a deterministic timed automaton (DTA) via membership and equivalence queries. Our algorithm is an extension of the L* algorithm with a Myhill-Nerode style characterization of recognizable timed languages, which is the class of timed languages recognizable by DTAs. We first characterize the recognizable timed languages with a Nerode-style congruence. Using it, we give an algorithm with a smart teacher answering symbolic membership queries in addition to membership and equivalence queries. With a symbolic membership query, one can ask the membership of a certain set of timed words at one time. We prove that for any recognizable timed language, our learning algorithm returns a DTA recognizing it. We show how to answer a symbolic membership query with finitely many membership queries. We also show that our learning algorithm requires a polynomial number of queries with a smart teacher and an exponential number of queries with a normal teacher. We applied our algorithm to various benchmarks and confirmed its effectiveness with a normal teacher.

In graph theory, a dynamic network can be understood as a global underlying graph whose edges are allowed to become temporarily unavailable at times. Extending Courcelle-like meta theorems to such a temporal setting is an important and challenging open question.

Without the consideration of temporality, a good number of width parameters has been introduced in the effort to better understand what lies between cliquewidth (number of different neighbourhoods) and treewidth (total size of neighbourhoods). We can cite rankwidth, bimodule-width, booleanwidth, and matching-width for the first category; and minor-based parameters such as Hajos/Hadwiger number and twinwidth for the second one. However, attempts in extending those parameters to temporal graphs are still scarce in the literature.

Twins in a temporal context would refer to vertices which are substitutes for each other in the solution of a number of classical graph problems, e.g. matching, epidemic spreading, journeys of optimal (temporal) length, and so on. Although most of these problems become NP-hard to optimise on an arbitrary input, we present in this talk an example where reducing a spatiotemporal input into a timeless graph and using both geometric and decomposition properties help in obtaining a PTAS solution. We hope this kind of technique could help in solving problems beyond first order logic when exploiting the conformist nature of twins.

We show that n-bit integers can be factorized by independently running a quantum circuit with $\tilde{O}(n^{3/2})$ gates for $\sqrt{n}+4$ times, and then using polynomial-time classical post-processing. In contrast, Shor's algorithm requires circuits with $\tilde{O}(n^2)$ gates. The correctness of our algorithm relies on a number-theoretic heuristic assumption reminiscent of those used in subexponential classical factorization algorithms. It is currently not clear if the algorithm can lead to improved physical implementations in practice.

No background in quantum computation will be assumed.

Based on the recent arXiv preprint: https://arxiv.org/abs/2308.06572

https://semflajolet.math.cnrs.fr/ Exceptionnellement à 14 heures.

Titles and abstracts available at: https://chocola.ens-lyon.fr/events/meeting-2023-09-28/

We present a layered approach to solve a multi-agent control problem. This methods mixes three domains: timed automata, SMT and reinforcement learning, in order to obtain the best of each: the method based on timed automata solves the combinatorial aspect of the problem, the SMT refine our model into a more realistic one and the two methods are combined into a SWA-SMT solver. Finally, the Reinforcment Learning trains the policy in order to show that the initial dataset generated with the the SWA-SMT solver is crucial for the overall success of the method.

Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building 'closures' pairing the transformed functions with the 'environment' of their free variables. Abstract machines rely on similar and yet different concepts of 'closures' and 'environments'.

In this talk, we analyze the relationship between the two approaches. We adopt a very simple lambda-calculus with tuples as source language and study abstract machines for both the source language and the target of closure conversion.

We overview three contributions. Firstly, a new simple proof technique for the correctness of closure conversion, inspired by abstract machines. Secondly, we show how the closure invariants of the target language allow us to design a new way of handling environments in abstract machines, not suffering the shortcomings of other styles. Thirdly, we analyze the machines from the point of view of sharing and time complexity, dissecting how different aspects of closure conversion impact on the cost of the execution.

Church’s Problem asks for the construction of a procedure which, given a logical specification φ(I, O) between input ω-strings I and output ω-strings O, determines whether there exists an operator F that implements the specification in the sense that φ(I, F(I)) holds for all inputs I. Büchi and Landweber gave a procedure to solve Church’s problem for MSO specifications and operators computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time of the non-negative reals. It turns out that in the continuous time there are phenomena which are very different from the canonical discrete time domain of the natural numbers.

We study a variant of the widely popular, fast, and often used family of community detection procedures referred to as label propagation algorithms. These mechanisms also exhibit many parallels with models of opinion exchange dynamics and consensus mechanisms in distributed computing.

Initially, given a network, each vertex starts with a random label in the interval [0,1]. Then, in each round of the algorithm, every vertex switches its label to the majority label in its neighborhood (including its own label). At the first round, ties are broken towards smaller labels, while at each of the next rounds, ties are broken uniformly at random.

We investigate the performance of this algorithm on the binomial random graph G(n,p). Via a technically delicate analysis, we show that for np>n^(5/8+epsilon), the algorithm terminates with a single label a.a.s. Moreover, we show that if np = omega(n^(2/3)), a.a.s., this label is the smallest one, whereas if n^(5/8+epsilon) < np = o(n^(2/3)), the surviving label is, a.a.s., not the smallest one.

Joint work with Lyuben Lichev (Univ. Jean Monnet), Dieter Mitsche (Univ. Jean Monnet & Pontifícia Univ. Católica de Chile), and Pawel Pralat (Toronto Metropolitan Univ.).