Mining Assumptions for Synthesis

Wenchao Li, Lili Dworkin, and Sanjit A. Seshia. Mining Assumptions for Synthesis. In Proceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011.

Download

[pdf] 

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. and also makes use of the counter-trace when one exists. We argue that our approach is a natural way to discover the designers intent. We demonstrate the effectiveness of our approach on examples from the domains of digital circuits and robotic controllers.

BibTeX

@InProceedings{li-memocode11,
  author = 	 {Wenchao Li and Lili Dworkin and Sanjit A. Seshia},
  title = 	 {Mining Assumptions for Synthesis},
  booktitle = 	 {Proceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)}, 
  month = {July},
  year = 	 {2011},
  OPTpages = {},
  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. and also makes use of
 the counter-trace when one exists. We argue that our approach is
 a natural way to discover the designers intent. We demonstrate
 the effectiveness of our approach on examples from the domains
 of digital circuits and robotic controllers.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Wed Jan 11, 2012 13:02:54