During my thesis, I studied a subclass of Petri nets called observation Petri nets. The complexity results obtained show that this class is particularly suited for checking parameterized properties, where the parameter is the number of tokens present in the net. Observation Petri nets were introduced for their application to population protocols, a distributed computing model. Population protocols are part of a class of models of concurrent systems in which we are interested in parameterized verification, and in which there are identical agents which synchronize through “simple” communication primitives. I studied other models of this class, like reconfigurable broadcast networks and register protocols and in the future I would like to turn my research towards the analysis of these kinds of distributed systems for which the parameterized problems are not immediately undecidable, broadening the range of formal method techniques used.

Stone spaces appear at the interface of computer science, logic and general mathematics. In this talk, we will give a gentle introduction to Stone spaces, distilling a few key examples that illustrate their peculiarities in an accessible way. We will also be hinting towards Stone duality and other related topics, such as applications in automata theory. No prerequisites.

Software interoperability is a recurring issue in nearly every bigger software project where two or more (legacy) software systems are involved. One aspect of interoperability, that is considered especially tricky is semantic interoperability, i.e., aligning the concepts, entities, data structures from multiple systems with each other. The model-driven software engineering community has investigated this issue under different names: model management, model synchronisation, inter-model consistency. From a theoretical side, there are two noteworthy common approaches: Goguen’s Colimit-approach (for general systems' theory) and Triple Graph Grammars (TGGs). The former describes that idea that one may always consider a “global integrated system” as the colimit of a diagram of interacting systems, while the latter is the foundation for a powerful framework of binary model synchronizers derived from a declarative description (grammar). In our investigation, it, however, turned out that both approaches each have significant drawback when considering them in practical applications: The colimit turns out to be a “forgetful” operation and TGGs are limited to a binary setting (it is a well-known fact from logic and databases that there are multi-ary relations that cannot be factored into a system of binary relations). Thus, we invented a novel formalism, called comprehensive systems, first introduced in [1]( https://link.springer.com/chapter/10.1007/978-3-030-45234-6_17), and theoretically flashed out in [2]( https://dl.acm.org/doi/10.1007/s00165-021-00555-2) and [3]( https://linkinghub.elsevier.com/retrieve/pii/S0304397521004059). Comprehensive systems provide an alternative to the colimit approach, which can be thought of as instead of “merging” a diagram into a singular object, they “flatten” the whole diagram. Moreover, they are designed for a general n-ary ($n \geq 2$) settings and thus can be considered as a generalization of triple graphs. In a series of papers, we have shown that comprehensive systems admit SPO and DPO rewriting in the setting of a weak adhesive HLR category. From a practical perspective, comprehensive systems serve as the theoretical foundation of a prototypical software interoperability tool called [CorrLang](https://corrlang.io).

In this talk, I will provide a brief historical overview over interoperability, model management, and model synchronisation, provide the motivation for comprehensive systems, sketch their theoretical properties (with an emphasis on partial morphisms), and, if time allows, demonstrate how comprehensive systems are reified in a concrete tool (CorrLang).

Zoom meeting registration link

YouTube live stream

The capabilities of distributed systems in stochastic environments are inherently limited by the difficulty of efficiently circulating information. Additional limitations may arise whenever the entities making up these systems are competing against each others. To better understand these limitations, my thesis presents and analyses several idealised models, inspired by biological scenarios.

In this talk, I will present a counter-intuitive result that is reminiscent of Braess' paradox, albeit in the context of social foraging rather than network flows. Then, motivated by flocking scenarios, I will discuss the feasibility of alignment in the presence of drift noise. Finally, I will consider the self-stabilizing bit-dissemination problem, modelling the challenge of efficiently spreading information while reaching a consensus when communications are extremely constrained.

Overall, this presentation will aim to offer fresh insights into the capabilities of distributed and competitive biological systems, shedding new light on their potential and limitations.

To design efficient algorithms for combinatorial optimization, it is desirable, given a polytope, to find more compact formulations which are faster to handle, when they exist. Extension complexity of P is defined as the minimal size of an affine lift. In the nineties, Yannakakis characterized this complexity in terms of the slack matrix of the polytope. Slack matrices allow to derive upper bounds, when a succinct factorization is found (as for the regular n-gon in [FRT12]), or lower bounds, which can be deduced via a lower bound on the rectangle cover (correlation polytope, Kaibel and Weltge, 2014), or via more sophisticated techniques, as Fiorini's hyperplane separation lemma and entropy arguments à la Razborov (matching polytope, Rothvoss 2017). Faenza et al. (2011) gave an alternative characterization of extension complexity via certain randomised two-party protocols.

In this thesis, we propose a different model for randomised protocols, with a more flexible structure. The characterization still holds, and it additionally holds in the symmetric setting: there is a one-to-one correspondence between G-symmetric randomised protocols guessing P, and G-symmetric extensions of P. We also established an (affine) connection between two known extensions of the permutahedron (by Goemans and by Fiorini et al.), and by analogy we construct a simple extension of the regular n-gon, which turns out to be a section of the one obtained by factorization (in [FRT12]).

Two other independent works are presented in the thesis: in 2019, together with H. Fournier, G. Malod and S. Tavenas, we constructed a counter-example to a question asked by Nisan for monotone computations of non-commutative polynomials, via algebraic branching programs. Our construction also gave lower bounds for computing the elementary symmetric polynomials in the multilinear homogeneous setting. In 2018, C. Saroglou, I. Soprunov and A. Zvavitch have shown a characterization of the n-simplex as the only polytope minimizing a certain sup-ratio of mixed volumes related to the Fenchel inequality, and conjectured that the characterization holds among all convex bodies. I derived some necessary conditions on convex bodies to be minimizers, yielding a positive solution to this conjecture in R^3.

Quantum annealing (QA) holds promise for optimization problems in quantum computing, especially for combinatorial optimization. This analog framework attracts attention for its potential to address complex problems. Its gate-based homologous, QAOA with proven performance, has brought lots of attention to the NISQ era. Several numerical benchmarks try to classify these two metaheuristics however, classical computational power highly limits the performance insights. In this work, we introduce a new parametrized version of QA enabling a precise 1-local analysis of the algorithm. We develop a tight Lieb-Robinson bound for regular graphs, achieving the best-known numerical value to analyze QA locally. Studying MaxCut over cubic graph as a benchmark optimization problem, we show that a linear-schedule QA with a 1-local analysis achieves an approximation ratio over 0.7020, outperforming any known 1-local algorithms.

This talk starts with a result in classical Finite Automata Theory: 'Two regular languages with the same number of words for each length can be mapped one onto the other by a letter-to-letter (finite) transducer'.

The notion of generating function of regular languages leads to the introduction of the model of weighted automata. The conjugacy of weighted automata, a concept borrowed to symbolic dynamics, is then defined and it is shown how the above statement can be derived from the central result of this work: 'Two equivalent weighted automata are conjugate to a third onewhen the weight semiring is B, N, Z, or any Euclidean domain (and thus any (skew) field)'.

This talk is based on a joint work with Marie-Pierre Béal and Sylvain Lombardy.

10:00 - 10:50 Claudia Faggian, Higher Order Bayesian Networks, Exactly 10:50 - 11:10 Coffee break 11:10 - 12:00 Fredrik Dahlqvist, Sampling semantics for probabilistic programs 12:00 - 14:00 Lunch break 14:00 - 14:50 Pedro Azevedo de Amorim, Compositional Expected Cost Semantics for Functional Probabilistic Programs 14:50 - 15:40 Paul-André Melliès, Asynchronous template games and strategies 15:40 - 16:00 Coffee break 16:00 - 16:50 Guillaume Baudart, Schedule Agnostic Semantics for Reactive Probabilistic Programming 16:50 - 17:40 Thomas Ehrhard, A syntax for coherent differentiation