Seminar on Foundations of Computing

This research seminar provides a venue for presenting research results concerning algorithm design, discrete mathematics, formal methods, logic and related areas of theoretical computer science. The seminar is jointly organized by the research laboratories DIMEA, FORMELA, and LIVE. 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 C117 in the building of the Faculty of Informatics on a (roughly) weekly schedule.

Spring 2025 – schedule overview

Speakers

15.9.Pranshu Gaba (Tata Institute of Fundamental Research, Mumbai)Optimizing expectation with guarantees for window mean payoff in Markov decision processes
29.9.Michal Dvořák (CVUT Prague)Pathfinding in Self-Deleting Graphs
6.10.Daniela Černá (CVUT Prague)Shattering triples with six permutations and related problems
20.10.Aneta Pokorná (MFF Prague/CAS)Reconstructing graphs using graphlet degree sequences
27.10.Sabine Rieder (FI MUNI Brno)Decision Tree Explanations in the Context of Machine Learning
3.11.Tomáš Hons (MFF Prague)A Polynomial Ramsey Statement for Bounded VC-dimension
10.11.Elizaveta Streltsova (ISTA) Face numbers of levels in arrangements and applications to crossing numbers
24.11.Calvin Chau (TU Dresden) Certificates and witnesses for multi-objective queries in Markov decision processes
1.12.Lenka Kopfová (ISTA) Moran process under strong selection
4.12.Nikola Sadovek (TU Dresden) Necessary and sufficient condition for k-dimensional transversals
8.12.Kristýna Pekárková (AGH University of Krakow) Identifying Imperfect Clones in Elections
10.12.Vincent Fischer (TUM) Runtime Verification for LTL in Stochastic Systems
15.12.Marek Filakovský (MUNI) Topology of generalized Clique complexes of grid graphs

Pranshu Gaba : Optimizing expectation with guarantees for window mean payoff in Markov decision processes

Monday, September 15, 14:00

The window mean-payoff objective strengthens the classical mean-payoff objective by computing the mean-payoff over a finite window that slides along an infinite path. In this talk, we will look at the problem of synthesizing strategies in Markov decision processes that maximize the window mean-payoff value in expectation, while also simultaneously guaranteeing that the value is above a certain threshold.

We solve the synthesis problem for three different kinds of guarantees: sure (that needs to be satisfied in the worst-case, that is, for an adversarial environment), almost-sure (that needs to be satisfied with probability one), and probabilistic (that needs to be satisfied with at least some given probability p). We show that for the window mean-payoff objective, all the three problems are in PTIME, and thus have the same complexity as for maximizing the expected performance without any guarantee. Moreover, we show that deterministic finite-memory strategies suffice for maximizing the expectation with sure and almost-sure guarantees, whereas, for maximizing expectation with a probabilistic guarantee, randomized strategies are necessary in general.

This is based on joint work with Shibashis Guha that was accepted in AAMAS 2025.

Michal Dvořák : Pathfinding in Self-Deleting Graphs

Monday, September 29, 14:00

We study the problem of pathfinding on traversal-dependent graphs, i.e., graphs whose edges change depending on the previously visited vertices. In particular, we study self-deleting graphs, introduced by Carmesin et al. (Sarah Carmesin, David Woller, David Parker, Miroslav Kulich, and Masoumeh Mansouri), which consist of a graph G=(V, E) and a function f: V->2^E, where f(v) is the set of edges that will be deleted after visiting the vertex v. In the (Shortest) Self-Deleting s-t-path problem we are given a self-deleting graph and its vertices s and t, and we are asked to find a (shortest) path from s to t, such that it does not traverse an edge in f(v) after visiting v for any vertex v.

We prove that Self-Deleting s-t-path is NP-hard even if the given graph is outerplanar, bipartite, has maximum degree 3, bandwidth 2 and |f(v)| ≤ 1 for each vertex v. We show that Shortest Self-Deleting s-t-path is W[1]-complete parameterized by the length of the sought path and that Self-Deleting s-t-path is W[1]-complete parameterized by the vertex cover number, feedback vertex set number and treedepth. We also show that the problem becomes FPT when we parameterize by the maximum size of f(v) and several structural parameters. Lastly, we show that the problem does not admit a polynomial kernel even for parameterization by the vertex cover number and the maximum size of f(v) combined already on 2-outerplanar graphs.

Daniela Černá : Shattering triples with six permutations and related problems

Monday, October 6, 14:00

Let n≥3 be an integer and (π123, π4, π5, π6) be six permutations of the same ground set [n]. We say that the triple {aπ1, a2, a3}⊂[n] is shattered by (π123, π4, π5, π6) if we can find all possible orderings in the set {(πi(a1),πi(a2),πi(a3)):i∈[6]}.

A natural extremal question is to determine the maximal possible number of triples that can be shattered in this way for a fixed n.

