Mining Assumptions for SynthesisWenchao LiUC [email protected] DworkinHaverford [email protected] A. SeshiaUC [email protected]—Automatic synthesis of a reactive system fromits formal specification is appealing but often difficult dueto the tedium of writing auxiliary specifications, especiallyon the environment. In several instances, specifications arefound unrealizable as a result of insufficient environmentalassumptions. We present an approach to this problem forsynthesis from LTL based on specification mining. For asatisfiable but unrealizable specification, a counter-strategycan be computed from the synthesis game as a witness tounrealizability. Our algorithm mines environment assumptionsfrom this counter-strategy as well as user scenarios if theyare provided. We argue that our approach is a natural way todiscover the designer’s intent. We demonstrate the effectivenessof our approach on examples from the domains of digitalcircuits and robotic controllers.I. INTRODUCTIONAutomatic synthesis of a reactive system from high-level specifications is a very attractive proposition. A userdescribes the target system using a high-level language, suchas linear temporal logic (LTL), and the tool will producea system that automatically satisifies the specification [20],[26]. Such a synthesis tool can enable the human userto specify core design properties while freeing her of thetedious low-level programming tasks. However, synthesis ischallenging on multiple dimensions: (i) it requires good-quality specifications on the system; (ii) it requires goodmodels (specifications) of the environment, and (iii) the un-derlying decision problems often have very high complexity.Industrial experience indicates that these specifications arehard to get right [14]. In this paper, we address the problemof inadequate environment specifications for synthesis fromLTL.A specification is unsatisfiable if there does not exist anyinput and output sequence that can accomplish the objectiveof the specification. On the other hand, a specification isunrealizable if there is no implementation that can produceoutputs to satisfy the specification given all possible inputsthat can be generated by the environment. Unsatisfiability isa stronger notion of a specification being unsynthesizablethan unrealizabilty. The problem that we are tackling inthis paper is the case when a specification is satisfiable butunrealizable.This class of specifications has been studied in pre-vious work. For example, the requirements analysis toolRATSY [7] is an interactive tool that can analyze un-realizability for Generalized Reactivity(1) specifications(GR(1)) [25]. The tool uses a game-theoretic approach bytaking on the role of the environment while the user takeson the role of the system. The game proceeds by the toolproviding inputs to the system and the user determining theoutputs as an attempt to satisfy the specification. The moveof the tool (and the environment) is a result of the finite-state counter-strategy computed for the environment so asto prevent the system from satisfying the specification.This paper builds upon the above work, using the counter-strategy to further suggest solutions to make the specifi-cation realizable. In particular, we use a template-basedspecification mining approach to find LTL properties that aresatisfied by the counter-strategy. By asserting the negationof these mined properties as an assumption of the originalspecification, we effectively rule out such moves by the en-vironment. We iterate this process until either we cannot finda specification in our library of templates that is satisfied bythe counter-strategy or the resulting specification becomesrealizable.Our work can be viewed as a debugging approach tounrealizability. Unrealizability typically arises either from anunder-constrained environment or from an over-constrainedsystem. We focus on debugging environmental assumptionsrather than system guarantees; note however, that these twoare complementary, and the proposed approach can easilybe adapted to generate guarantees as well. K¨onighofer etal. [23] identify guarantees that can be weakened or signalsthat can be less restricted in order to obtain a realizablespecification. Our focus is on generating additional envi-ronment assumptions, since it is the more tricky problem inpractice — it is often easier to miss an environment behaviorthan to miss a system specification because the formeris not inherently part of the design and seldom formallydefined. Particularly, we want additional assumptions thatare tailored to the type of synthesis (GR(1) in this casehere) and the existing specification. As also noted in [23],the Boolean formula false is also a valid assumption toresolve unrealizability but a trivial and uninteresting one.We propose a template-based specification mining approachto address this problem. By imposing a particular structureon the form of specifications (using templates), we reducethe possibility of generating uninteresting assumptions.Figure 1. Flow of Assumption MiningFigure 1 shows the main flow of our method. Our spec-ification mining algorithm takes in as input a library ofspecification templates, a set of user scenarios (desired I/Otraces of the target implementation), and a counter-strategystate machine generated from unrealizability analysis, andproduces as output a candidate assumption that can be addedto the existing specification to make it realizable.One may argue in favor of an alternate approach where theadditional environment assumption is constructed directlyfrom the counter-strategy so that the resulting specificationis realizable. Chatterjee et al. [12] showed that in fact onecan construct such an assumption by analyzing the gamegraph that is used to answer the realizability question. Infact, the assumption synthesized (as a B¨uchi automaton) isminimal in terms of the number of safety and fair edgesmanipulated in the game graph during synthesis. However,such a monolithic environment assumption (see, e.g., Fig.3 in [12]) can be difficult for a human user to understandeven for correcting a simple specification. Moreover, theB¨uchi automaton synthesized does not directly translate to aLTL description. In addition, the behavior of the weakest as-sumption does not neccessarily coincide with the designer’sintent. We offer an alternative approach that is simpler fromthe theoretical viewpoint but