Automatic Synthesis of Distributed and Parameterized Systems (ASDPS)

Project Description

• Principal Investigator: Swen Jacobs
• Scientific Assistant: Mouhammad Sakr
• Funding: DFG research grant
• Funding Period: 2015-2017 (extended to 2019)

Project Goals

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.

Publications

• Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings (N. Mirzaie, F. Faghih, S. Jacobs and B. Bonakdarpour)
  in OPODIS 2018, LIPIcs 125, 2018, pages 29:1-29:17.

• Design Understanding: From Logic to Specification
  (G. Fey, T. Ghasempouri, S. Jacobs, G. Martino, J. Raik and H. Riener)
  in VLSI-SoC 2018, IEEE, 2018, pages 172-175.

• A Symbolic Algorithm for Lazy Synthesis of Eager Strategies (S. Jacobs and M. Sakr)
  in ATVA 2018, LNCS 11138, 2018, pages 211-227.

• Distributed Synthesis for Parameterized Temporal Logics (S. Jacobs, L. Tentrup and M. Zimmermann)
  in Information & Computation 262(2), 2018, pages 311-328.

• Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity (S. Jacobs and M. Sakr)
  in VMCAI 2018, LNCS 10747, 2018, pages 247-268.

• The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants and Results (S. Jacobs, N. Basset, R. Bloem, R. Brenguier, M. Colange, P. Faymonville, B. Finkbeiner, A. Khalimov, F. Klein, T. Michaud, G. A. Pérez, J.-F. Raskin, O. Sankur, L. Tentrup)
  in SYNT 2017, EPTCS 260, 2017, pages 116-143.

• The Third Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants and Results
  (S. Jacobs, 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 (S. Jacobs and R. Bloem)
  in SYNT 2016, EPTCS 229, 2016, pages 133-148.

• A High-Level LTL Synthesis Format: TLSF v1.1 (S. Jacobs, F. Klein and S. Schirmer)
  in SYNT 2016, EPTCS 229, 2016, pages 112-132.

• Distributed PROMPT-LTL Synthesis (S. Jacobs, L. Tentrup and M. Zimmermann)
  in GandALF 2016, EPTCS 226, 2016, pages 228-241.

• Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems (R. Bloem, N. Braud-Santoni and S. Jacobs)
  in CAV 2016, LNCS 9779, pages 157-176.

• Decidability in Parameterized Verification
  (R. Bloem, S. Jacobs, 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)
  (S. Jacobs, 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)
  (S. Jacobs, 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 (S. Außerlechner, S. Jacobs 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.