In previous work [1]}, we introduce a data-driven formal control synthesis framework for unknown stochastic systems. The framework takes a set of input-output data of the system and a desired property in LTL on finite traces (LTLf) [2]} as input and synthesizes a robust control policy with guaranteed lower-bound on the probability of achieving the LTLf property. The method employs GP regression and a discretization to construct an abstraction in the form of an uncertain Markov process for the unknown system with a simulation relation. It then computes a robust policy on the abstraction with a quantified bound on the error (distance) to the optimal solution. This error is due to both the discretization and regression errors in generating the abstraction. Given the inherent computational complexity, the framework is completely offline and cannot take advantage of runtime data to reduce its error.
