FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Reactive Control Improvisation

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: