@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{ehlers-vmcai14,
  author    = {R{\"{u}}diger Ehlers and Sanjit A. Seshia and Hadas Kress-Gazit},
  title     = {Synthesis with Identifiers},
 booktitle = {Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
 month = "January",
 year = {2014},
 pages = {415--433},
 abstract = {We consider the synthesis of reactive systems from specifications with 
identifiers. Identifiers are useful to parametrize the input and output of a reactive 
system, for example, to state which client requests a grant from an arbiter, or the 
type of object that a robot is expected to fetch. 
Traditional reactive synthesis algorithms only handle a constant bounded range 
of such identifiers. However, in practice, we might not want to restrict the number 
of clients of an arbiter or the set of object types handled by a robot a priori. We 
first present a concise automata-based formalism for specifications with identifiers. 
The synthesis problem for such specifications is undecidable. We therefore 
give an algorithm that is always sound, and complete for unrealizable safety specifications. 
Our algorithm is based on computing a pattern-based abstraction of a 
synthesis game that captures the realizability problem for the specification. The 
abstraction does not restrict the possible solutions to finite-state ones and captures 
the obligations for the system in the synthesis game. We present an experimental 
evaluation based on a prototype implementation that shows the practical applicability 
of our algorithm.},
  wwwnote = {Extended version available <a href="http://www.eecs.berkeley.edu/~sseshia/pubdir/vmcai2014-final-extended.pdf">here</a>.}
}