Verification and Parameter Synthesis for Stochastic Systems using Optimistic Optimization
Negin Musavi, Dawei Sun, Sayan Mitra, Geir Dullerud, Sanjay Shakkottai

TL;DR
This paper introduces a novel algorithm for formal verification and parameter synthesis of continuous state-space Markov chains, leveraging optimistic optimization and bandit problem techniques to improve sample efficiency and scalability.
Contribution
It reformulates the verification problem as a multi-armed bandit problem and proposes HOO-MB, an algorithm with theoretical regret bounds and practical advantages over existing tools.
Findings
HooVer scales to realistic-sized problems.
HooVer is more sample-efficient than PlasmaLab.
HooVer performs well on models with sharp objective function slopes.
Abstract
We present an algorithm for formal verification and parameter synthesis of continuous state-space Markov chains. This class of problems 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 overall 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 (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 depends on key problem parameters like…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Bandit Algorithms Research · Reinforcement Learning in Robotics · Gaussian Processes and Bayesian Inference
