<h1 class="item-title" style="margin:0px;padding:0px;border:0px;outline:0px;font-size:28.799999px;vertical-align:baseline;background:none;line-height:23.040001px;font-family:georgia,"times new roman",serif;letter-spacing:0.1ex" dir="auto"><span style="font-size:14.4px;font-family:"Helvetica Neue",Arial,"Liberation Sans",FreeSans,sans-serif">A fully funded 5-year Ph.D. position in Computer Science and Engineering with the subject “Space-Aware Synthesis of Situated Autonomous Systems” is open at the Department of Computer Science and Engineering, Chalmers | University of Gothenburg, Sweden. We are looking for excellent and motivated candidates. This is a joint call at our department with several projects and is limited to a maximum of 4 projects being funded in this round. Thus, only highly qualified applicants will be funded.</span><span style="font-size:14.4px;font-family:"Helvetica Neue",Arial,"Liberation Sans",FreeSans,sans-serif"> </span><br></h1><div class="item-text dynamic-text" style="margin:1em 0px 0px;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none;line-height:18px;font-family:"Helvetica Neue",Arial,"Liberation Sans",FreeSans,sans-serif" dir="auto"><div style="margin:0px;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">The Ph.D. position that I am advertising will be hosted by the Formal Methods (FM) research unit and supervised by Dr. Yehia Abd Alrahman.  Our unit (and department as a whole) has excellent research groups that work on Modelling and Verification problems, that may intersect with research in control and AI. <br></p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">The objective of the Ph.D. project is to develop novel methods and algorithms for automatic production of correct-by-design situated autonomous systems. That is, systems that live on autonomous machines (such as robots) and populate a shared physical space. Such machines can influence each other by merely moving/modifying the space. Situated Autonomous systems are expected to operate while co-existing with other machines and/or humans. Thus, there is a pressing demand to make them safe, reliable, and robust to sudden changes. </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Consider for example autonomous cars: these cars share the road as a driving space and need to handle all traffic situations such as changing lanes, negotiating junctions, etc., and additionally to respond robustly to the driver and/or a pedestrian’s sudden intervention, while ensuring the safety on the road. According to the automotive industry standard ISO26262, a self-driving car may need to be tested for 255 million miles without having accident to be verified “fully safe” on the road. Clearly, testing is very expensive and is shown to have low coverage in distributed settings. Indeed, it is very hard to reproduce the error by simply testing for a longer time. </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">We will use Formal Methods instead, and more specifically Controller Synthesis as a design technique. Our goal is to extend existing synthesis techniques to permit native reasoning about time-space related design properties. The work in this project is on the intersection of computer science, control theory, and AI. </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> The thesis will be focused on several aspects of modelling, reasoning, and verification of Situated Autonomous Systems. More specifically, we will target the following:</p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"></p><ul style="margin:0.5em 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none;list-style:outside"><li style="margin:0px 0px 0px 1.75em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Define mathematical formalisms that describe the dynamics (or the semantics) of the system both in Space and Time. The main challenge here is to exploit the finite variability of the physical space to provide representative and compact discrete abstractions that account to the movement in space.</li><li style="margin:0px 0px 0px 1.75em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">We will study Spatio-Temporal logics and identify efficient fragments that permit reasoning about space mobility as time passes.</li><li style="margin:0px 0px 0px 1.75em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Provide online synthesis algorithms that natively analyse a snapshot of the currently observed space and provide short-time horizon control plans.  </li></ul><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Ideal candidates are expected to have knowledge in one or more of the following topics: </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"></p><ul style="margin:0.5em 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none;list-style:outside"><li style="margin:0px 0px 0px 1.75em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Spatio-temporal reasoning.</li><li style="margin:0px 0px 0px 1.75em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Controller synthesis or Supervisory control (Knowledge in model-based reinforcement learning techniques is a plus)
</li><li style="margin:0px 0px 0px 1.75em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Concurrency or applications of Automata in Synthesis and Control.</li></ul><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Please use the instructions in the Joint call (Link below) to apply. More information about the project are available in the project link below.</p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Links:</p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Project description: can be found here <a href="https://chalmers-my.sharepoint.com/:f:/g/personal/sannapet_chalmers_se/Es7l3kX-Xw1Iu1Gx-QZvSaAB1csKLA_SPSQL0YyyeBljbw?e=j56Mfz" target="_blank" rel="nofollow" style="margin:0px;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none;color:rgb(51,102,153);text-decoration:none">Inst.doktorander</a></p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Joint call: <a href="https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=31163" target="_blank" rel="nofollow" style="margin:0px;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none;color:rgb(51,102,153);text-decoration:none">https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=31163</a></p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Note: If you are interested, please forward any informal inquiries directly to me, before submitting your application. 
</p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none"> </p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Many Thanks,</p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Yehia</p><p style="margin:0px 0px 1em;padding:0px;border:0px;outline:0px;font-size:14.4px;vertical-align:baseline;background:none">Plain text email: yehiaa [at] chalmers [dot] se</p></div></div>