Data-Driven Controller Synthesis via Finite Abstractions With Formal Guarantees

Construction of finite-state abstractions (a.k.a. symbolic abstractions) is a promising approach for formal verification and controller synthesis of complex systems. Finite-state abstractions provide simpler models that can replicate the behaviors of original complex systems. These abstractions are usually constructed by leveraging precise knowledge of systems' dynamics, which is often unknown in real-life applications. In this letter, we develop a data-driven technique for constructing finite abstractions for continuous-time control systems with unknown dynamics. In our data-driven context, we collect samples from trajectories of unknown systems to construct finite abstractions with a guarantee of correctness. We propose a data-based gridding method to efficiently determine state-set discretization parameters while minimizing the expected number of transitions in the abstraction construction, thus reducing computational efforts. By establishing a feedback refinement relationship between an unknown system and its data-driven finite abstraction, one can design a controller over the data-driven finite abstraction. The controller can then be refined back to the original unknown system to meet a desired property of interest. We illustrate our proposed data-driven approach using a vehicle motion planning benchmark.