Processing math: 100%
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

  • 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).
  • Older 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

generated by bibbase.org
  2024 (2)
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis. Hausmann, D., Lehaut, M., & Piterman, N. In Kobayashi, N., & Worrell, J., editor(s), Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14574, of Lecture Notes in Computer Science, pages 55–78, 2024. Springer
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis [link]Paper   doi   link   bibtex   2 downloads  
Fair ω-Regular Games. Hausmann, D., Piterman, N., Saglam, I., & Schmuck, A. In Kobayashi, N., & Worrell, J., editor(s), Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14574, of Lecture Notes in Computer Science, pages 13–33, 2024. Springer
Fair $ω$-Regular Games [link]Paper   doi   link   bibtex  
  2023 (7)
ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae. Azzopardi, S., Lidell, D., Piterman, N., & Schneider, G. In André, É., & Sun, J., editor(s), Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part II, volume 14216, of Lecture Notes in Computer Science, pages 276–287, 2023. Springer
ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae [link]Paper   doi   link   bibtex  
Compositional verification of priority systems using sharp bisimulation. Di Stefano, L., & Lang, F. Formal Methods in System Design. 2023.
Compositional verification of priority systems using sharp bisimulation [link]Paper   doi   link   bibtex   1 download  
Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging Ants. De Nicola, R., Di Stefano, L., Inverso, O., & Valiani, S. In 21st International Conference on Computational Methods in Systems Biology (CMSB), 2023.
doi   link   bibtex  
Language Support for Verifying Reconfigurable Interacting Systems. Abd Alrahman, Y., Azzopardi, S., Di Stefano, L., & Piterman, N. International Journal on Software Tools for Technology Transfer. 2023.
doi   link   bibtex  
Modelling Flocks of Birds and Colonies of Ants from the Bottom Up. De Nicola, R., Di Stefano, L., Inverso, O., & Valiani, S. International Journal on Software Tools for Technology Transfer. 2023.
doi   link   bibtex  
Games for Efficient Supervisor Synthesis. Hausmann, D., Jha, P. K., & Piterman, N. IEEE Control. Syst. Lett., 7: 2881–2885. 2023.
Games for Efficient Supervisor Synthesis [link]Paper   doi   link   bibtex   1 download  
Compositional Verification of Stigmergic Collective Systems. Di Stefano, L., & Lang, F. In Dragoi, C., Emmi, M., & Wang, J., editor(s), Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings, volume 13881, of Lecture Notes in Computer Science, pages 155–176, 2023. Springer
Compositional Verification of Stigmergic Collective Systems [link]Paper   Compositional Verification of Stigmergic Collective Systems [pdf] paper   doi   link   bibtex   1 download  
  2022 (9)
