PhD Position in Formal Methods, Gothenburg (Sweden)

There is an open PhD position in the department of Computer Science and Engineering at Chalmers University of Technology / the University of Gothenburg, Sweden. The student will work on the project "Symbolic Reactive Synthesis on Planning Domains” with Professor Nir Piterman. The student will join the formal methods unit, with currently 6 active PhD students.

The project will seek to combine usage of Planning Domain Description Language (PDDL) in reactive synthesis (automatic production of programs from high-level descriptions of their desired behavior). This will include both theoretical and practical contributions. More concretely, the work will include the study of temporal logic, planning domains and planning techniques, automata, and two player games. Temporal logic and planning domains are used for describing in a high level the required behavior of a program, planning techniques are used to extract information about the problem, automata are used as an algorithmic tool for manipulation of logic formulae, and two-player games enable to consider strategies and programs. We will study these formalisms, analyze their properties, devise algorithms to manipulate and translate between them, as well as implement tools that will show the applicability of the developed techniques.