Spring 2023 – schedule overview
Ondřej Lengál (Brno University of Technology): Recent Developments in Complementation of Omega-Automata
Monday, 27 February, 14:00, room C417
Automata accepting omega-regular languages, such as Büchi automata,
are an essential tool for model-checking of liveness properties,
proving termination of programs, or deciding logics such as S1S.
Efficient algorithms for their complementation are necessary components
of the omega-automata toolbox. I will describe our recent progress in this field.
The talk is based on a joint work with Vojta Havlena, Bára Šmahlíková (both FIT BUT),
Yong Li, and Andrea Turrini (both Chinese Academy of Sciences).
Alexandru Malekshahian (King's College London): On the probability that G(n,p) is bipartite
Monday, 6 March, 14:00, room C417
In this talk I will discuss the following basic question: what is the
probability that the Erdős-Renyi random graph G(n,p) is bipartite?
In connection to their work on the solvability of random Boolean equations,
Pittel and Yeum studied this problem in a window around the
critical probability p=1/n. In this talk I will focus on the supercritical
regime p=c/n where c>1 and discuss an approach to this problem via the
study of the random cluster model from statistical physics.
Joint work with Matthew Jenssen and Will Perkins.
Matjaž Krnc (University of Primorska): Graphs with two moplexes are more than perfect
Monday, 13 March, 14:00, room C417
A moplex is a natural graph structure that arises when lifting Dirac's
classical theorem from chordal graphs to general graphs. In the chordal case,
having at most two simplicial modules forces the graph to be interval.
In this talk we focus on graphs containing 2 moplexes, which forms a
counterpart to the class of interval graphs. We show that all 2-moplex graphs
are perfect. More specifically, the class of all connected 2-moplex graphs is
sandwiched between proper interval graphs, and cocomparability graphs
(both inclusions are tight for hereditary classes). We also show that every
connected 2-moplex graph contains a Hamiltonian path, (in contrast with
cocomparability graphs). On the other hand, we show that Graph Isomorphism
and Max-Cut remain NP-hard (in contrast with interval graphs).
This is based on joint work with Clément Dallard, Robert Ganian, Meike Hatzel, and Martin Milanič.
Jae-baek Lee (University of Victoria): Disconnected Common Graphs via Supersaturation
Monday, 20 March, 14:00, room C417
A graph H is said to be common if the number of labelled monochromatic copies of H in a 2-colouring of the edges of a large complete graph is asymptotically minimized by a random colouring. It is well known that the disjoint union of two common graphs may not be common; e.g., K_2 and K_3 are common, but their disjoint union is not. We find the first pair of uncommon graphs whose disjoint union is common and a common graph and an uncommon graph whose disjoint union is common. Our approach is to reduce the problem of showing that certain disconnected graphs are common to a constrained optimization problem, in which the constraints are derived from supersaturation bounds related to Razborov's Triangle Density Theorem.
Alberto Espuny Díaz (TU Ilmenau): Threshold for (some) spanning trees in random geometric graphs
Monday, 27 March, 14:00, room C417
Consider the following model of random graphs: a total of n vertices are assigned to uniformly random positions on the unit square, independently of each other, and any two vertices are then joined by an edge if the distance between their positions is less than a given parameter r. This is called the random geometric graph G(n,r) and, similarly to the binomial random graph G(n,p), increasing properties exhibit thresholds (with respect to the parameter r) which we wish to understand. The behaviour of random geometric graphs, however, is very different from the behaviour of G(n,p). In this talk, I will highlight some of these differences and eventually focus on the case of balanced s-ary trees, for which we have established the threshold. This is based on joint work with Lyuben Lichev, Dieter Mitsche and Alexandra Wesolek.
Jakub Gajarský (University of Warsaw): Twin-width, sparsity, stability and freezing
Monday, 3 April, 14:00, room C417
Twin-width is a graph-theoretic notion introduced by Bonnet et al. in 2020. In the short time since its introduction it has attracted a lot of attention, largely because on the one hand it is quite general (it generalizes for example graphs of bounded clique-width, graphs with excluded minor and posets of bounded width) and on the other hand it still has good structural, combinatorial and algorithmic properties.
The theory of sparse graphs developed by Nešetřil and Ossona de Mendez is a very successful approach to generalize many commonly studied graph theoretic notions (such as planar graphs, bounded degree graphs, graphs with excluded minors) and to study sparse graphs from a unified perspective, and it has led to many interesting results in the last 15 years.
Monadic stability is a model theoretic notion originating in Saharon Shelah’s work in his classification program for logical theories. Currently, monadically stable graph classes are becoming of more and more interest for researchers in graph theory and algorithmics, because of newly found and conjectured connections between logic and structural graph theory.
In the talk I will describe two results explaining how the notions of twin-width, sparsity and monadic stability are related to each other. I will then introduce a technique called ‘freezing’ that is applicable to graphs of bounded twin-width and which was used in the proofs of the results mentioned above.
Magdalena Prorok (AGH University): Directed graphs without rainbow triangles
Monday, 17 April, 14:00, room C417
One of the most fundamental questions in graph theory is Mantel's theorem
which determines the maximum number of edges in a triangle-free graph of order n.
Recently a colourful variant of this problem has been solved. In such variant
we consider k graphs on a common vertex set, thinking of each graph as edges
in a distinct colour, and want to determine the smallest number of edges in
each colour which guarantees existence of a rainbow triangle.
In this talk we solve the analogous problem for directed graphs without rainbow triangles,
either directed or transitive, for any number of colours. The constructions
and proofs essentially differ for k=3 and k≥4 and the type of the forbidden triangle.
This is joint work with Sebastian Babiński and Andrzej Grzesik.
Keat Hng (Czech Academy of Sciences): Approximating fractionally isomorphic graphons
Monday, 24 April, 14:00, room C417
Fractional isomorphism of finite graphs is an important and well-studied
concept at the intersection of graph theory and combinatorial optimization.
It has many different characterizations that involve a range of very different
and seemingly unrelated properties of graphs. Recently, Grebík and Rocha
developed a theory of fractional isomorphism for graphons, i.e. limits of
dense graph sequences, where they showed that every characterization of
fractional isomorphism in graphs has a well-defined graphon counterpart
and that these are indeed all equivalent characterizations of fractional
isomorphism for graphons. They asked whether fractionally isomorphic graphons
can be characterized as the limits of graph sequences which are entrywise
fractionally isomorphic (in the graph sense). We answer their question in
the affirmative.
This is joint work with Jan Hladký.
Alessandro Abate (University of Oxford): Logic meets Learning – Formal Synthesis with Neural Templates
Thursday, 18 May, 14:00, room C417
I shall present recent work on CEGIS, a “counterexample-guided inductive synthesis” framework for sound synthesis tasks that are relevant for dynamical models, control problems, and software programs. The inductive synthesis framework comprises the interaction of two components, a learner and a verifier. The learner trains a neural template on finite samples. The verifier soundly validates the candidates trained by the learner, by means of calls to a SAT-modulo-theory solver. Whenever the candidate is not valid, SMT-generated counter-examples are passed to the learner for further training. I shall elucidate the ins&outs of the CEGIS framework, and display its workings on a few problems: synthesis of Lyapunov functions and of barrier certificates; hybridisation of nonlinear dynamics for safety verification; synthesis of digital controllers for continuous plants; and an application in real-time autonomy.
Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford, where he is also Deputy Head of Department. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received an MS/PhD from the University of Padova and UC Berkeley. His research interests lie on the formal verification and control of stochastic hybrid systems, and in their applications in cyber-physical systems, particularly involving safety criticality and energy. He blends in techniques from machine learning and AI, such as Bayesian inference, reinforcement learning, and game theory.
Djordje Žikelić (IST Austria): Formal Verification and Learning-based Control of Infinite-state Stochastic Systems
Monday, June 5, 14:00, room C417
Stochastic systems provide a formal model for systems that exhibit uncertain behavior. However, in contrast to their finite-state counterparts, formal verification and control of infinite-state stochastic systems are less understood. This talk will advocate for the use of martingale-based methods for formal verification and controller synthesis in infinite-state stochastic systems. The key advantage of martingale-based methods is that they provide formal guarantees while allowing for fully automated verification and control algorithms with applications in programming languages, control theory and artificial intelligence. In this talk, we present novel martingale-based methods for static analysis of probabilistic programs and for controller synthesis in stochastic dynamical systems. In particular, for the latter, we present the first framework for learning and formally verifying neural controllers in stochastic systems.
James Main (University of Mons): Different Strokes in Randomised Strategies
Monday, June 12, 14:00, room C417
Two-player games on (possibly stochastic) graphs are a prevalent model in theoretical computer science. Notably, such games are useful in the context of reactive synthesis, i.e., for automatic design of systems that behave well no matter the behaviour of the environment they interact with. Optimal strategies in games on graphs may require randomisation when dealing with inherently probabilistic goals, balancing multiple objectives, or in contexts of partial information. There is no unique way to define randomised strategies. For instance, one can use so-called mixed strategies or behavioural ones. In the most general settings, these two classes do not share the same expressiveness. A seminal result in game theory - Kuhn's theorem - asserts their equivalence in games of perfect recall.This result crucially relies on the possibility for strategies to use infinite memory, i.e., unlimited knowledge of all past observations. However, computer systems are finite in practice. Hence it is pertinent to restrict our attention to finite-memory strategies, defined as automata with outputs. Randomisation can be implemented in these in different ways: the initialisation, outputs or transitions can be randomised or deterministic respectively. Depending on which aspects are randomised, the expressiveness of the corresponding class of finite-memory strategies differs.
In this talk, we provide a complete taxonomy of the classes of finite-memory strategies obtained by varying which of the three aforementioned components are randomised.