Fall 2023 - schedule overview

Filip Pokrývka (Masaryk University): Sparse Graphs of Twin-width 2 Have Bounded Tree-width

Monday, September 25, 14:00, room C417

Twin-width is a structural width parameter introduced by Bonnet, Kim, Thomassé and Watrigant [FOCS 2020]. Very briefly, its essence is a gradual reduction (a contraction sequence) of the given graph down to a single vertex while maintaining limited difference of neighbourhoods of the vertices, and it can be seen as widely generalizing several other traditional structural parameters. Having such a sequence at hand allows to solve many otherwise hard problems efficiently. Our paper focuses on a comparison of twin-width to the more traditional tree-width on sparse graphs. Namely, we prove that if a graph G of twin-width at most 2 contains no K_t,t subgraph for some integer t, then the tree-width of G is bounded by a polynomial function of t. As a consequence, for any sparse graph class C we obtain a polynomial time algorithm which for any input graph G∈C either outputs a contraction sequence of width at most c (where c depends only on C), or correctly outputs that G has twin-width more than 2. On the other hand, we present an easy example of a graph class of twin-width 3 with unbounded tree-width, showing that our result cannot be extended to higher values of twin-width.

Joint work with Benjamin Bergougnoux, Jakub Gajarský, Grzegorz Guśpiel, Petr Hliněný, and Marek Sokołowski

Ehsan Goharshady(IST Austria): Non-Termination: Program Reversal and Invariant Generation

Monday, October 02, 14:00, room C417

Proving the non-termination of programs is a fundamental challenge in the field of program analysis and verification. While verifying that a program always terminates is crucial for safety and reliability, the complement, non-termination proving, can be equally important for detecting bugs and verifying security-critical and real-time systems. In this talk, we will explore an approach for non-termination proving of polynomial programs via invariant generation techniques and program reversal.

MichaelAnastos (IST Austria): Robust Hamilotnicity in families of Dirac graphs

Monday, October 09, 14:00, room C417

A graph is called Dirac if its minimum degree is at least half of the number of vertices in it. Joos and Kim showed that every graph family G=(G_1,...,G_n) of Dirac graphs on [n] contains a Hamilton cycle transversal, i.e., there exists a Hamilton cycle H on [n] and a bijection h:E(H) -> [n] such that e belongs to G_{h(e)} for every e in E(H).
In this talk we present robust versions of this theorem. In particular we show that for p is sufficiently large, if we let H_i be a random subgraph of G_i then the graph family H=(H_1,...,H_n) contains a Hamilton cycle transversal w.h.p.

Chloé Capon (University of Mons): Generation and Exploitation of Counterexamples in Stochastic Models

Monday, October 16, 14:00, room C417

Reactive synthesis is a core problem in formal methods. Given a system to control trying to enforce some specification within an uncontrollable environment, it aims at the automated construction of provably-safe system controllers. Synthesis algorithms and tools permit to construct a suitable (formal) controller if one exists, i.e., if the specification can be enforced. If not the case, they simply tell us that no such controller exists. However, from a practical standpoint we need to help practitioners understand why their attempt failed. This can be done by generating counterexamples which carry information on why the synthesis process did not work. The generation of counterexamples has been studied in basic stochastic models such as Markov chains and also Markov decision processes (MDPs) which contain both non-deterministic choices and stochastic transitions. However, this has only been studied for verification: counterexamples can be used to prove the existence of a bad controller, but not the non-existence of a suitable one. In this talk, we tackle the generation of counterexamples for MDPs in the synthesis mindset.

Nicolas Lecomte (University of Mons): Transferring controllers in reactive synthesis

Monday, October 16, 14:00, room C417

In reactive synthesis, most algorithms are computationally expensive and ill-suited to be applied in a continuous development process that needs the controller to be adapted to small changes to specifications or to the system efficiently. To tackle this problem, we would like to allow the transfer of controllers, which consists in taking a controller that has been built for a certain setting and adapting it to a new context, with guarantees on its behavior. This talk surveys preliminary work pertaining to this research agenda. To measure the a priori efficiency of the transfer of a controller between two systems, we plan to use similarity metrics. Moreover, repair techniques could be useful to apply small changes to a transferred controller and adapt it to its new environment.

Marcin Briański (Jagiellonian University, Poland): Width parameters beyond Treewidth

Monday, November 6, 14:00, room C417

Treewidth is a classical width parameter used in structural graph theory and serves as a cornerstone of Graph Minors project of Robertson and Seymour. Besides being an important structural parameter, it is widely known for its usefulness in graph algorithms --- a quality that is highlighted by Courcelle's Theorem about tractability of MSO expressible properties.