Using the flag algebra method, we prove that no six-tuple of permutations shatters more than 1/2 C(n,3) O(n2) triples. On the other hand, for every n≥3, we construct six permutations of [n] that shatter at least 975/482 C(n,30) triples. We also determine exact values for n∈{6,7,8,9}. These results improve the previously known bounds of Johnson and Wickes.

Next, we focus on related problems, where we add more restrictions on the six-tuple (π123, π4, π5, π6).

This is a joint work with Alexander Clifton, Bartłomiej Kielak, and Jan Volec.

Aneta Pokorná: Reconstructing graphs using graphlet degree sequences

Monday, October 10, 14:00

Graphlets are small subgraphs rooted at a fixed vertex. The number of occurrences of graphlets aligned to a particular vertex, called graphlet degree sequence, gives a topological description of the surrounding of the analyzed vertex.

A long standing open problem in graph theory, the reconstruction conjecture, asks whether the structure of a graph is uniquely determined by its vertex-deleted subgraphs. We ask whether the structure of a graph G is uniquely determined by the graphlet degree sequences of its vertices (considering all graphlets smaller than G). We'll show that the answer is positive for graphs having certain type of asymmetric vertex-deleted subgraphs. Note that the idea of using asymmetry is novel even among the partial results for the (harder) reconstruction from vertex-deleted subgraphs.

Sabine Rieder: Decision Tree Explanations in the Context of Machine Learning

Monday, October 27, 14:00

Trust in a decision-making system requires both safety guarantees and the ability to interpret and understand its behavior. This is particularly important for learned systems, whose decision-making processes are often highly opaque. Recently, decision trees have become customary for representing controllers and policies.

In this talk, we investigate two directions in which decision trees can be used to explain RL systems. The first application area is shielding. Shielding is a prominent model-based technique for enforcing safety in reinforcement learning. However, because shields are automatically synthesized using rigorous formal methods, their decisions are often similarly difficult for humans to interpret and inherently non-deterministic. Therefore, their decision tree representations become too large to be explainable in practice. To address this challenge, we propose a novel approach for explainable safe RL that enhances trust by providing human-interpretable explanations of the shield’s decisions. Our method represents the shielding policy as a hierarchy of decision trees, offering top-down, case-based explanations.

Secondly, we consider concept-based explanations of neural networks, where the nodes in the DT correspond to a semantic concept in the NN. In contrast to previous work, our explanations focus on fidelity with respect to the original network.

Tomáš Hons: A Polynomial Ramsey Statement for Bounded VC-dimension

Monday, November 3, 14:00

A theorem by Ding, Oporowski, Oxley, and Vertigan states that every sufficiently large bipartite graph without twins contains a matching, co-matching, or half-graph of any given size as an induced subgraph. We prove that this Ramsey statement has polynomial dependency assuming bounded VC-dimension of the initial graph, using the recent verification of the Erdős-Hajnal property for graphs of bounded VC-dimension. Since the theorem of Ding et al. plays a role in (finite) model theory, which studies even more restricted structures, we also comment on further refinements of the theorem within this context.

Elizaveta Streltsova: Face numbers of levels in arrangements and applications to crossing numbers

Monday, November 10, 14:00

Levels in arrangements play a fundamental role in discrete and computational geometry and are a natural generalization of convex polytopes, which correspond to the 0-level. In the talk, I will focus on two new results. We determine the space of all linear and affine relations among the face numbers of levels in simple arrangements of n hemispheres in Sd, thereby completing a long line of research on such relations and answering a question posed by Andrzejak and Welzl in 2003. Moreover, we proved a special case n = d + 4 of the long-standing conjecture of Eckhoff, Linhart, and Welzl about the complexity of the (⩽ k)-levels, which implies (by Gale duality) a tight lower bound for the spherical arc crossing number of complete graphs. To obtain these results, we introduce the notion of the g-matrix, which encodes the face numbers of levels in an arrangement and generalizes the classical g-vector of a polytope.

Joint work with Uli Wagner

Calvin Chau: Certificates and witnesses for multi-objective queries in Markov decision processes

Monday, November 24, 14:00

Probabilistic model checking (PMC) is a powerful technique for the formal verification of probabilistic systems, such as randomised algorithms or communication protocols. In recent years, independently checkable certificates and witnesses have been extensively studied to enhance the trustworthiness and explainability of model checking tools.

This talk focuses on certificates and witnesses for multi-objective queries in Markov decision processes (MDPs). Markov decision processes are the standard model in PMC and multi-objective queries are natural formalisms to specify multiple conflicting requirements. For the certification, we first generalize prior work on certificates for single-objective reachability and then improve existing certificates for the decomposition of maximal end components. Based on the characterisation of the certificates, mixed-integer linear programs (MILPs) are derived to find minimal witnesses in the form of subsystems. Finally, we report on an implementation and promising experimental results, showing the efficacy of our techniques.

Lenka Kopfová: Moran process under strong selection

