ProbStar Temporal Logic for Verifying Complex Behaviors of Learning-enabled Systems

This paper introduces a novel quantitative verification framework for analyzing the temporal behaviors of learning-enabled systems (LES). Our approach employs ProbStar Temporal Logic (ProbStarTL) to specify LES temporal behaviors alongside advanced reachability and verification algorithms. Unlike existing qualitative methods focusing primarily on reach-avoid properties, our framework enables quantitative analysis of temporal properties. ProbStarTL, distinct from Signal Temporal Logic, operates on sequences of timed probabilistic star reachable sets, known as ProbStar signals. It features a clear syntax and dual qualitative and quantitative semantics. Our framework includes depth-first search algorithms for generating ProbStar traces and novel verification algorithms that transform ProbStarTL specifications into a computable disjunctive normal form for analysis. Our verification algorithms allow for both exact and approximate analyses. The exact scheme guarantees sound and complete results with precise satisfaction probabilities, while the approximate scheme offers sound results with maximum and minimum satisfaction probabilities at a reduced computational cost. The new verification framework is implemented using StarV, and its effectiveness is demonstrated through case studies on a learning-based adaptive cruise control system and an advanced emergency braking system.