Automatic Synthesis of Distributed and Parameterized Systems (ASDPS)
- Principal Investigator: Swen Jacobs
- Scientific Assistant: Mouhammad Sakr
- Funding: DFG research grant
- Funding Period: 2015-2017
This project aims at developing new methods and tools for the verification and synthesis of distributed and parameterized systems, such as communication protocols with a given or even a parametric number of components. To this end, we study approaches for the verification of distributed and parameterized systems and generalize the underlying ideas to develop novel methods for the more difficult task of automatic synthesis. This includes the development of efficient methods for the distributed synthesis problem with finite-state components, reductions from parameterized to distributed verification and synthesis, and methods for the synthesis of distributed infinite-state systems.
- The Third Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants and Results
(with R. Bloem, R. Brenguier, A. Khalimov, F. Klein, R. Könighofer, J. Kreber, A. Legg, N. Narodytska, G. A. Pérez, J.-F. Raskin, L. Ryzhyk, O. Sankur, M. Seidl, L. Tentrup and A. Walker)
in SYNT 2016, EPTCS 229, 2016, pages 149-177.
- The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond (with R. Bloem)
in SYNT 2016, EPTCS 229, 2016, pages 133-148.
- A High-Level LTL Synthesis Format: TLSF v1.1 (with F. Klein and S. Schirmer)
in SYNT 2016, EPTCS 229, 2016, pages 112-132.
- Distributed PROMPT-LTL Synthesis (with L. Tentrup and M. Zimmermann)
in GandALF 2016, EPTCS 226, 2016, pages 228-241.
- Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems (with R. Bloem and N. Braud-Santoni)
in CAV 2016, LNCS 9779, pages 157-176.
- Decidability in Parameterized Verification
(with R. Bloem, A. Khalimov, I. Konnov, S. Rubin, H. Veith and J. Widder)
in ACM SIGACT News 47(2), 2016, pages 53-64.
- The First Reactive Synthesis Competition (SYNTCOMP 2014)
(with R. Bloem, R. Brenguier, R. Ehlers, T. Hell, R. Könighofer, G. A. Pérez, J.-F. Raskin, L. Ryzhyk, O. Sankur, M. Seidl, L. Tentrup and A. Walker)
in STTT 2016 (published online first, journal issue to appear).
- The Second Reactive Synthesis Competition (SYNTCOMP 2015)
(with R. Bloem, R. Brenguier, R. Könighofer, G. A. Pérez, J.-F. Raskin, L. Ryzhyk, O. Sankur, M. Seidl, L. Tentrup and A. Walker)
in SYNT 2015, EPTCS 202, pages 27-57.
- Tight Cutoffs for Guarded Protocols with Fairness (with S. Außerlechner and A. Khalimov)
in VMCAI 2016, LNCS 9583, pages 476-494. Full version on arXiv.
- Decidability of Parameterized Verification
(R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith and J. Widder)
in series: Synthesis Lectures in Distributed Computing Theory, Morgan & Claypool. September 2015.
- Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
(R. Bloem, K.Chatterjee, S. Jacobs and R. Koenighofer)
in TACAS 2015, LNCS 9035, pages 517-532.
Extended version available on arXiv.