Let us consider the case of solving Maximum Weight Independent Set (MWIS). It is easily solvable (in FPT time) on graphs of bounded treewidth. However, it is not the end of the story. It is quite easy to convince oneself that MWIS is easily solvable on Chordal graphs, which do not have bounded Treewidth. This leads to the introduction to a new width parameter --- Tree Independence Number --- for which it turns out we have an XP time algorithm for MWIS.

In this talk I will discuss properties of a related relaxation of Treewidth called Induced Matching Treewidth (introduced by Yolov under the name Minor-Matching Hypertree Width), its connections to the aforementioned Tree Independence Number, as well as present a sketch of a proof that bounding this parameter gives a χ-bounded class of graphs.

This talk is based on joint work with Tara Abrishami, Jadwiga Czyżewska, Rose McCarty, Martin Milanič, Paweł Rzążewski, and Bartosz Walczak.

Jan Böker (RWTH Aachen): Fine-grained Expressivity of Graph Neural Networks

Monday, November 13, 14:00, room C417

Numerous recent works have analyzed the expressive power of message-passing graph neural networks (MPNNs), primarily utilizing combinatorial techniques such as the 1-dimensional Weisfeiler-Leman test (1-WL) for the graph isomorphism problem. However, the graph isomorphism objective is inherently binary, not giving insights into the degree of similarity between two given graphs. We resolve this issue by considering continuous extensions of both 1-WL and MPNNs to graphs. Concretely, we show that the continuous variant of 1-WL delivers an accurate topological characterization of the expressive power of MPNNs on graphons, revealing which graphs these networks can distinguish and the level of difficulty in separating them. We identify the finest topology where MPNNs separate points and prove a universal approximation theorem. Consequently, we provide a theoretical framework for graph and graphon similarity combining various topological variants of classical characterizations of the 1-WL. In particular, we characterize the expressive power of MPNNs in terms of the tree distance, which is a graph distance based on the concepts of fractional isomorphisms, and substructure counts via tree homomorphisms, showing that these concepts have the same expressive power as the 1-WL and MPNNs on graphons. Empirically, we validate our theoretical findings by showing that randomly initialized MPNNs, without training, exhibit competitive performance compared to their trained counterparts. Moreover, we evaluate different MPNN architectures based on their ability to preserve graph distances, highlighting the significance of our continuous 1-WL test in understanding MPNNs' expressivity.

This is joint work with Ron Levie, Ningyuan Huang, Soledad Villar, and Christopher Morris.

Abhisekh Sankaran (Tata Consultancy Services Research, Pune, India): Program Verification using Small Models

Monday, November 20, 14:00, room C417

Christoph Weinhuber (TU Munich): Game-Theoretic Verification Using Stochastic Games: Equilibria Properties and Their Refinements

Monday, December 4, 14:00, room C417

In this presentation, we provide an overview of the advances in game-theoretic verification techniques, particularly focusing on equilibria-based properties and their refinements. We address the challenges faced by an increasing number of agents by presenting a novel extension to PRISM-games, correlated equilibria, where players can coordinate via a public signal. We introduce a novel concept of equilibria refinements, social welfare, and fairness, offering a fresh perspective on equilibria. Furthermore, we shed light on the novel concept of robust equilibria, which allow for a more realistic framework to reason about real-world applications.

Sabine Rieder (TU Munich): Safety Assurances of Neural Network Based Systems

Monday, December 4, 14:00, room C417

Neural Networks (NNs) have become widely used in different application domains including safety critical ones. However, it is well known that NNs are prone to produce erroneous results with high confidence when faced unknown inputs or sometimes even slight perturbations of known inputs. With the rise of NN based systems in safety-critical applications, the need for ensuring their safety arises. In this talk, we will give an overview of current developments in the area of NN verification as well as NN runtime monitoring. We will conclude the talk with a presentation of our monitoring technique based on observing the activation values of hidden neurons at runtime.

Bodhayan Roy (IIT, Kharagpur, India): The maximum cut problem on interval graphs

Monday, December 11, 14:00, room C417

Interval graphs are intersection graphs of intervals on the real line, and a well studied class among geometric graphs. Most of the well known optimization problems have polynomial time algorithms, some even linear time algorithms, on this class of graphs. However, the maxcut problem is an exception.
The maxcut (or, maximum cut) problem asks for a bipartition (A,B) of the vertex set of a graph, so that the number of edges having exactly one end vertex in each of A and B, are maximized. It is an important problem due to practical aspects like classification, circuit design etc. A few years ago, maxcut was found to be NP-complete for interval graphs. In this talk, we discuss the complexity of the maxcut problem on interval graphs and its subclasses.