ERC Consolidator Project "D-SynMA: Distributed
Synthesis from Single to Multiple
Agents"
Announcement
The project has ended in April 2024, some of our results are still pending publication. We will update here when they are published.
This has been an incredible journey. Thank you for following!
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
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
-
Older news ...
- Accepted for publication: "Distribution of Reconfiguration Languages maintaining Tree-like Communication Topology", by Daniel Hausmann, Mathieu Lehaut, and Nir Piterman, to appear in 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2024) (June 2024).
- Accepted for publication: "A Direct Translation from LTL with Past to Deterministic Rabin Automata", by Shaun Azzopardi, David Lidell, and Nir Piterman, to appear in 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024) (June 2024).
- Accepted for publication: "Faster and Smaller Solutions of Obliging Games", by Daniel Hausmann and Nir Piterman, to appear in 35th International Conference on Concurrency Theory (Concur 2024) (June 2024).
- Accepted for publication: "Adding Reconfiguration to Zielonka's Asynchronous Automata", by Mathieu Lehaut and Nir Piterman, to appear in 15th International Symposium on Games, Automata, Logics, and Formal Verification (Gandalf 2024) (May 2024).
- The project has now ended. We are working on publishing further results that were obtained during the project duration and on the final report of the project (May 2024).
- Accepted for publication: "Synthesis for prefix first-order logic on data words", by Julien Grange and Mathieu Lehaut, to appear in 44th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2024) (Apr 2024).
- Accepted for publication: "Fair Omega-regular Games", by Daniel Hausmann, Nir Piterman, Irmak Saglam and Anne-Kathrin Schmuck to appear in 27th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024) (Dec 2024).
- Accepted for publication: "Symbolic Solution of Emerson-Lei Games for Reactive Synthesis", by Daniel Hausmann, Mathieu Lehaut, and Nir Piterman to appear in 27th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024) (Dec 2024).
- Accepted for publication: "Games for Efficient Supervisor Synthesis", by Daniel Hausmann, Prabhat Kumar Jha, and Nir Piterman to appear in 62nd IEEE Conference on Decision and Control (CDC 2023) (July 2023).
- Accepted for publication: "ppLTLTT: Temporal testing for pure-past linear temporal logic formulae", by Shaun Azzopardi, David Lidell, Nir Piterman, and Gerardo Schneider to appear in 21st International Symposium on Automated Technology for Verification and Analysis (ATVA) (July 2023).
- Accepted for publication: "Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants", by Rocco De Nicola, Luca Di Stefano, Omar Inverso and Serenella Valiani to appear in 21st International Conference on Computational Methods
in Systems Biology (CMSB 2023).
- Accepted for publication: "Games for Efficient Supervisor Synthesis", by Daniel Hausmann, Prabhat Kumar Jha, and Nir Piterman to appear in IEEE Control Systems Letters (L-CSS) (June 2023).
- Accepted for publication: "Compositional verification of priority systems using sharp bisimulation.", by Luca Di Stefano and Frédéric Lang to appear in Formal Methods in System Design (2023).
- Accepted for publication: "Compositional Verification of Stigmergic Collective Systems", by Luca Di Stefano and Frédéric Lang to appear in 24th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2023 (October 2022).
- Accepted for publication:
- "Model Checking Reconfigurable Interacting Systems", by Yehia Abd Alrahman, Shaun Azzopardi, and Nir Piterman; and
- "Runtime Verification meets Controller Synthesis", by Shaun Azzopardi, Nir Piterman, and Gerardo Schneider
in International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) 2022 (August 2022).
-
Accepted for publication:
- "AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification", by Shaun Azzopardi, Joshua Ellul, Ryan Falzon and Gordon Pace;
- "Tainting in Smart Contracts: Combining Static and Runtime Verification", by Shaun Azzopardi, Joshua Ellul, Ryan Falzon and Gordon Pace; and
- "Runtime Verification of Kotlin Coroutines", by Shaun Azzopardi, Denis Furian, Yliès Falcone and Gerardo Schneider
in Runtime Verification 2022 (29th June 2022).
-
Claudia Cauli successfully defended her thesis. We are grateful to Piero Bonatti,
who served as opponent, and Meghyn Bienvenu, Ana Ozaki,
and Sebastian Rudolph, who served as her committee (17 June 2022).
-
Claudia Cauli's thesis is available here. She will be defending on June 17th (31 May 2022).
-
Luca Di Stefano joined our team (1 May 2022).
-
Accepted for publication: "Actions over Core-closed Knowledge Bases"
by Claudia Cauli, Magdalena Ortiz, and Nir Piterman, to appear in IJCAR
(International Joint Conference on Automated Reasoning) 2022. (2 May 2022)
-
Accepted for publication: "R-CHECK: A Model Checker for Verifying Reconfigurable MAS"
by Yehia Abd Alrahman, Shaun Azzopardi, and Nir Piterman, to appear in AAMAS
(Autonomous and Multi-Agent Systems) 2022. (27 January 2022)
-
Prabhat Kumar Jha joined our team (12 January 2022).
-
David Lidell joined our team (10 January 2022).
-
We have started a recruitment process for a postdoctoral researcher. Apply
here (22 December 2021).
-
We are very pleased to announce that Nir Piterman is promoted to a Full Professor at the University of Gothenburg,
Department of Computer Science and Engineering. (26 August 2021)
-
Accepted for publication: "On the Interpretation and Monitoring of Timed Deontic Logics"
by Shaun Azzopardi, Gordon Pace, Fernando Schapachnik, and Gerardo Schneider, to appear in RV
(Runtime Verification) 2021. (20 July 2021)
-
Accepted for publication: "A Linear-Time Nominal mu-Calculus with Name Allocation"
by Daniel Hausmann, Stefan Milius and Lutz Schröder, to appear in MFCS (Mathematical Foundations
of Computer Science) 2021. (1 July 2021)
-
Accepted for publication: "Nominal Büchi Automata with Name Allocation"
by Henning Urbat, Daniel Hausmann, Stefan Milius and Lutz Schröder, to appear in CONCUR
(Concurrency Theory) 2021. (1 July 2021)
-
Accepted for publication: "Modelling and Verification of Reconfigurable Multi-Agent Systems"
by Yehia Abd Alrahman and Nir Piterman, to appear in JAAMAS (the official journal of the
International Foundation for Autonomous Agents and Multi-Agent Systems.)
(29 June 2021)
-
Accepted for publication: "Satisfiability and query answering over open and closed DL-LiteF knowledge bases" by Claudia Cauli, Magdalena Ortiz, and
Nir Piterman, to appear in KR (Knowledge Representation) 2021.
(15 June 2021)
-
PhD project "Combining Path-finding Algorithms in Temporal Reactive Synthesis" chosen for funding by Wallenberg AI, Autonomous Systems and Software Program (WASP) (15 June 2021). Another PhD opening to be available soon ...
-
We have started a recruitment process for a PhD student. Apply
here (9 June 2021).
-
Accepted for publication: "Incorporating Monitors in Reactive Synthesis without Paying the Price" by Shaun Azzopardi,
Nir Piterman, and Gerardo Schneider, to appear in ATVA (Automated Technology for Verification and Analysis) 2021.
(5 June 2021)
-
Mathieu Lehaut joined our team (10 May 2021).
-
Daniel Hausmann joined our team (3 May 2021).
-
Accepted for publication: "Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning" by Claudia Cauli, Meng Li,
Nir Piterman, and Oksana Tkachuk, to appear in CAV (Computer Aided Verification) 2021.
(19 April 2021)
-
PhD position to be available soon ... (18 March 2021).
-
Nir Piterman is editor in chief of Formal Methods in System Design (1 March 2021).
-
Yehia Abd Alrahman is now an independent Young fellow at the Swedish Research Council. He started his VR starting grant
"SynTM: Synthesis of Teamwork Multi-Agent
Systems" 2021-2024. (01 March 2021)
-
We have started a recruitment process for a postdoc. Apply
here (24 January 2021).
-
Accepted for publication: "Synthesis of Run-To-Completion Controllers for Discrete Event Systems" by Yehia Abd Alrahman, Victor Braberman,
Nicolas D'Ippolito, Nir Piterman, and Sebastian Uchitel, to appear in ACC (American Control Conference) 2021.
(24 January 2021)
-
Accepted for publication: "Control and Discovery of Reactive System Environments" by Maureen Keegan, Victor Braberman, Nicolas D'Ippolito,
Nir Piterman, and Sebastian Uchitel, to appear in the
journal of transactions on software engineering. (27 Nov 2020)
-
Yehia Abd Alrahman recieved funding for the VR starting grant
"SynTM: Synthesis of Teamwork Multi-Agent
Systems". Yehia is awarded 4,000,000 SEK for 2021-2024. (29 Oct 2020)
-
Nir Piterman recieved funding for the VR research grant
"Enabling Reactive Synthesis Through
Runtime Verification" . The award is for
4,000,000 SEK for 2021-2024 and will support a PhD
position. (29 Oct 2020)
-
Yehia Abd Alrahman presented "Reconfigurable Interaction for MAS Modelling" in Highlights 2020. (17 Sep
2020)
Here is the poster.
-
Shaun Azzopardi joined our team. (1 Sep 2020)
-
Mauricio Martel joined our team. (1 Jul 2020)
-
Yehia Abd Alrahman presented our
paper "Reconfigurable Interaction for MAS Modelling"
in AAMAS.
(11 May 2020)
-
Our AAMAS paper was invited to a special issue of JAAMAS of best papers from the conference. (23 Apr 2020)
-
Accepted for publication: "Reconfigurable Interaction for MAS Modelling" by Yehia Abd Alrahman, Giuseppe Perelli,
and Nir Piterman, to appear in AAMAS (Autonomous Agents and Multiagent Systems) 2020. (15 Jan 2020)
-
Giuseppe Perelli accepted a research position in Rome. (1 Jan 2020)
-
Accepted for publication: "Combinations of Qualitative Winning for Stochastic Parity Games" by Krishnendu Chatterjee
and Nir Piterman, to appear in Concur 2019.
(14 Jun 2019)
-
Accepted for publication: "Equilibrium Design for Concurrent Games" by Julian Gutierrez, Muhammad Najib, Giuseppe Perelli,
and Michael Wooldridge, to appear in Concur 2019.
(14 Jun 2019)
-
We have moved to the University of Gothenburg. (1 Mar 2019)
-
Accepted for publication: "Environmentally-Friendly GR(1) Synthesis" by Rupak Majumdar, Nir Piterman, and Anne-Kathrin Schmuck,
to appear in TACAS (Tools and Algorithms for the Construction and Analysis of Systems) 2019.
(Jan 25 2019)
-
Yehia Abd Alrahman joined our team. (1 Sep 2018)
-
Giuseppe Perelli joined our team. (1 Jul 2018)
-
Work on the project started! (1 May 2018)
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