Information about the project
The Department of Computer Science and Engineering is strongly international, with approximately 270 employees from over 30 countries. The department is a shared department between the University of Gothenburg and Chalmers University of Technology. The position is placed in the Formal Methods unit, which is internationally recognized for its high-profile research track record and extensive network of collaborators.
The successful candidate will work on the project “Combining Path-finding Algorithms in Temporal Reactive Synthesis” financed by WASP (Wallenberg AI, Autonomous Systems and Software Program). Reactive synthesis – automatic production of programs from high-level descriptions of their desired behavior – is emerging as a viable tool for the development of robots and reactive software. In high level, this is like telling a robot what you would like it to do and automatically planning how to do it. The project will improve the capabilities of reactive synthesis techniques through improving algorithms for the analysis of state-spaces through the combination of path finding and strategy finding. This will include both theoretical and practical contributions. More concretely, the work will include the study of temporal logic, automata, and two player games. Temporal logic is used for describing in a high level the required behavior of a program, 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.