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.
Fall 2022 – schedule overview
|19 September||Matas Šileikis (Czech Academy of Sciences)||Graph flip processes|
|3 October||Navid Talebanfard (Czech Academy of Sciences)||A variant of the VC-dimension with applications to depth-3 circuits|
|10 October||Marta Grobelna (TU Munich)||Controller Synthesis for Multi-Agent Systems|
|31 October||Matěj Konečný (Charles University)||Extending partial automorphisms|
|7 November||Tomasz Krawczyk (Jagiellonian University)||PQ-trees for circular-arc graphs -- some applications|
|14 November||Marcin Briański (Jagiellonian University)||Forbidding an induced ordered subgraph -- some results on χ-boundedness|
|21 November||Stefanie Mohr, Calvin Chau (TU Munich)||Verification of Neural Networks|
|28 November||Kush Grover, Muqsit Azeem (TU Munich)||Stochastic Games|
|5 December||Tereza Klimošová (Charles University)||On Vizing’s edge colouring question|
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
This is joint work with Peter Frankl and Svyatoslav Gryaznov.
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.
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.
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.
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.
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.
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.
Spring 2021: Special Seminar – part of Round the World Relay in Combinatorics, where a number of seminars and groups around the world were getting together. Each site hosted a talk, and everyone was welcome.
Fall 2020: ITI Online Seminar – a one-semester online venue for presenting current research in discrete mathematics and theoretical computer science in the Czech Republic.