Automated replication of tuple spaces via static analysis. De Nicola, R., Di Stefano, L., Inverso, O., & Uwimbabazi, A. Sci. Comput. Program., 223: 102863. 2022.
Automated replication of tuple spaces via static analysis [link]Paper   Automated replication of tuple spaces via static analysis [pdf] paper   doi   link   bibtex   3 downloads  
Modelling Flocks of Birds from the Bottom Up. De Nicola, R., Di Stefano, L., Inverso, O., & Valiani, S. In Margaria, T., & Steffen, B., editor(s), International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), volume 13703, of Lecture Notes in Computer Science, pages 82–96, 2022. Springer
Modelling Flocks of Birds from the Bottom Up [link]Paper   Modelling Flocks of Birds from the Bottom Up [pdf] paper   doi   link   bibtex   1 download  
A Survey on Satisfiability Checking for the μ-Calculus Through Tree Automata. Hausmann, D., & Piterman, N. In Raskin, J., Chatterjee, K., Doyen, L., & Majumdar, R., editor(s), Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660, of Lecture Notes in Computer Science, pages 228–251, 2022. Springer
A Survey on Satisfiability Checking for the \(μ\)-Calculus Through Tree Automata [link]Paper   doi   link   bibtex  
Model Checking Reconfigurable Interacting Systems. Abd Alrahman, Y., Azzopardi, S., & Piterman, N. In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2022.
link   bibtex   1 download  
Runtime Verification meets Controller Synthesis. Azzopardi, S., Piterman, N., & Schneider, G. In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2022.
link   bibtex   3 downloads  
AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification. Azzopardi, S., Ellul, J., Falzon, R., & Pace, G. In Runtime Verification (RV), 2022.
link   bibtex  
Tainting in Smart Contracts: Combining Static and Runtime Verification. Azzopardi, S., Ellul, J., Falzon, R., & Pace, G. In Runtime Verification (RV), 2022.
link   bibtex  
Runtime Verification of Kotlin Coroutines. Azzopardi, S., Furian, D., Falcone, Y., & Schneider, G. In Runtime Verification (RV), 2022.
link   bibtex  
R-CHECK: A Model Checker for Verifying Reconfigurable MAS. Abd Alrahman, Y., Azzopardi, S., & Piterman, N. In Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, of AAMAS '22, pages 1518–1520, Richland, SC, 2022. International Foundation for Autonomous Agents and Multiagent Systems
link   bibtex   abstract   6 downloads  
  2021 (7)
Incorporating Monitors in Reactive Synthesis Without Paying the Price. Azzopardi, S., Piterman, N., & Schneider, G. In Hou, Z., & Ganesh, V., editor(s), Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings, volume 12971, of Lecture Notes in Computer Science, pages 337–353, 2021. Springer
Incorporating Monitors in Reactive Synthesis Without Paying the Price [link]Paper   doi   link   bibtex   2 downloads  
On the Specification and Monitoring of Timed Normative Systems. Azzopardi, S., Pace, G., Schapachnik, F., & Schneider, G. In Runtime Verification: 21st International Conference, RV 2021, Virtual Event, October 11–14, 2021, Proceedings, pages 81–99, Berlin, Heidelberg, 2021. Springer-Verlag
On the Specification and Monitoring of Timed Normative Systems [link]Paper   doi   link   bibtex   abstract  
A Linear-Time Nominal μ-Calculus with Name Allocation. Hausmann, D., Milius, S., & Schröder, L. In Bonchi, F., & Puglisi, S. J., editor(s), 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia, volume 202, of LIPIcs, pages 58:1–58:18, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik
A Linear-Time Nominal \(μ\)-Calculus with Name Allocation [link]Paper   doi   link   bibtex  
Nominal Büchi Automata with Name Allocation. Urbat, H., Hausmann, D., Milius, S., & Schröder, L. In Haddad, S., & Varacca, D., editor(s), 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203, of LIPIcs, pages 4:1–4:16, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Nominal Büchi Automata with Name Allocation [link]Paper   doi   link   bibtex  
Modelling and Verification of Reconfigurable Multi-Agent Systems. Abd Alrahman, Y., & Piterman, N. Autonomous Agents and Multi-Agent Systems, 35. August 2021.
Modelling and Verification of Reconfigurable Multi-Agent Systems [link]Paper   doi   link   bibtex   abstract   11 downloads  
Synthesis of Run-To-Completion Controllers for Discrete Event Systems. Abd Alrahman, Y., Braberman, V. A., D'Ippolito, N., Piterman, N., & Uchitel, S. In 2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 25-28, 2021, pages 4892–4899, 2021. IEEE
Synthesis of Run-To-Completion Controllers for Discrete Event Systems [link]Paper   doi   link   bibtex   abstract   11 downloads  
Control and Discovery of Reactive System Environments. Keegan, M., Braberman, V. A., D'Ippolito, N., Piterman, N., & Uchitel, S. IEEE Transactions on Software Engineering. 2021. To appear
Control and Discovery of Reactive System Environments [link]Paper   link   bibtex   4 downloads  
  2020 (3)
