We designed novel algorithms and developed reference implementations for weighted model counting and distributionaware sampling of satisfying assignments for a SAT formula. The project was motivated by important applications in synthesis tools. In particular, a distribution-aware sampling used in the underlying solvers for sketch-based synthesis provided guarantees on the convergence to an optimal solution. On the other hand, weighted model counting forms the backbone of computational engines for automatic problem generation in context of MOOCs. Prior work in this area scaled only to small problems in practice, or failed to provide strong theoretical guarantees, or employed a computationally-expensive maximum a posteriori probability (MAP) oracle that assumes prior knowledge of a factored representation of the weight distribution. In the first stage of the project, we contributed two novel algorithms, UniWit and ApproxMC, that provided strong theoretical guarantees and scaled to problems involving thousands of variables. Our model counting algorithm, ApproxMC, is the first scalable approximate model counter to the best of our knowledge. We extended the techniques developed in UniWit and ApproxMC and developed novel algorithms, UniGen and WeightMC, that provide stronger theoretical guarantees and also scales to problems involving hundreds of thousands of variables [CMV13a,CMV13b,CMV14,CFMSV14].

We have started an investigation into the problem of synthesis from component libraries [LV13]. Our goal is to construct an interface abstraction through which the library components can interact. Our motivation is that by using interfaces, every component can be considered as a black-box, and thus a system can be synthesized when only the specification of every component described by an LTL formula is available to the designer. Moreover, interfaces allow the use of hierarchies of compositions which does not exist in the current state-of-the-art.

Synthesis from components is the automated construction of a composite system from a library of reusable components such that the system satisfies the given specification. This is in contrast to classical synthesis, where systems are always constructed from scratch. In the control-flow model of composition, exactly one component is in control at a given time and control is switched to another when the component reaches an exit state. The composition can then be described implicitly by a transducer, called a composer, which statically determines how the system transitions between components. Recently, it was shown that control-flow synthesis of deterministic composers from libraries of probabilistic components is decidable.

In this work, we considered the more general case of probabilistic composers. We showed that probabilistic composers are more expressive than deterministic composers, and that the synthesis problem still remains decidable. In the near future, we will pursue how these theoretical results can help in improving the scalability of reactive synthesis for the robotics application domain [NLV14].

A major critique of reactive synthesis, the problem of synthesizing a reactive system from a given temporal logic formula, is that it shifts the problem of implementing a system that adheres to the specification in mind to formulating a temporal logic formula that expresses it. A potential customer of a computerized system may find it hard to specify his requirements by means of a temporal logic formula. Instead, he might find it easier to provide good and bad examples of ongoing behaviors (or computations) of the required system, or classify a given computation as good or bad. This is a classical scenario for interactive learning of an unknown language using membership and equivalence queries. Regular omega languages are the main means to model reactive systems. Learning omega regular languages using membership and equivalence queries thus provides a mechanism for synthesizing an implementation of a reactive system.

In this work, which is a collaboration with Dana Angluin (Yale), we provide an algorithm for learning an unknown regular set of infinite words, using membership and equivalence queries. Three variations of the algorithm learn three different canonical representations of omega regular languages, using the notion of families of DFAs. One is of size similar to L-dollar, a DFA representation recently learned using L-star [Farzan et al.]. The second is based on the syntactic FORC, introduced in [Maler and Staiger]. The third is a new representation. We show that the second can be exponentially smaller than the first, and the third is at most as large as the first two, with up to a quadratic saving with respect to the second [AF14].

We developed a novel algorithm to synthesize controllers enforcing linear temporal logic specifications on discrete-time linear control systems [RMT13]. The central step within this approach is the computation of the maximal controlled invariant set contained in a possibly non-convex safe set. Although it is known how to compute approximations of maximal controlled invariant sets, its exact computation remains an open problem. We provide an algorithm which computes a controlled invariant set that is guaranteed to be an under-approximation of the maximal controlled invariant set. Moreover, we guarantee that our approximation is at least as good as any invariant set whose distance to the boundary of the safe set is lower bounded. The proposed algorithm is founded on the notion of sets adapted to the dynamics and binary decision diagrams. Contrary to most controller synthesis schemes enforcing temporal logic specifications for control systems, we do not compute a discrete abstraction of the continuous dynamics. Instead, we abstract only the part of the continuous dynamics that is relevant for the computation of the maximal controlled invariant set. For this reason we call our approach specification guided. Our preliminary implementation handles up to five continuous dimensions and specifications containing up to 160 predicates defined as polytopes in about 30 minutes with less than 1GB memory. No other approach to control software synthesis currently scales to 5 continuous variables.

We consider the synthesis of reactive systems from temporal specifications with identifiers, which can parametrize the input and output. We give a new specification formalism for this problem, prove that the synthesis problem is undecidable, and give a sound algorithm based on computing a pattern-based abstraction of the original synthesis game. Results are demonstrated on the Robot Waiter challenge problem formalized in Year 1 of the ExCAPE project. This is one of the first results that extends the theory of synthesis from temporal logic to a richer class of specifications and to synthesis of infinite-state systems [ESK14].

- D. Angluin and D. Fisman. Learning Omega Regular Languages. Algorithmic Learning Theory - 24th International Conference, ALT 2014.
- S. Chakraborty, D. Fremont, K. Meel, S. A. Seshia, and M. Y. Vardi. Distribution-aware sampling and weighted model counting for SAT. In AAAI 2014.
- S. Chakraborty, K.S. Meel, M.Y. Vardi. A Scalable Nearly Uniform Generator of SAT-Witnesses. In Proc. of CAV 2013.
- S. Chakraborty, K.S. Meel, M.Y. Vardi. A Scalable Approximate Model Counter. In Proc. of CP 2013.
- S. Chakraborty, K.S. Meel, M.Y. Vardi. Balancing Scalability and Uniform in SAT WItness Generator. In Proc. of DAC 2014.
- R. Ehlers, S. A. Seshia, and H. Kress-Gazit. Synthesis with identifiers.In Kenneth L. McMillan and Xavier Rival, editors, VMCAI, volume 8318 of Lecture Notes in Computer Science, pages 415–433. Springer, 2014.
- Y. Lustig and M. Y. Vardi. Synthesis from component libraries. STTT, 15(5-6):603–618, 2013.
- S. Nain, Y. Lustig, M. Y. Vardi. Synthesis from Probabilistic Components. CoRR abs/1407.1667 (2014)
- M. Rungger, M.J. Mazo, and P. Tabuada. Specification-guided controller synthesis for linear systems and safe linear-time temporal logic. In Proceedings of the 16th international conference on Hybrid systems: computation and control, pages 333– 342. ACM, 2013.