Monday, December 1, 14:00

Moran process is a standard random process in evolutionary game theory that models the competition between two or more species in a network-like population. The population is represented by a graph, where vertices correspond to the individuals and edges to the direct interactions between them. Individuals reproduce, their offspring migrate along the edges of the network, and they replace their neighbors.

We study a modified version of the Moran process that corresponds to strong selection, as in the dynamics of invasive species. In this process, only the mutant individuals spread and eventually take over the whole population. The key quantity that we study is the so-called fixation time, which is the expected time until all individuals become mutants. We give tight upper and lower bounds for the fixation time on a general population structure and refine them for some classes.

Nikola Sadovek: Necessary and sufficient condition for k-dimensional transversals

Thursday, December 4, 14:00, room A502

Helly’s theorem (1913) gives a criterion for when a family of convex sets in R^d has a common point: if every group of d+1 sets intersects, then the entire family does. Viewing a point as a 0-dimensional affine subspace, a theorem of Goodman, Pollack, and Wenger (1988) provides an analogous condition for the existence of a hyperplane (a (d–1)-dimensional affine subspace) that meets every set in the family. In this talk, we present a common generalization of these results by characterizing when a k-dimensional affine subspace of R^d intersects all the sets in a given family of convex sets, for any 0≤k≤d-1. This is joint work with Daniel McGinnis.

Kristýna Pekárková: Identifying Imperfect Clones in Elections

Monday, December 8, 14:00

Many collective decision-making processes can be viewed as elections, where a set of alternatives (“candidates”) is evaluated by a group of agents (“voters”), each expressing preferences over them. We encounter such “elections” everywhere, from the most visible examples in politics (including local referenda, parliamentary, and presidential elections), to decisions like shortlisting applicants for a given job position, to casual situations such as deciding which movie a group should watch.

The field of Computational Social Choice (COMSOC) studies the algorithmic and combinatorial aspects of these decision-making processes. It investigates a wide range of topics, including: What is an efficient and fair way to select a winner? How can we prevent manipulation or strategic voting? What kinds of structure can be detected in preference data, and how hard is it to find?

In elections, perfect clones are groups of candidates that appear indistinguishable from the voters’ perspective – either they are ranked consecutively by every voter (in ordinal elections, where preferences are expressed as complete rankings), or they are approved by exactly the same voters (in approval elections, where each voter gives a simple yes/no judgment on each candidate). However, such perfect similarity is too strict and rarely observed in real data. In this talk, we will discuss the concept of imperfect clones for both ordinal and approval elections. For each setting, we propose several relaxations of perfect clones, and analyze the (parameterized) complexity of two fundamental tasks: detecting the presence of imperfect clones in a given election, and partitioning the entire candidate set into families of imperfect clones.

The talk is based on joint work with Théo Delemazure, Piotr Faliszewski, Łukasz Janeczko, Dušan Knop, Grzegorz Lisowski, Jan Pokorný, Šimon Schierreich, and Ildi Schlotter.

Vincent Fischer: Runtime Verification for LTL in Stochastic Systems

Wednesday, December 10, 14:00, room C123

Runtime verification encompasses several lightweight techniques for checking whether a system’s current execution satisfies a given specification. We focus on runtime verification for Linear Temporal Logic (LTL). Previous work describes monitors which produce, at every time step one of three outputs - true, false, or inconclusive - depending on whether the observed execution prefix definitively determines satisfaction of the formula. However, for many LTL formulas, such as liveness properties, satisfaction cannot be concluded from any finite prefix. For these properties traditional monitors will always output inconclusive. We propose a novel monitoring approach that replaces hard verdicts with probabilistic predictions and an associated confidence score. Our method guarantees eventual correctness of the prediction and ensures that confidence increases without bound from that point on.

Marek Filakovský: Topology of generalized Clique complexes of grid graphs

Monday, December 15, 14:00, room C117

It is classical, that one can capture properties of a graph G using a higher dimensional data structure called simplicial complex. Many different graph complexes have been defined during the years - Neighbourhood, Box, Clique, Independence, Matching... A common technique in the area is to compute topological (homotopy, homology, cohomology) or combinatorial properties(shellability) of graph complexes coming from some restricted family of graphs.

We continue in this approach and determine the homotopy type of a generalization of Clique complexes, we call k-bounded clique complexes for a class of graphs that contains grid graphs. Using the Alexader duality, we obtain homotopy type of total-k-cut complexes of grid graphs, recently introduced by Bayer et. al. (DCG 2024) in connection to Fröberg's theorem.

Past terms

Spring 2025

Fall 2024

Spring 2024

Fall 2023

Spring 2023

Fall 2022

Spring 2022

Fall 2021

Spring 2021: Special Seminarpart 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 Seminara one-semester online venue for presenting current research in discrete mathematics and theoretical computer science in the Czech Republic.

Spring 2020

Fall 2019

Spring 2019