Distributed systems are collections of processes that collaborate. They are behind many modern services, from online banking to social media. A central challenge in these systems is achieving consensus among all computers or processes. This challenge is addressed by agreement algorithms. They play an important role in ensuring the smooth operation of a distributed system. These algorithms help to ensure and maintain consistency and reliability across the system.

In this thesis, our primary focus was on the k-set agreement problem. This problem is a generalization of the conventional consensus problem, it centers on achieving an agreement among processes, where the agreement is on at most k values, with k=1 being the consensus. The task made complex when certain processes either crash or exhibit unpredictable behavior, known as Byzantine behavior. Our objective was to clarify the conditions under which the k-set agreement can be resolved and to delineate its solvability limits.

A key achievement of this research is the comprehensive mapping of the solvability of the k-set agreement. Through new and improved algorithms, we have boosted the efficiency of k-set agreement, especially in environments characterized by Byzantine behaviors and bounded message delays, encapsulated in the Byzantine synchronous message passing system, both in authenticated and unauthenticated environment.

Although our primary focus was the Byzantine synchronous message passing system, we also explored asynchronous environments characterized by the unpredictability of message deliveries and potential process crashes. Here, we extended the solutions to address these challenges, filling gaps left by prior studies.

To summarize, our study offers an exhaustive analysis on the k-set agreement within a Byzantine Synchronous message passing system, through innovative and optimal algorithms.

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.

This manuscript is part of the field of formal verification, a computer science discipline aimed to ensure that programs are error-free. In this context, specification is one facet which consists of formally stating the properties the program has to satisfy. Our focus is on distributed algorithms which are particularly difficult to conceptualise. To tackle this problem, we explore data logic which is adapted to this purpose. In our framework, a data value is an element of a countable set, elements of structures have one or more data values and the logic can only test whether two data values are equal or not. The logics are analysed through the lens of the satisfiability problem. This work begins by exposing the state of the art concerning different logics on various structures such as words, multisets, data-words, data-multisets and graphs. Some identified gaps in the literature are filled, including missing proofs and unexplored cases. Additionally, two classical helpful tools in the analysis of the satisfiability problem are presented, namely Ehrenfeucht-Fraïssé games and domino problems. Afterwards, the main contribution of this work begins which is the definition and study of a new data logic, called the local fragment, introducing for this purpose the local modality. Inspired by the notion of locality and Gaifmans' graphs, our approach distinguishes itself by integrating locality in the definition of our logic, at the level of syntax. We show that our logic is indeed a fragment of first-order logic, as the local modality can be expressed in first-order logic. A sub-fragment called the existential fragment is also defined. Subsequently, our new logic from the point of view of the satisfiability problem is analysed; is identified criteria for which the logic is decidable and others for which it is not. Furthermore, in the cases where the logic is decidable, we try to analyse the complexity of the satisfiability problem, and succeeded in most of the cases.

Transducers are finite-state machines which compute functions (or relations) from words to words. They can be seen as simple programs with limited memory which manipulate strings. These machines have been studied for long in fundamental computer science as a part of automata theory, and are used in many areas such as compiling, natural language processing or stream processing.

Various transducer models have been defined in the literature, thanks to many features (such as non-determinism, two-wayness or nesting) which enable to increase the expressive power of the machines. In this setting, a natural question is to solve the related class membership problems: given a function computed by a transducer with “complex” features, can it be computed by a “simpler” transducer? Some of these problems have been solved in the literature, using somehow disparate proof techniques. They are generally considered as difficult. In practice, such problems can be interpreted as program optimization issues: given a program using a lot of resources, can we build a “more efficient” equivalent program?

This thesis solves various membership problems between existing classes of transductions, both over finite or infinite words. Among others, the celebrated models of two-way transducers and pebble transducers are investigated in detail. Each time, the membership procedure is non-trivial and turns out to be effective (in the sense that it builds a “simpler” transducer whenever it exists). Therefore our results can be considered as program optimization statements. Furthermore, we offer a systematic high-level strategy for solving these problems, which relies on semantic properties (i.e. dealing intrinsically with the functions) as well as syntactic properties (referring to the transducers which compute these functions).

Additionally, this thesis provides new computation models and characterizations in order to capture known classes of transductions. These results complete the previous understanding of these classes and provide new insights on their expressive power. The author believes that the various techniques of this manuscript form a rather extensive toolbox for investigating other open membership problems.

