@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{fremont-cav18,
author = {Daniel Fremont and Sanjit A. Seshia},
title = {Reactive Control Improvisation},
booktitle = {30th International Conference on Computer Aided Verification (CAV)},
year = {2018},
abstract = {Reactive synthesis is a paradigm for automatically building correct-by-construction
systems that interact with an unknown or adversarial environment.
We study how to do reactive synthesis when part of the specification of
the system is that its behavior should be random. Randomness can be useful, for
example, in a network protocol fuzz tester whose output should be varied, or a
planner for a surveillance robot whose route should be unpredictable. However,
existing reactive synthesis techniques do not provide a way to ensure random behavior
while maintaining functional correctness. Towards this end, we generalize
the recently-proposed framework of control improvisation (CI) to add reactivity.
The resulting framework of reactive control improvisation provides a natural
way to integrate a randomness requirement with the usual functional specifications
of reactive synthesis over a finite window. We theoretically characterize
when such problems are realizable, and give a general method for solving them.
For specifications given by reachability or safety games or by deterministic finite
automata, our method yields a polynomial-time synthesis algorithm. For various
other types of specifications including temporal logic formulas, we obtain a
polynomial-space algorithm and prove matching PSPACE-hardness results. We
show that all of these randomized variants of reactive synthesis are no harder in
a complexity-theoretic sense than ordinary reactive synthesis.},
}