Authors: Daniel J. Fremont and Sanjit A. Seshia
Paper Information
Title: | Reactive Control Improvisation |
Authors: | Daniel J. Fremont and Sanjit A. Seshia |
Proceedings: | CAV All Papers |
Editors: | Georg Weissenbacher, Hana Chockler and Igor Konnov |
Keywords: | reactive synthesis, control improvisation, formal languages and automata theory, probabilistic games, robotic planning |
Abstract: | ABSTRACT. Reactive synthesis has become a widely-used paradigm for automatically building correct-by-construction implementations for 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. There are several examples of such systems, including 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 introduce a notion of randomized reactive synthesis based on the recently-proposed framework of control improvisation (CI). This framework provides a natural way to integrate a randomness requirement with the usual functional specifications of reactive synthesis. We define a reactive version of CI which can be used to solve randomized reactive synthesis problems over finite windows. We theoretically characterize when such problems are realizable, and give a general method for solving them. For specifications given by reachability/safety games or 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. In all of these cases, we show that randomized reactive synthesis is no harder in a complexity-theoretic sense than ordinary reactive synthesis. |
Pages: | 18 |
Talk: | Jul 14 16:45 (Session 99A: Synthesis) |
Paper: |