Mining Assumptions for Synthesis

Unformatted text preview:

Mining Assumptions for Synthesis Wenchao Li UC Berkeley wenchao berkeley edu Lili Dworkin Haverford College ldworkin haverford edu Abstract Automatic synthesis of a reactive system from its formal specification is appealing but often difficult due to the tedium of writing auxiliary specifications especially on the environment In several instances specifications are found unrealizable as a result of insufficient environmental assumptions We present an approach to this problem for synthesis from LTL based on specification mining For a satisfiable but unrealizable specification a counter strategy can be computed from the synthesis game as a witness to unrealizability Our algorithm mines environment assumptions from this counter strategy as well as user scenarios if they are provided We argue that our approach is a natural way to discover the designer s intent We demonstrate the effectiveness of our approach on examples from the domains of digital circuits and robotic controllers I I NTRODUCTION Automatic synthesis of a reactive system from highlevel specifications is a very attractive proposition A user describes the target system using a high level language such as linear temporal logic LTL and the tool will produce a system that automatically satisifies the specification 20 26 Such a synthesis tool can enable the human user to specify core design properties while freeing her of the tedious low level programming tasks However synthesis is challenging on multiple dimensions i it requires goodquality specifications on the system ii it requires good models specifications of the environment and iii the underlying decision problems often have very high complexity Industrial experience indicates that these specifications are hard to get right 14 In this paper we address the problem of inadequate environment specifications for synthesis from LTL A specification is unsatisfiable if there does not exist any input and output sequence that can accomplish the objective of the