PhD positions at the Department of Computer Science

2016

Department of Computer Science, Faculty of Informatics, Masaryk University, announces an open call for up to two PhD positions with special funding starting from February 2016, in the following areas:

The deadline for application is June 1, 2016.

General information

Perspective PhD students are expected to show their research background and skills in the area of the selected PhD topic. They should also be proficient in English; prior knowldge of Czech is not necessary.

Stipend

Each of the PhD positions is funded with a stipend of net value 20000CZK per month (this amount consists of the standard doctoral stipend and the extra departmental supplement of 10000CZK per month), which is approximately 750Eur and is on the level of an average net salary in the Czech Republic. The stipend is granted to successful applicants for the first 2 years, with an expected renewal (after an evaluation) for another 2 years. The total length of study is 4 years.

Application procedure

Applicants are advised to contact directly their perspective supervisor (as listed below) for more specific details, well ahead of the deadline. Applications consisting of CV, motivation letter, and possibly other relevant documents supporting the candidate's excellence should be sent to prof. RNDr. Mojmír Křetínský, CSc. (mojmir(atsign)fi(dot)muni(dot)cz) before June 1, 2016. Applications will be evaluated by the departmental committee, which will choose the best eligible applicant(s) over all the advertised topics.
The candidates are still obliged to pass the standard admission procedure for doctoral study. The stipend can be awarded only after successfully completing the standard admission procedure.


Topic: Synthesis and Verification of Stochastic Systems Using Learning Methods

Supervisor: doc. RNDr. Tomáš Brázdil, Ph.D.
Area: Theoretical computer science, Formal Methods

We concentrate on analysis of systems that exhibit randomness and non-determinism. Randomness often stems from failures in physical components, unreliable communication, randomization, etc. Non-determinism naturally arises from underspecification, concurrency, etc. Such systems are typically modelled using Markov decision processes (MDPs), or stochastic games. These models have been widely studied for decades in various contexts such as engineering, artificial intelligence and machine learning (AI-ML), and, a bit more recently, formal verification. Recent results indicate that the field of formal verification may hugely benefit from results and methods developed in the framework of AI-ML. The aim of this PhD project is to further investigate the interplay between synthesis methods from AI-ML and formal verification of MDPs and stochastic games.

Topic: Parameter and model fitting of complex adaptive systems

Supervisor: prof. RNDr. Luboš Brim, CSc.
Area: Theoretical computer science, Formal Methods

Many natural systems (e.g., brains, immune systems, ecologies, societies) and increasingly, many artificial systems (parallel and distributed computing systems, artificial intelligence systems, artificial neural networks, evolutionary programs) are characterized by apparently complex behaviors that emerge as a result of often nonlinear spatiotemporal interactions among a large number of component systems at different levels of organization. These systems have recently become known as Complex Adaptive Systems (CAS). Building suitable sound integrated dynamic models of CAS can be seen as a key step towards the development of predictive models of whole systems.
While the structure of such models is usually available, some of the quantitative features of models are not easily determined. These quantitative attributes, which significantly affect the system dynamics, are usually reflected in the model as parameters. In order to obtain reliable models, parameters, such as reaction rates or concentration values, need to be specified exactly hand in hand with appropriate modifications in the model structure.
Parameter and model fitting is an algorithmic procedure which seeks to find model parameters and model structure adaptations which make the results computed from a model agree with a dataset obtained by measurement and observation of the system or by temporal pattern hypotheses about the system dynamics provided by analysts.
The goal of this disseration project is the development of new original computational methods and techniques that would allow to use formal verification techniques, model checking in particular, as a vehicle for discovering parameter values and model adaptations of discrete models that guarantee the system satisfies the given global property (hypothesis) formulated in temporal logic. The approach will be based on verification as this is in principle an excellent methodology to verify/refute interesting hypotheses. Scalability needed for the analysis of complex (multi-dimensional and multi-scale) models is to be supported by using techniques as known from high-performance computing, e.g. parallel and distributed model checking algorithms.

Control of distributed multi-agent systems under temporal constraints

Supervisor: prof. RNDr. Ivana Černá, CSc.
Area: Theoretical computer science, Formal Methods

Modern engineering systems such as autonomous ground and aerial vehicles, or human-robot collaborative teams, evolve quickly due to industrial needs. As these systems are typically safety critical, there is an equally growing need for formal approaches to their specification, design and verification. The perspective student shall focus on the problem of synthesis of control strategy for a complex dynamic distributed systems that satisfies given both qualitative and quantitative formal specifications. A special focus should be given on coordination of multiple devices working on a common task. Prior introductory knowledge of formal approaches to formal verification is welcome.

Topic: Structural Graph Theory and Algorithmic Metatheorems

Supervisor: prof. RNDr. Petr Hliněný, Ph.D.
Area: Theoretical computer science, Graph Theory

The perspective student shall work on width and depth parameters (such as tree-width and tree-depth and other) of graphs and other relational structures, and apply the theoretical results in algorithmic metatheorems on restricted graph classes. The focus shall be on investigation of sparse graph classes and on complementary “dense” depth parameters such as the new shrub-depth, and on metatheorems for problems formulated in FO logic. Prior introductory knowledge of structural graph theory, logic and parameterized compexity is welcome.
For more information, consult the current research directions.

Stochastic games in operational research

Supervisor: prof. RNDr. Antonín Kučera, Ph.D.
Area: Theoretical computer science, Formal Methods

An optimal behaviour of autonomous agents (robots) in an unknown and possibly adversarial environment can be understood as the problem of synthesizing an optimal or suboptimal strategy in a game where the players correspond to the agents and the environment, and the players' objectives model their intentions. One typical example is patrolling, where a limited number of agents (police patrols, security guards, etc.) need to patrol a given a set of targets (doors, petrol stations, military bases, etc.) so that a possible intrusion is detected with the maximal achievable probability. Problems of this type can be formalized as specific one-sided imperfect information games whose game-theoretic and algorithmic properties have not yet been studied systematically. In the framework of the proposed PhD project, the student should concentrate on discovering the fundamental properties of these games, developing efficient algorithms for synthesizing (sub)optimal strategies, implement them, and then testing their efficiency on real-world examples. The student can benefit from a rich network of international contacts of the group, and cooperate with world class experts in the field of infinite stochastic games.

Scalable Program Verification with Symbolic Execution

Supervisor: doc. RNDr. Jan Strejček, Ph.D.
Area: Theoretical computer science, Formal Methods

The perspective student shall work on increasing efficiency and scalability of automated methods for program analysis, bug finding, and verification. In particular, the attention should be given to possible combinations of symbolic execution with abstraction, interpolation, and other program analysis techniques like abstract interpretation and model checking. The work should bring theoretical results like new or improved algorithms as well as their implementations demonstrating real benefits of theoretical advances. These implementations should be able to handle (a nontrivial class of) programs written in C.
Prior knowledge of formal methods for program analysis and verification, and solid programming skills are welcome.

Responsible contact: prof. RNDr. Petr Hliněný, Ph.D.: Petr%20Hlin%C4%9Bn%C3%BD%20%3Cprodekan(dot)veda%40fi(dot)muni(dot)cz%3E