Reconfigurable Interaction for MAS Modelling. Abd Alrahman, Y., Perelli, G., & Piterman, N. In Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems, of AAMAS '20, pages 7-15, Richland, SC, 2020. International Foundation for Autonomous Agents and Multiagent Systems
Reconfigurable Interaction for MAS Modelling [link]Paper   link   bibtex   abstract   29 downloads  
A distributed API for coordinating AbC programs. Abd Alrahman, Y., & Garbi, G. International Journal on Software Tools for Technology Transfer. feb 2020.
A distributed API for coordinating AbC programs [link]Paper   doi   link   bibtex   abstract   2 downloads  
Programming interactions in collective adaptive systems by relying on attribute-based communication. Abd Alrahman, Y., De Nicola, R., & Loreti, M. Sci. Comput. Program., 192: 102428. 2020.
Programming interactions in collective adaptive systems by relying on attribute-based communication [link]Paper   doi   link   bibtex   abstract   1 download  
  2019 (10)
Equilibrium Design for Concurrent Games. Gutierrez, J., Najib, M., Perelli, G., & Wooldridge, M. In 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands., pages 22:1–22:16, 2019.
Equilibrium Design for Concurrent Games [link]Paper   link   bibtex  
On Computational Tractability for Rational Verification. Gutierrez, J., Najib, M., Perelli, G., & Wooldridge, M. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 329–335, 2019.
On Computational Tractability for Rational Verification. [link]Paper   link   bibtex  
Reasoning about Quality and Fuzziness of Strategic Behaviours. Bouyer, P., Kupferman, O., Markey, N., Maubert, B., Murano, A., & Perelli, G. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 1588–1594, 2019.
Reasoning about Quality and Fuzziness of Strategic Behaviours. [link]Paper   link   bibtex  
Enforcing Equilibria in Multi-Agent Systems. Perelli, G. In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS '19, Montreal, QC, Canada, May 13-17, 2019, pages 188–196, 2019.
Enforcing Equilibria in Multi-Agent Systems. [link]Paper   link   bibtex   6 downloads  
Nash Equilibrium and Bisimulation Invariance. Gutierrez, J., Harrenstein, P., Perelli, G., & Wooldridge, M. In Logical Methods in Computer Science, volume 15, issue 3. 2019.
doi   link   bibtex   1 download  
A calculus for collective-adaptive systems and its behavioural theory. Abd Alrahman, Y., De Nicola, R., & Loreti, M. Inf. Comput., 268. 2019.
A calculus for collective-adaptive systems and its behavioural theory [link]Paper   doi   link   bibtex   abstract   3 downloads  
A coordination protocol language for power grid operation control. Abd Alrahman, Y., & Vieira, H. T. J. Log. Algebraic Methods Program., 109. 2019.
A coordination protocol language for power grid operation control [link]Paper   doi   link   bibtex   abstract   4 downloads  
Testing for Coordination Fidelity. Abd Alrahman, Y., Mezzina, C. A., & Vieira, H. T. In Boreale, M., Corradini, F., Loreti, M., & Pugliese, R., editor(s), Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, volume 11665, of Lecture Notes in Computer Science, pages 152-169, 2019. Springer
Testing for Coordination Fidelity [link]Paper   doi   link   bibtex   abstract   3 downloads  
Combinations of Qualitative Winning for Stochastic Parity Games. Chatterjee, K., & Piterman, N. In 30th International Conference on Concurrency Theory, of LIPIcs, pages 229-246, Amsterdam, Netherlands, August 2019. Schloss Dagstuhl
link   bibtex  
Environmentally-Friendly GR(1) Synthesis. Majumdar, R., Piterman, N., & Schmuck, A. In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 11428, of Lecture Notes in Computer Science, pages 229-246, Prague, Czech Republic, April 2019.
Environmentally-Friendly GR(1) Synthesis [pdf] paper   link   bibtex   11 downloads