Preface

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

• Roderick Bloem, Graz University of Technology, Austria
• Swarat Chaudhuri, Rice University, USA
• Pedro R. D'Argenio, Universidad Nacional de C\'ordoba - CONICET, Argentina
• Rayna Dimitrova, The University of Texas at Austin, USA
• Rüdiger Ehlers, University of Bremen, Germany
• Bernd Finkbeiner, Saarland University, Germany
• Dana Fisman, Ben-Gurion University, Israel
• Swen Jacobs, Saarland University, Germany
• Stephane Lafortune, University of Michigan, USA
• Alessio Lomuscio, Imperial College London, UK
• Doron Peled, Bar Ilan University, Israel
• Ruzica Piskac, Yale University, USA
• Nadia Polikarpova, University of California San Diego, USA
• Arjun Radhakrishna, University of Pennsylvania, USA
• Veselin Raychev, ETH Zurich, Switzerland
• Roopsha Samanta, Purdue University, USA
• Ocan Sankur, CNRS, France
• Sven Schewe, University of Liverpool, UK
• Armando Solar-Lezama, MIT, USA
• Ufuk Topcu, University of Texas at Austin, USA
• Frits Vaandrager, Radboud University Nijmegen, Netherlands
• Damien Zufferey, MPI-SWS, Germany

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

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

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].

References

Synthesizing Universally-Quantified Inductive Invariants

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.