Logic List Mailing Archive

CfA: PhD Position in Formal Methods (Symbolic Reactive Synthesis on Planning Domains), Chalmers University of Technology - Gothenburg (Sweden), deadline: 15 May

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. This position is supported by WASP (Wallenberg AI, Autonomous Systems, and Software Program) alongside 4 other positions to work with my colleagues Fredrik Johansson (Machine Learning), Hazem Torfah (Autonomous Systems), Gregory Gay (Software Testing), and Muoi Tran (Secure Networks).
Research scope: formal methods, reactive synthesis, planning, automata, games, temporal logics
Apply here: https://tiny.cc/gbgphd
The successful candidate will work on the project “Symbolic Reactive Synthesis on Planning Domains”. 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. Planning domain description language (PDDL) is a standard language used to specify planning problems and domains in artificial intelligence. It provides a way to define objects, actions, and goals for automated planning systems to solve complex tasks. The project will seek to combine usage of PDDL in reactive synthesis. 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.
The aim of the doctoral (third-cycle) education is to acquire the knowledge and skills necessary to conduct independent research within computer science, and to contribute to the development of knowledge by writing a scholarly thesis.
PhD (third-cycle) education is through a fixed-term employment contract for 5 years. During these 5 years, most of the student’s time will be devoted to their research. They will also be assisting the department’s education by working 20% of their time on a teaching or supporting role. The 20% support component may be concentrated in certain parts of the year according to department’s needs (in consultation with the student). In addition, the student will have to undertake 60 Higher Education Credits (HECs) in courses enriching their knowledge in computer science, supporting their research, and gaining general (scientific) skills.
This project is supported by WASP and the appointed student will also belong to the WASP graduate school. Some of the required HECs will be specialized WASP courses about autonomous systems and AI. The appointed student will also be eligible to participate in other WASP supported programs (such as visits to universities abroad or short-term research visits to other universities).

--
[LOGIC] mailing list, provided by DLMPST
More information (including information about subscription management) can
be found here: http://dlmpst.org/pages/logic-list.php