View Full Document


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

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...

Join to view Mining Assumptions for Synthesis and access 3M+ class-specific study document.

We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Mining Assumptions for Synthesis and access 3M+ class-specific study document.


By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?