Data-Driven Safety Verification of POMDPs: Showing Learnability of Safety Certificates via Spectral Learning of Weighted Automata

We develop a data-driven method for finite-horizon safety verification of a partially observable Markov decision process (POMDP) with unknown transition and observation kernels under a fixed finite-state controller. The method uses only observation data and covers two sampling regimes: multiple independent trajectories generated from a common initial distribution, and a single trajectory whose closed-loop latent process is stationary and geometrically mixing. We represent an observation-based safety specification by a deterministic finite automaton (DFA). Exploiting the weighted finite automaton (WFA) realization of the observation-word probability function of the closed-loop POMDP, we estimate empirical Hankel matrices and apply the Ho-Kalman algorithm to obtain a WFA estimate, which is used as a proxy for the unknown POMDP. More precisely, we estimate the probability with which the learned WFA generates words which satisfy the specification. This estimated probability, in turn, can be used to provide a PAC (Probably Approximately Correct) bound on the probability with which the words generated by the unknown POMDP satisfy the specification. This then allows us to provide PAC bounds on safety certificates for the original POMDP, showing that safety certificates of POMDPs are PAC learnable.