Preservation Theorems in first-order logic are a collection of results derived from classical Model Theory. These results establish a direct correspondence between the semantic properties of formulas and the syntactic constraints imposed on the language used to express them. However, studying these theorems becomes notably challenging when focusing on finite models, which is unfortunate given that the field of Finite Model Theory is better equipped to describe phenomena occurring in Computer Science. This thesis presents a systematic approach to investigating Preservation Theorems within the realm of Finite Model Theory. The traditional ad-hoc proofs are replaced with a theoretical framework that generalizes techniques based on locality, and introduces a topological presentation of preservation theorems called logically presented pre-spectral spaces. Introducing these topological spaces enables the development of a compositional theory for preservation theorems. Additionally, this thesis takes an initial stride towards systematically examining preservation theorems across inductively defined classes of finite structures. It accomplishes this by proving a generic fixed point theorem for a topological extension of logically presented pre-spectral spaces, specifically Noetherian spaces.

Details can be found here: https://www.irif.fr/~alopez/posts/2023-08-23.html

Temporal graphs are an extension of graphs which represent networks that evolve and change over time. In this context, the edges can be available at certain times and unavailable at others and they are called temporal edges. The length, or another property associated to an edge, that could classically be captured by the weight of an arc, can now have different values based on the time the edge is available. The classical notions from graph theory require novel definitions for temporal graph, taking into account the temporal dimension. A temporal walk, for instance, correspond to a sequence of adjacent temporal edges that are available one after the other. A node $v$ is temporally reachable from a node $u$ if there exists a temporal walk from $u$ to $v$. In this dissertation we explore problems that can be grouped into two main topics: temporal walk computation and temporalisation of a static graph.

We study the problem of computing minimum cost temporal walks, where ``cost'' is to be intended in a very wide sense. Indeed, we introduce an algebraic cost structure that can be instantiated to model all the classical criteria of walk optimisation in temporal graphs such as arrival time or duration, as well as linear combination of them or lexicographic compositions. Moreover, we study this problem in temporal graphs that are subject to waiting time constraints. Our main result on this topic is a temporal-edge scanning algorithm for single-source minimum-cost walks taking as input an acyclic time-expanded representation of the temporal graph and running in linear time. We also show that the setting in which we obtain linear-time is the widest possible: an additional logarithmic factor is needed both when the acyclicity assumption is dropped, or when a weaker temporal graph representation is used.

When we speak about temporalisation we are referring to the network design problem of turning a static graph into a temporal graph while optimising a certain criteria. In particular, we study a problem inspired by the optimisation of bus/metro/tramway schedules in a public transport network where each trajectory of a vehicle is modelled by a walk in the directed graph representing the map of the network. We consider the problem of turning a collection of such walks (called trips) in a directed graph into a temporal graph by assigning a starting time to each trip so as to maximise the reachability among pairs of nodes. We obtain several complexity results. Among them, we show that maximising reachability via trip temporalisation is hard to approximate within a factor $\sqrt{n}/12$ in an $n$-vertex digraph, even if we assume that for each pair of nodes, there exists a trip temporalisation connecting them. On the positive side, we show that there must exist a trip temporalisation connecting a constant fraction of all pairs if we additionally assume symmetry, that is, when the collection of trips to be scheduled is such that, for each trip, there is a symmetric trip visiting the same nodes in reverse order. Notice that symmetry is a fair assumption in the context of public transit networks, where a bus or metro line usually consists in trips in both directions.

The definition of algebraic structures on arbitrary types in homotopy type theory (HoTT) has proven elusive so far. This is due to types being spaces instead of plain sets in general, and equalities of elements of a type behaving like homotopies. Equational laws of algebraic structures must therefore be stated coherently. However, in set-based mathematics, the presentation of this coherence data relies on set-level algebraic structures such as operads or presheaves which are thus not subject to additional coherence conditions. Replicating this approach in HoTT leads to a situation of circular dependency as these structures must be defined coherently from the beginning.

In this thesis, we break this situation of circular dependency by extending type theory with a universe of cartesian polynomial monads which, crucially, satisfy their laws definitionally. This extension permits the presentation of types and their higher structures as opetopic types which are infinite collections of cells whose geometry is described by opetopes. Opetopes are geometric shapes originally introduced by Baez and Dolan in order to give a definition of n-categories. The constructors under which our universe of cartesian polynomial monads is closed allow us to define, in particular, the Baez-Dolan slice construction on which is based our definition of opetopic type.

