PhD positions at the Department of Computer Science

2017

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

The deadline for application is May 28, 2017.
(In the previous call, with start in Feb 2017, the Selection Committee of the Department has voted David Klaška as eligible for the stipend (20000CZK per month), under supervision of prof. Kučera.)

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 knowledge 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 May 28, 2017. 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 complexity is welcome.
For more information, consult the current research directions.

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