Research projects

Parameterized complexity and algorithmic metatheorems

The theory of parameterized complexity truly revolutionarized the area of algorithm design in recent years, as it provides a way to attack many NP-hard problems with algorithms that are efficient wrt. certain additional restrictions (the parameters). We focus on design of parameterized combinatorial algorithms, on algorithmic metatheorems for logics, and complexity lower bounds.

Contact: Petr Hliněný a Jan Obdržálek

Width and depth parameters of graphs

In this area we study traditional as well as some new parameters describing the “width” of combinatorial objects (in the sense of complexity, how much they “resemble” trivial input structures like trees) – tree-width, branch-width, rank-width, DAG-width, or DAG-depth, to mention just a few. The expected outcome is that on input objects of low width, many otherwise hard algorithmic problems become tractable, as for instance various MSO-definable properties. We pay specific attention also to recent “depth” parameters, like shrub-depth. The question of how to obtain such low width/degree/depth decompositions is also studied.

Contact: Petr Hliněný a Jan Obdržálek

Crossing number of graphs

We study the problem how to draw a graph with the least possible number of edge crossings, which appears to be an unusually difficult algorithmic task. Our first interest is in finding good efficient approximation algorithms of the crossing number (some of which are even practically implementable, a quite rare case in this area). Besides that we deal with theoretical research of crossing-critical graphs, and with computational hardness questions related to this problem. We are now particularly looking at an approximate structural description of crossing-critical graphs.

Contact: Petr Hliněný

Modelling and verification of communication protocols

Since the year 2008, we have been developing and improving SCStudio - Sequence Chart Studio, a user-friendly tool for modeling and verification of communication protocols. We offer topics on implementation improvements to undergraduate students who are interested in completing their bachelor/master theses in this area. We also try to extend the scope of practical applicability of our tool. For example, we collaborate with LaBAK on verification of a newly developed payment protocol.

Contact: Vojtěch Řehák

Continuous-time stochastic systems in performance analysis

We develop formal models and the corresponding verification algorithms for systems that operate in real time and may exhibit random behaviour (such as communication protocols with random latency and message losses). Currently, we concentrate on various extensions of standard continues-time models, such as continues-time Markov chains, stochastic Petri nets, queueing networks etc., with discrete-time control mechanisms.

Contact: Tomáš Brázdil and Vojtěch Řehák

Efficient strategy synthesis for games with discrete state-space

We aim at designing efficient algorithms for computing optimal (or nearly optimal) strategies in games with discrete and possibly infinite state-space. This includes games over various automata-theoretic models such as (multi)counter machines, pushdown automata, or queueing systems, and we also consider games with stochastic states. The studied objectives range from simple reachability or safety to long-run average properties or temporal properties expressible in various temporal logics.

Current topics for undergraduate students:

  • Algorithms for solving codebreaking games. Codebreaking games are played by two players, the codemaker and the codebreaker. The codemaker selects a secret code and the codebreaker strives to discover this code using a minimal number of allowed experiments that reveal some partial information about the code. Examples of codebreaking games include Mastermind, various variants of Balance Puzzles, etc. Codebreking games can also model security problems related to information leakage (such as API-level attacks in hardware security modules in ATM networks), string-matching problems applied in genetics, etc. The goal of the project is to develop efficient algorithms and tools for solving general deductive games. The main problem is the large number of experiments available to the codebreaker, which can be reduced by considering appropriate symmetries. The project is a continuation of the previous work described in the master thesis of Miroslav Klimoš (see also the LPAR 2015 paper) which resulted in a software tool Cobra.
    More information: Cobra: A Tool for Solving General Deductive Games. By Miroslav Klimoš and Antonín Kučera. In Proceedings of 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2015).
    Contact: Antonín Kučera

Security games

We concentrate on a subfield of algorithmic game theory concerned with applications in security and patrolling. Security games are typically played by two parties, defenders and attackers. The goal of the defenders is to protect a set of targets while the attackers try to seize them. Such games naturally model protection of important facilities (airports, military objects), specific areas (watching over seaside resorts, guarding convoys in oceans), etc. We study fundamental properties of security games, such as the existence and type of optimal strategies, as well as efficient algorithms for their solution. We collaborate with a research group of Michal Pěchouček (see that successfully applies related theoretical concepts in practice.

Current topics for undergraduate students:

  • Algorithmic Analysis of Patrolling Games. A central problem in security and operational research is how to deploy limited security resources (such as police patrols, security guards, etc.) to maximize their effectiveness. Clearly, police patrols cannot be everywhere all the time, security guards cannot check every door every minute, etc., which raises a crucial question how to utilize them best. This question can be formalized as the strategy synthesis problem in patrolling games where the goal of one player (the patroller) is to visit the targets so that the probability of discovering the attack performed by the other player is maximized. The goal of the project is to develop efficient strategy synthesis algorithms for patrolling games and solve some of the open game-theoretic questions about these games.

This research area is rich and new topics for both Bachelor and Master theses can easily be found. Interested students are advised to contact Tomáš Brázdil, Antonín Kučera, and Vojtěch Řehák

Static program analysis of sequential imperative and low-level programs

We primarily focus on finding software behaviour violating semantic model of a sequential imperative programing language. So far we have developed an abstract interpretation based tool Stanse which has found over 160 real defects in the Linux kernel. We are currently working on an experimental library Bugst providing ground for fast implementation of new techniques based on symbolic program execution.

Current topics for undergraduate students:

  • Loop Bound Analysis Based on Symbolic Execution
  • Execution synthesis

Contact: Jan Strejček

research.txt · Last modified: 2015/09/01 11:37 by Antonin Kucera