Opetopic types then enable us to define coherent higher algebraic structures, among which infinity-groupoids and (infinity, 1)-categories. Crucially, their higher structure is univalent in that it coincides with the one induced by their identity types. We then establish some expected results in order to motivate our definitions.

In this thesis, we focus on the syndrome decoding problem (SDP), its generalization, cryptanalysis, and its application to digital signature scheme designs. We introduce a new problem, which we refer to as the generalized syndrome decoding problem. In the cryptanalytic part of the thesis, we then focus on the classical and quantum cryptanalysis of the generalized syndrome decoding problem using the information set decoding framework. More precisely, we calculate the running time of three different (classical) information set decoding algorithms, which we refer to as Prange's, Stern's/Dumer's, and Wagner's algorithms. The three algorithms are adapted to solve specific versions of the generalized problem which are given over the Hamming weight, taken as a baseline, and the Lee weight, taken as an alternative to the most commonly used Hamming weight. We then compare the obtained running times with the running time of the hybrid classical-quantum algorithm, obtained by introducing the Grover search and the amplitude amplification in the appropriate step of Wagner's algorithm. In the protocol design part of the paper, we modify Stern's identification protocol, and the corresponding signature scheme, to the newly introduced generalized syndrome decoding problem. To keep the zero-knowledge property of the scheme, we eventually replace the syndrome decoding problem with the permuted kernel one (PKP), for which we show that the average-case SDP reduces to average-case PKP. We then suggest different methods for optimizing the efficiency of the scheme and then provide numerical results that compare the efficiency of the original construction and our newly introduced scheme. The outcome of this work is an analysis of the newly introduced variant of the syndrome decoding problem that estimates the asymptotic complexity of the problem, as well as the concrete security of the scheme based on this problem. The results indicate that the proper choice of a weight function introduces a harder version of the syndrome decoding problem and thus yields more efficient protocols based upon it.

Graph partition is one of the central problem in graph theory, originated from the famous 4-color problem. In this thesis, two major problems concerning graph partition are considered: the edge separation of signed graphs and the vertex decomposition of sparse graphs.

