SpRInG: A Spatial Relation Inference Generator for Robot Systems

The spatial distribution of sensed objects strongly influences the behavior of mobile robots. Yet, as robots evolve in complexity to operate in increasingly rich environments, it becomes much more difficult to specify the underlying relations between sensed object spatial distributions and robot behaviors. This thesis aims to address this challenge by leveraging system trace data to automatically infer relations that help to better characterize these spatial associations. In particular, we introduce SpRInG, a framework for the unsupervised inference of system specifications from traces that characterize the spatial relationships under which a robot operates. Our method builds on a parameterizable notion of reachability to encode relationships of spatial neighborship, which are used to instantiate a language of patterns. These patterns provide the structure to infer, from system traces, the connection between such relationships and robot behaviors. We show that SpRInG can automatically infer spatial relations over two distinct domains: autonomous vehicles in traffic and a surgical robot. Our results demonstrate the power and expressiveness of SpRInG, in its ability to learn existing specifications as machine-checkable first-order logic, uncover previously unstated specifications that are rich and insightful, and reveal contextual differences between executions.