Published: 28th November 2017
DOI: 10.4204/EPTCS.260
ISSN: 2075-2180


Proceedings Sixth Workshop on
Heidelberg, Germany, 22nd July 2017

Edited by: Dana Fisman and Swen Jacobs

Dana Fisman and Swen Jacobs
Invited Presentation: Synthesis Challenges in Building a Multi-Robot Task Server
Rupak Majumdar
Invited Presentation: Quantitative Assume Guarantee Synthesis
Jan Oliver Ringert
Invited Presentation: Synthesizing Universally-Quantified Inductive Invariants
Sharon Shoham
CTL* synthesis via LTL synthesis
Roderick Bloem, Sven Schewe and Ayrat Khalimov
Symbolic vs. Bounded Synthesis for Petri Games
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch and Ernst-Rüdiger Olderog
A Class of Control Certificates to Ensure Reach-While-Stay for Switched Systems
Hadi Ravanbakhsh and Sriram Sankaranarayanan
Performance Heuristics for GR(1) Synthesis and Related Algorithms
Elizabeth Firman, Shahar Maoz and Jan Oliver Ringert
Invited Paper: SyGuS Techniques in the Core of an SMT Solver
Andrew Reynolds and Cesare Tinelli
SyGuS-Comp 2017: Results and Analysis
Rajeev Alur, Dana Fisman, Rishabh Singh and Armando Solar-Lezama
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
Swen Jacobs, Nicolas Basset, Roderick Bloem, Romain Brenguier, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Thibaud Michaud, Guillermo A. Pérez, Jean-François Raskin, Ocan Sankur and Leander Tentrup


The idea of system synthesis, the process of automatically computing implementations from their specifications, dates back to Church [1957]. For several decades, synthesis was considered impractical because of the high complexity of the solving algorithms. However, research on synthesis has recently gained a lot of momentum, with concrete applications showing that it can be useful, for instance, for designing the intricate pieces of code that most programmers find challenging, or for orchestrating tasks in reactive environments.

The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Application domains include software, hardware, embedded, and cyber-physical systems. Computation models include functional, reactive, hybrid and timed systems. Identifying, formalizing, and evaluating synthesis in concrete application domains is encouraged.

The sixth iteration of the workshop took place on July 22, 2017 in Heidelberg, Germany. It was co-located with the 29th International Conference on Computer Aided Verification. The program featured a keynote talk by Rupak Majumdar (Max Planck Institute for Software Systems), four contributed talks and three invited talks. In addition, it featured a special session about the Syntax-Guided Synthesis Competition (SyGuS-Comp) and the Reactive Synthesis Competition (SYNTCOMP).

The program committee of SYNT 2017, comprising of

has selected the contributed papers contained in this EPTCS volume, and additional reviews were contributed by Jesko Jecking-Harbusch and Felix Klein. All regular papers were reviewed by at least three reviewers. After the workshop, the authors of all papers were asked to submit a revised version, incorporating the comments made during the discussion at the workshop.

We thank the organizers of CAV 2017 for their support in the organization of this workshop, the Austrian National Research Network RiSE (Rigorous Systems Engineering) for sponsorship of the workshop, as well as all the authors, the invited speakers, the programme committee, and the external referees for their valuable contributions.

November 2017, Dana Fisman and Swen Jacobs (Program Co-chairs)

Synthesis Challenges in Building a Multi-Robot Task Server

Rupak Majumdar (Max Planck Institute for Software Systems)

In this talk, I will talk about synthesis challenges that arose in our attempts to build Antlab, an end-to-end system that takes streams of user task requests and executes them using collections of robots. In Antlab, each request is specified declaratively in linear temporal logic extended with quantifiers over robots. The user does not program robots individually, nor know how many robots are available at any time or the precise state of the robots. The Antlab runtime system manages the set of robots, schedules robots to perform tasks, automatically synthesizes robot motion plans from the task specification, and manages the co-ordinated execution of the plan.

We are using Antlab as a vehicle to test out different ideas in synthesis. I will describe a repeated re-planning and dynamic conflict resolution algorithm and its hierarchical version. On the theoretical side, I will describe a game problem with dynamic and stochastic rewards which get discounted over time. I will conclude with our unfinished attempts to understand the "right" notion of compositionality in synthesis.

This talk represents joint work with Rayna Dimitrova, Ivan Gavran, Adrian Leva, Kaushik Mallik, Thomas Moor, Vinayak Prabhu, Indranil Saha, Anne-Kathrin Schmuck, Sadegh Soudjani, and Damien Zufferey.

Quantitative Assume Guarantee Synthesis

Jan Oliver Ringert (Tel Aviv University)

In assume-guarantee synthesis, we are given a specification (A,G), describing an assumption on the environment and a guarantee for the system, and we construct a system that interacts with an environment and is guaranteed to satisfy G whenever the environment satisfies A. While assume-guarantee synthesis is 2EXPTIME-complete for specifications in LTL, researchers have identified the GR(1) fragment of LTL, which supports assume-guarantee reasoning and for which synthesis has an efficient symbolic solution. In recent years we see a transition to quantitative synthesis, in which the specification formalism is multi-valued and the goal is to generate high-quality systems, namely ones that maximize the satisfaction value of the specification.

We study quantitative assume-guarantee synthesis. We start with specifications in LTL[F], an extension of LTL by quality operators. The satisfaction value of an LTL[F] formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification.

We define the quantitative extension GR(1)[F] of GR(1). We show that the implication relation, which is at the heart of assume-guarantee reasoning, has two natural semantics in the quantitative setting. Indeed, in addition to max{1-A,G}, which is the multi-valued counterpart of Boolean implication, there are settings in which maximizing the ratio G/A is more appropriate. We show that GR(1)[F] formulas in both semantics are hard to synthesize. Still, in the implication semantics, we can reduce GR(1)[F] synthesis to GR(1) synthesis and apply its efficient symbolic algorithm. For the ratio semantics, we present a sound approximation, which can also be solved efficiently. Our experimental results show that our approach can successfully synthesize GR(1)[F] specifications with over a million of concrete states.

This invited talk presented joint work with Shaull Almagor, Orna Kupferman, and Yaron Velner. A paper with the same title is published as [1].


[1] Shaull Almagor, Orna Kupferman, Jan Oliver Ringert & Yaron Velner (2017): Quantitative Assume Guarantee Synthesis. In Rupak Majumdar & Viktor Kuncak, editors: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, Lecture Notes in Computer Science 10427, Springer, pp. 353-374, doi:10.1007/978-3-319-63390-9_19.

Synthesizing Universally-Quantified Inductive Invariants

Sharon Shoham (Tel Aviv University)

A fundamental approach for safety verification is the use of inductive invariants - properties that hold initially, imply the safety property, and are preserved by every step of the system. A common practice is to model a system using logical formulas, and then come up with an inductive invariant in the form of a logical formula. For infinite-state systems (such as programs that manipulate dynamic memory, or distributed algorithms that are designed to run on any number of nodes), these formulas are in many cases quantified.

In this talk I will discuss recent approaches for synthesizing inductive invariants in the form of universally-quantified formulas in uninterpreted first-order logic. The key idea is to generalize from concrete counterexamples to induction into universally-quantified clauses based on the logical notion of a diagram.