Bachelor's and Master's Thesis Supervision
Besides the topics already announced,
students are welcome to contact Formela staff members, explain their preferences, and agree on a thesis proposal tailored specifically to them.
Depending on the mutual agreement, the difficulty can range from "interesting" to "highly demanding". Perspective Ph.D. students are recommended to insist on the latter.
Topics currently available
Patrolling Games: Simulation and Visualization
The goal is to develop a simulator for patrolling games, where a mobile patroller moves among protected targets represented as vertices in a directed graph. Patroller's moves are controlled by a precomputed randomized strategy. The goal is to visualize the strategy, allow for dynamic changes in the structure of the graph and adapt the strategy on the fly.
Contact: Antonín Kučera, Vít Musil, Vojtěch Řehák
Comparing the functionality of patrolling strategies for different environment types
In robotic patrolling, an autonomous device (such as a drone) strives to detect undesirable activities in a predefined set of targets. These activities can be initiated either by an adversarial attacker or spontaneously by nature, which is formally reflected in the objective function used for evaluating the quality of the patrolling strategy. A challenging open problem is how much the chosen type of environment (adversarial or non-adversarial) influences the design of the patroller's moving strategy.
The main goal of the thesis is to answer this question by providing rigorous (theoretical or experimental) evidence.
Contact: Antonín Kučera
Successfully defended theses
Pavel Šimovec
Transformation of Nondeterministic Büchi Automata to Slim Automata. (2021)
Tereza Schwarzová
QBF-Based Simplification of Acceptance Condition of Emerson-Lei Automata. (2021)
Matěj Pavlík
Implementation of 3-valued BDDs in Q3B. (2021)
Marek Jankola
Transformation of Nondeterministic Büchi Automata to Tight Automata. (2021)
Monika Šlachtová
Interactive specification of patrolling problems. (2021)
Matúš Galba
Graphic simulator of patrolling games. (2020)
Martin Zahradníček
Algorithmic Analysis of Population Protocols. (2020, Dean's Award)
Tomáš Lamser
Algorithmic analysis of patrolling games. (2016, Dean's Award, VCLA Student Award)
Tatiana Zbončáková
Reductions of TGBA by Advanced Simulations. (2021)
Tomáš Jašek
Verification of Memory Safety with Predator and Symbiotic. (2021)
Juraj Síč
Satisfiability of DQBF Using Binary Decision Diagrams. (2020, Dean's Award, 2nd place in IT SPY 2020)
Miloslav Chodil
The satisfiability problem for probabilistic temporal logics. (2019, Dean's Award)
Richard Kakaš
Causality-Based Parallelization of Input Data Processing. (2018)