HooVer: A Framework for Verification and Parameter Synthesis in Stochastic Systems using Optimistic Optimization

This paper provides a new approach for probabilistic verification of control and dynamical systems in the scenario where there is a finite computational budget that must be used judiciously; it is based on leveraging multiarmed bandits theory from machine learning. We present an algorithm for formal verification and parameter synthesis of continuous state-space Markov chains, introduce our associated computational tool HooVer, and demonstrate their use on example applications. The problem class considered captures the design and analysis of a wide variety of autonomous and cyber-physical systems defined by nonlinear and black-box modules. In order to solve these problems, one has to maximize certain probabilistic objective functions over all choices of initial states and parameters. In this paper, we identify the assumptions that make it possible to view this problem as a multi-armed bandit problem. Based on this fresh perspective, we propose an algorithm Hierarchical Optimistic Optimization algorithm with Mini-batches (HOO-MB) for solving the problem that carefully instantiates an existing bandit algorithm - Hierarchical Optimistic Optimization - with appropriate parameters. As a consequence, we obtain theoretical regret bounds on sample efficiency of our solution that depend on key problem parameters like smoothness, near-optimality dimension, and batch size. The batch size parameter enables us to strike a balance between the sample efficiency and the memory usage of the algorithm. Experiments, using our open-source tool HooVer, suggest that the approach scales to realistic-sized problems and is often more sample-efficient compared to PlasmaLab - a leading tool for verification of stochastic systems. Specifically, HooVer has distinct advantages in analyzing models in which the objective function has sharp slopes. In addition, HooVer shows promising behavior in parameter synthesis for a linear quadratic regulator (LQR) example.