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 6 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-2024

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

    We currently have no open positions. We will update when more positions become available.

    D-SynMA Publications