  There is a growing interest in building autonomous systems that interact with
complex environments. The difficulty associated with obtaining an accurate
model for such environments poses a challenge to the task of assessing and
guaranteeing the system's performance. We present a data-driven solution that
allows for a system to be evaluated for specification conformance without an
accurate model of the environment. Our approach involves learning a
conservative reactive bound of the environment's behavior using data and
specification of the system's desired behavior. First, the approach begins by
learning a conservative reactive bound on the environment's actions that
captures its possible behaviors with high probability. This bound is then used
to assist verification, and if the verification fails under this bound, the
algorithm returns counter-examples to show how failure occurs and then uses
these to refine the bound. We demonstrate the applicability of the approach
through two case-studies: i) verifying controllers for a toy multi-robot
system, and ii) verifying an instance of human-robot interaction during a
lane-change maneuver given real-world human driving data.