In the first part of this thesis, we focus on signature packing problems of signed graphs. A signed graph $(G, \sigma)$ is a graph $G$ equipped with a signature $\sigma$ which assigns to each edge of $G$ a sign (either $+$ or $-$). The key concept that separates a signed graph from a 2-edge-colored graph is the notion of switching, a switching at a subset $X$ of vertices of $G$ is to multiply the signs of all edges in the edge-cut $(X, V\setminus X)$ by $-$. A signed graph $(G, \sigma')$ is said to be switching-equivalent (or simply equivalent) to $(G, \sigma)$ if it is obtained by a switching on an edge-cut. Then we define the signature packing number of a signed graph $(G, \sigma)$, denoted $\rho(G, \sigma)$, to be the maximum number of signatures $\sigma_1, \sigma_2,\cdots, \sigma_l$ such that each $\sigma_i$ is switching equivalent to $\sigma$ and the sets $E^{-}_{\sigma_i}$, negative edges of $(G,\sigma_i)$, are pairwise disjoint. We show that it is captured by specific homomorphism. Then we establish connection to several well-known problems: e.g. the four coloring problem, Seymour's edge coloring conjecture. More precisely, we first show that if $G$ is a $K_5$-minor-free bipartite simple graph, then for any signature $\sigma$ we have $\rho(G,\sigma)\geq 4$. Secondly, we continue using the language of packing number and extend the technique to verify that for any antibalanced signed planar graph $(G,\sigma)$ of negative girth at least $5$, $\rho(G,\sigma)\geq 5$. Thirdly, we study a generalization of the packing number. Instead of considering one signature and its equivalent signatures, we separate $k$ signatures which are not necessarily switching equivalent. Since there exists planar graph of packing number 1, we investigate sufficient conditions for a planar graph such that we could separate 2 or 3 signatures.

The second part of this thesis is about vertex decomposition of sparse graphs. We first study the vertex decomposition of planar graphs of girth at least $5$. It is known that every planar graph of girth at least $5$ can be vertex decomposed into two induced subgraphs, one of maximum degree at most 3, the other of maximum degree at most 5. We strengthen this result by showing that these induced subgraphs can be chosen to be forests. We then work on sparse graphs with maximum average degree condition. More precisely, we use potential method to prove that every graph $G$ of $mad(G)\leq \frac{16}{5}$ can be vertex decomposed into two forests of maximum degree at most 1 and 4. Consequently, every graph of genus at most $1$ and girth at least $6$ also admits such decomposition.

The principal goal of this thesis is to use the framework of polygraphs for a fine study of the shapes of higher-dimensional cells (of dimension 3, and implicitly of dimension 4) arising from quadratic normalisations appearing in combinatorial group theory. The thesis includes constructing coherent presentations of a class of monoids admitting a right-noetherian Garside family. Thereby, it presents a unifying generalisation of two distinct extensions of Deligne's original construction of coherent presentations of spherical Artin-Tits monoids, given by Gaussent, Guiraud and Malbos: to general Artin-Tits monoids, and to Garside monoids. In addition, a coherent presentation of monoids admitting quadratic normalisation of class (4, 3) is constructed and specialised to the already known column coherent presentation of plactic monoids of type A, constructed by Hage and Malbos. Furthermore, correspondences are established between the notion of quadratic normalisations (developed by mathematicians in France, led by Dehornoy) and the notion of factorability (developed by mathematicians in Germany led by Bödigheimer, with the goal of using suitable normal forms to understand group homology). Namely, factorable monoids are characterised in the axiomatic setting of quadratic normalisation. Additionally, quadratic normalisation of class (4,3) is characterised in terms of factorability and a condition ensuring the termination of the associated rewriting system.

Complexity measures of Boolean functions capture various aspects of the hardness of computing a function and their study is about finding connections between different complexity measures.

In the first part of this thesis, we introduce and study Certificate Game complexity, a measure of complexity based on the probability of winning a game in which two players are given inputs with different function values and are asked to output some index $i$ where their inputs differ, in a zero-communication setting. We give upper and lower bounds for private coin, public coin, shared entanglement and non-signaling strategies, and give some separations.

In the second part of this thesis, we revisit the celebrated proof of the sensitivity conjecture by Hao Huang. Using spectral techniques, Huang proved that every subgraph of the hypercube Hn of dimension n induced on more than half the vertices has maximum degree at least $\sqrt{n}$. Combined with earlier work, this completed a proof of the sensitivity conjecture. We show an alternate proof of Huang’s result using only linear dependency of vectors associated with the vertices of the hypercube. Our approach helps gain insight on more structural properties of the induced subgraph in addition to the largest degree. As an application, we show that for any Boolean function $f$, the polynomial degree is bounded above by the product of 0-sensitivity and 1-sensitivity, $s_0(f)s_1(f)$, a strictly stronger statement which implies Huang’s theorem. We also obtain structural relations for induced subgraphs at distance 3.

A key implement in Huang’s proof was signed hypercubes with the property that every cycle of length 4 is assigned a negative sign. We take a detailed look at this signature and give a nearly optimal signature that uses the minimum number of negative edges while ensuring that every 4-cycle is negative. This problem turns out to be related to one of Erdős’ problems on the largest 4-cycle free subgraph of the hypercube.

This thesis is concerned with the studying of an extension of the propositional linear logic with fixpoints of type from a Curry-Howard-Lambek perspective. Linear logic with fixpoints of types, called MULL, allows us to have inductive and coinductive proofs. We develop a categorical semantics of MULL based on Seely categories and on strong functors acting on them. Then we introduce and study MULLP as an extension of Polarized Linear Logic, with least and greatest fixpoints. Taking advantage of the implicit structural rules of MULLP, we introduce a term syntax for this language, in the spirit of the classical λ-calculus and of system L. We equip this logical system with a deterministic reduction semantics as well as a categorical semantic. We always examine our categorical semantics with concrete cases such as category of sets and relations, category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving, and coherence spaces with totality. In the case of MULLP, we prove an adequacy result for MULLP between its operational and denotational semantics, from which we derive a normalization property thanks to the properties of the totality interpretation. We will also study non-wellfounded proofs in linear logic, which one can see as an extension of inductive proofs, from a denotational semantics point of view by making a relation between validity condition for non-wellfounded proofs and totality interpretation. Finally, we will provide a categorical setting for the exponentials that are encoded using fixpoints operator.