Keynote
Rupak Majumdar (MPI-SWS): 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.
Invited Talks
Jan Oliver Ringert (Tel Aviv University): 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.
We also present our work in the CAV synthesis session (Thu. 15:30). The talk at SYNT'17 will put more emphasis on GR(1)[F] example specifications, our reduction to GR(1), and initial evaluation.
Sharon Shoham (Tel Aviv University): 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.
Andrew Reynolds (University of Iowa): SyGuS Techniques in the Core of an SMT Solver.
Recent work has shown that SMT solvers, instead of just acting as subroutines for synthesis tasks, can be instrumented to perform synthesis themselves. This talk will overview two techniques for synthesis conjectures in SMT solvers. The first is based on first-order quantifier instantiation, and can be used to tackle a restricted but fairly common class of properties, known as single invocation properties. The second relies on a deep embedding of the synthesis problem into the theory of inductive datatypes, which can then be solved using enumerative syntax-guided techniques. This talk will discuss current challenges for these two techniques. For the first, we describe challenges for devising quantifier instantiation techniques for synthesis for new background theories and ways of minimizing solutions. For the second, we describe how a DPLL(T)-based solver can perform enumerative syntax-guided search while incorporating techniques that prune search space, including those are specialized for programming-by-examples.