ERC Consolidator Project "D-SynMA: Distributed Synthesis from Single to Multiple Agents"

Announcement

We are very pleased to announce that Prof. Nir Piterman is awarded an ERC Consolidator Grant for the project "D-SynMA: Distributed Synthesis from Single to Multiple Agents". The main aim of the project is to develop the theoretical foundations that will enable reactive synthesis in the context of multiple agents. This includes studying two-player games and their solutions, modelling solutions for interacting agents, and studies of temporal logic. (see project summary below).

The project is 5 years long and will include funding for several postdoc positions supervised by Nir Piterman at the University of Gothenburg in Gothenburg, Sweden.


Grant agreement ID: 772459

Overall budget: € 1 871 272

Duration: 2018-2023

The Scope of D-SynMA

The concept of reactive-synthesis is a long-standing dream of the formal methods community going back to A. Church. Reactive Synthesis is a formal method for automatically generating input-enabled programs from formal descriptions of desired behaviours and interactions. For example, a robot may need to arrive at a certain location whilst making sure that it never collides with objects. Synthesized programs then, by construction, fulfil their specified goals in a dynamically evolving environment. The promise of correct- by-construction of systems promises to revolutionize the design of reactive systems and has been a long standing dream of the community. In recent years, the correct-by-construction development of robots and software systems is becoming a reality. The techniques to make systems safe and reliable are investigated and are starting to emerge and consolidate. However, these techniques enable devices to work in isolation or co-exist. We currently do not have techniques that enable development of real autonomous collaboration between devices. Such techniques will revolutionize all usage of devices and, as consequence, our lives. Manufacturing, supply chain, transportation, infrastructures, and earth- and space exploration would all transform using techniques that enable development of collaborating devices. When considering isolated (and co-existing) devices, reactive synthesis automatic production of plans from high level specification is emerging as a viable tool for the development of robots and reactive software. This is especially important in the context of safety-critical systems, where assurances are required and systems need to have guarantees on performance. The techniques that are developed today to support robust, assured, reliable, and adaptive devices rely on a major change in focus of reactive synthesis. The revolution of correct- by-construction systems from specifications is occurring and is being pushed forward. However, to take this approach forward to work also for real collaboration between devices the theoretical frameworks that will enable distributed synthesis are required. Such foundations will enable the correct-by- construction revolution to unleash its potential and allow a multiplicative increase of utility by cooperative computation. D-SynMA will take distributed synthesis to this new frontier by considering novel interaction and communication concepts that would create an adaptable framework of correct-by-construction application of collaborating devices.

News

    The D-SynMA team

    The D-SynMA team, led by Nir Piterman at the University of Gothenburg, study theoretical foundations that will enable to apply reactive synthesis from temporal specifications to work for multiple agents. This includes studying two-player games and their solutions, modelling solutions for interacting agents, and studies of temporal logic. Specifically, research will focus on the following objectives:
    • Consider modelling frameworks that combine message passing and variable sharing allowing for synchronization as well as passage of information;
    • Work on algorithmic analysis of games that arise from combinations of multiple agents supporting rich modelling features. This includes analysis of partial information games and applications of abstraction and compositionality to games analysis;
    • Study specification languages that extend temporal and strategy logic by allowing to reason about how agents interact as well as what are their goals. Algorithmically analyse games that arise from such specifications.

    Team Members

    Former Members

    We are collaborating actively with a number of researchers around the world on topics related to the D-SynMA project. We have generous funds available for members of the D-SynMA team to travel and visit with our collaborators.

    Open positions

    Postdoctoral positions

    For the postdoc positions, we are seeking exceptional candidates with a strong, internationally competitive track record of research in verification. More Specifically, we are interested in candidates who have specialized expertise in one or more of the following areas:

    • Theory of Computation, Logics and Games;
    • Automata on Infinite Objects;
    • Model Checking and Temporal logics;
    • Reactive Synthesis and/or Supervisory Control.
    Experience in programming is a plus, but not required. Our view is that a postdoc position aims to give new holders of the doctorate the opportunity mainly to strengthen and develop their scholarly proficiency. For this reason, we aim for those who have a doctoral degree not older than 3 years counting from last date of application.

    PhD student positions

    For the PhD student positions, we are seeking exceptional candidates who have background in the theory of computation and/or formal methods, and who are eager to work on deep foundational problems in computing. A bachelor's and a master's degree are required. The thesis research will be conducted under Prof. Piterman's supervision at the University of Gothenburg in Gothenburg, Sweden. The working language at the University of Gothenburg is English.

    How to apply

    If you are interested in a postdoc or PhD position working on D-SynMA and/or related projects, please send email directly to Prof. Nir Piterman. Please note in your application that you are interested in the D-SynMA project. Starting dates are negotiable.

    D-SynMA Publications