Joint DIMEA and FORMELA seminar

This research seminar provides a venue for presenting research results concerning algorithms, discrete structures, formal methods, logic and related areas of theoretical computer science. The seminar is jointly organized by the research laboratories DIMEA and FORMELA. The seminar builds on the FMDSA seminar organized by the FORMELA laboratory in the past.

Time and place

The seminar takes place on Monday at 2PM term time in Room C417 in the building of the Faculty of Informatics on a (roughly) weekly schedule.

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.