Joint DIMEA and FORMELA seminar

Fall 2022 – schedule overview

Matas Šileikis (Czech Academy of Sciences): Graph flip processes

Monday, 19 September, 14:00, room C417

Consider a discrete time graph process, where at each step we choose, uniformly at random, a k-tuple of vertices and transform the subgraph it induces by a predefined rule, for example "if you see a clique, remove all its edges" or "whatever you see, replace it by a random graph G(k,1/2)". We will show how to convert the question about concentration of this process (for a quadratic number of steps) to a dynamical system in the space of graphons. We will consider a few examples of simple rules, and consider a rule which gives rise to a periodic trajectory.
The talk is based on work with P. Araújo, F. Garbe, J. Hladký, E. K. Hng and F. Skerman.

Navid Talebanfard (Czech Academy of Sciences): A variant of the VC-dimension with applications to depth-3 circuits

Monday, 3 October, 14:00, room C417

We introduce a new analogue of the well-known VC-dimension. We show that for this notion, the corresponding Sauer-Shelah bound can be significantly beaten. We will use this to make progress on an extremal problem arising in circuit complexity.
This is joint work with Peter Frankl and Svyatoslav Gryaznov.

Marta Grobelna (TU Munich): Controller Synthesis for Multi-Agent Systems

Monday, 10 October, 14:00, room C417

Multi-agent systems (MAS) consist of multiple computing entities, called agents, that collaboratively solve tasks. In particular, a complex task is divided into simpler tasks and distributed among the agents according to their capabilities. Each agent is equipped with sensors to sense the environment and communication modules that allowed them to exchange information with other agents, in order to make decisions about joint actions that fulfill the assigned task. Due to the high degree of flexibility, MASs have many areas of application, for instance, in robotics, computer networks, or smart grids. Since most of the environments where MAS can be deployed are safety-critical, guaranteeing the safety of such systems is crucial. Formal methods are mathematically rigorous approaches that can be used to provide such guarantees.
In this talk I will focus on controller synthesis, whose goal is to automatically synthesize a desired system from its specification. The advantage of synthesis over verification, is that it provides a correct-by-construction system making the subsequent verification step redundant. In order to understand their importance, I will overview the different synthesis approaches that can be applied to MAS and finally sketch our idea about cascades of games.

Matěj Konečný (Charles University): Extending partial automorphisms

Monday, 31 October, 14:00, room C417

A partial automorphism of a graph is an isomorphism between induced subgraphs of the graph. In 1992, as a key component for solving a problem in model theory, Hrushovski proved the followng purely combinatorial result: For every finite graph G there is a finite graph H containing G as an induced subgraph such that every partial automorphism of G extends to an automorphism of H. Since then, analogous results have been proved for various other classes of structures and the connection with model-theory has been well established. In this talk I will give an overview of the area.

Tomasz Krawczyk (Jagiellonian University): PQ-trees for circular-arc graphs -- some applications

Monday, 7 November, 14:00, room C417

In 2019 Krawczyk (basing on the ideas of Hsu) devised a PQ-tree for circular-arc graphs, which is a data structure that allows to represent all canonical intersection models of a circular-arc graph. In my talk I will show some examples on how to use this data structure to efficiently solve some computational problems in the class of circular-arc graphs, such as canonization and isomorphism. We will also discuss some results that allow us to search for a canonical model of a circular-arc graph which satisfies certain conditions with respect to the Helly property.
Some results mentioned in the talk are a joint work with Deniz Ağaoğlu Çağırıcı, Jan Derbisz, and Grzegorz Gutowski.

Marcin Briański (Jagiellonian University): Forbidding an induced ordered subgraph -- some results on χ-boundedness

Monday, 14 November, 14:00, room C417

The investigation of χ-bounded classes of graphs can be viewed as a quest to understand what structures, besides cliques, force a graph to have a high chromatic number. As one might expect due to the NP-hardness of graph colouring, this question is not an easy one to answer, as evidenced by many long standing open problems in this field with the Gyárfás–Sumner Conjecture (is the class of graphs without a fixed forest as an induced subgraph χ-bounded?) being a particularly prominent example.
A somewhat different way to construct an interesting class of graphs is to forbid an induced ordered subgraph, wherein we consider all our graphs together with some linear order on the vertex set and require a subgraph to be consistent with this order. As an example, in this way one can easily define the classes of comparability graphs and chordal graphs -- two very thoroughly investigated subclasses of perfect graphs. A natural question one might ask then is for which ordered graphs H does forbidding H as an induced ordered subgraph produce a χ-bounded class of graphs? Due to the existence of graphs with high girth and high chromatic number any such H (regardless of ordering) need be acyclic, however unlike in the unordered case we know of many examples of ordered forests which do not give a χ-bounded class of graphs. Indeed, no general conjecture on when forbidding an ordered forest gives a χ-bounded class of graphs has been put forward yet.
In this talk I will present some of the known results on this topic, in particular I will sketch a proof that forbidding any induced ordered matching always yields a χ-bounded class of graphs.
This talk is based on joint work with James Davies, Rose McCarthy and Bartosz Walczak.

Stefanie Mohr and Calvin Chau (TU Munich): Verification of Neural Networks

Monday, 21 November, 14:00, room C417

The talk will be given in two parts. In the first talk, Stefanie will discuss a short introduction to Neural Networks and an overview of techniques to verify them. The second talk will be given by Calvin, who will dive into an abstraction-based approach to verify Neural Networks.

First Abstract: Since Neural Networks have been improved a lot over the past years, they start to appear in safety critical systems. To ensure their safety and that they follow certain specifications, there are various methods that try to verify their behavior. In this talk, I will give a short introduction and overview of these techniques.

Second Abstract: In this talk, we present an abstraction approach for compressing the size of the networks to ease the verification process. Our approach is based on semantic similarity of neurons and uses linear programming and orthogonal projection to reduce the size of the network. Further we describe how our abstraction can be refined, potentially allowing for a counter-example guided abstraction refinement (CEGAR) approach.

Kush Grover and Muqsit Azeem (TU Munich): Stochastic Games

Monday, 28 November, 14:00, room C417

The seminar will consist of two parts. The first talk will be a brief introduction to stochastic games, and the second talk will be its application by showing how a real-world problem can be modeled and solved as a stochastic game.

First talk: Verification of Concurrent Stochastic Games

Concurrent reachability games belong to the family of stochastic games played on graphs. In this talk, I will briefly introduce concurrent stochastic games with reachability objectives, compare them with turn-based games, and give an overview of techniques from literature to solve them.

Second talk: Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games

I will talk about security risks in the form of advanced persistent threats (APTs) and their detection using dynamic information flow tracking (DIFT). We model the tracking and the detection as a stochastic game between the attacker and the defender. Solving these games gives us trade-offs between resource efficiency of the tracking and efficacy of the detection.

Tereza Klimošová (Charles University): On Vizing’s edge colouring question

Monday, 5 December, 14:00, room C417

In his 1965 seminal paper on edge colouring, Vizing proved that a (Δ+1)-edge colouring can be reached from any given proper edge colouring through a series of Kempe changes, where Δ is the maximum degree of the graph. He concludes the paper with the following question: can an optimal edge colouring be reached from any given proper edge colouring through a series of Kempe changes? In other words, if the graph is Δ-edge-colourable, can we always reach a Δ-edge-colouring? We answer this question in the affirmative for triangle-free graphs.

Joint work with Marthe Bonamy, Oscar Defrain, Aurélie Lagoutte and Jonathan Narboni.