<div dir="ltr"><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">A fully funded 5-year Ph.D. position in Computer Science and Engineering with the subject “<b>Space-Aware Synthesis of Situated Autonomous Systems”</b> 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></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-US" style="font-size:13pt;font-family:"MS Gothic"">
</span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">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. </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">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. </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">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 an 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. </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">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. </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> The thesis will be focused on several aspects of modelling, reasoning, and verification of </span><span style="font-family:AppleSystemUIFont;font-size:13pt">Situated Autonomous Systems. More specifically, we will target the following:</span></p><p class="MsoNormal" style="margin:0cm 0cm 0cm 36pt;text-align:justify;font-size:12pt;font-family:Calibri,sans-serif"><span lang="EN-GB" style="font-size:13pt;font-family:Symbol">·<span style="font-stretch:normal;font-size:7pt;line-height:normal;font-family:"Times New Roman";font-size-adjust:none;font-kerning:auto;font-variant-alternates:normal;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-east-asian:normal;font-feature-settings:normal"> </span></span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">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 physical space.</span></p><p class="MsoNormal" style="margin:0cm 0cm 0cm 36pt;text-align:justify;font-size:12pt;font-family:Calibri,sans-serif"><span lang="EN-GB" style="font-size:13pt;font-family:Symbol">·<span style="font-stretch:normal;font-size:7pt;line-height:normal;font-family:"Times New Roman";font-size-adjust:none;font-kerning:auto;font-variant-alternates:normal;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-east-asian:normal;font-feature-settings:normal">  </span></span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">We will study Spatio-Temporal logics and identify efficient fragments that permit reasoning about space mobility as time passes.</span></p><p class="MsoNormal" style="margin:0cm 0cm 0cm 36pt;text-align:justify;font-size:12pt;font-family:Calibri,sans-serif"><span lang="EN-GB" style="font-size:13pt;font-family:Symbol">·<span style="font-stretch:normal;font-size:7pt;line-height:normal;font-family:"Times New Roman";font-size-adjust:none;font-kerning:auto;font-variant-alternates:normal;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-east-asian:normal;font-feature-settings:normal">  </span></span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Provide online synthesis algorithms that natively analyse a snapshot of the currently observed space and provide short-time horizon control plans. </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Ideal candidates are expected to have knowledge in one or more of the following topics: </span></p><p class="MsoNormal" style="margin:0cm 0cm 0cm 36pt;text-align:justify;font-size:12pt;font-family:Calibri,sans-serif"><span lang="EN-GB" style="font-size:13pt;font-family:Symbol">·<span style="font-stretch:normal;font-size:7pt;line-height:normal;font-family:"Times New Roman";font-size-adjust:none;font-kerning:auto;font-variant-alternates:normal;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-east-asian:normal;font-feature-settings:normal">   </span></span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Spatio-temporal reasoning. </span><span lang="EN-US" style="font-size:13pt;font-family:"MS Gothic"">
</span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"></span></p><p class="MsoNormal" style="margin:0cm 0cm 0cm 36pt;text-align:justify;font-size:12pt;font-family:Calibri,sans-serif"><span lang="EN-GB" style="font-size:13pt;font-family:Symbol">·<span style="font-stretch:normal;font-size:7pt;line-height:normal;font-family:"Times New Roman";font-size-adjust:none;font-kerning:auto;font-variant-alternates:normal;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-east-asian:normal;font-feature-settings:normal">   </span></span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Controller synthesis or Supervisory control (Knowledge in model-based reinforcement learning techniques is a plus)</span><span lang="EN-US" style="font-size:13pt;font-family:"MS Gothic"">
</span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"></span></p><p class="MsoNormal" style="margin:0cm 0cm 0cm 36pt;text-align:justify;font-size:12pt;font-family:Calibri,sans-serif"><span lang="EN-GB" style="font-size:13pt;font-family:Symbol">·<span style="font-stretch:normal;font-size:7pt;line-height:normal;font-family:"Times New Roman";font-size-adjust:none;font-kerning:auto;font-variant-alternates:normal;font-variant-ligatures:normal;font-variant-numeric:normal;font-variant-east-asian:normal;font-feature-settings:normal">    </span></span><span dir="LTR"></span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Concurrency or applications of Automata in Synthesis and Control.</span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span><span lang="EN-US" style="font-size:13pt;font-family:"MS Gothic"">
</span><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"></span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0);text-align:justify"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Please use the instructions in the Joint call (Link below) to apply. More information </span>about the<span style="font-family:AppleSystemUIFont;font-size:13pt"> project is available in the project link below.</span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Links:</span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">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"><span style="color:rgb(220,161,13)">Inst.doktorander</span></a></span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Joint call: <a href="https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=31163" target="_blank"><span style="color:rgb(220,161,13);text-decoration:none">https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=31163</span></a></span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Note: If you are interested, please forward any informal inquiries directly to me, before submitting your application. </span><span lang="EN-US" style="font-size:13pt;font-family:"MS Gothic"">
</span><span lang="EN-GB" style="font-size:13pt;font-family:"MS Gothic""></span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont"> </span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Many Thanks,</span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-GB" style="font-size:13pt;font-family:AppleSystemUIFont">Yehia</span></p><p class="MsoNormal" style="margin:0cm;font-size:medium;font-family:Calibri,sans-serif;color:rgb(0,0,0)"><span lang="EN-US">Plain text email: yehiaa [at] chalmers [dot] se</span></p></div>