VERIFICATION OF STOCHASTIC SYSTEMS USING BARRIER CERTIFICATES

Abstract

Design and implementation of control systems in safety critical applications regularly involves formal verification to ensure specification satisfaction and correctness of implementation. The M.Tech dissertation work presents a methodology for temporal logic verification of stochastic systems using a discretizationfree approach that combines automata-based verification and barrier certificates. The main objective is to provide a lower bound on the probability that a given temporal logic specification is satisfied over a finite time horizon. This work considers a subclass of temporal logic specifications called safe-LTL properties over finite traces. The method essentially utilizes the automaton representation of the negation of specification for decomposing the specification to a sequence of simpler reachability problems and compute upper bounds for the reachability probabilities using barrier certificates. The work proposes novel theoretical results for barrier certificate based verification of safety properties for switched stochastic systems in continuous-time, which is then implemented using SMT solvers and Counter Example Guided Inductive Synthesis (CEGIS) framework. In addition, this work also handles the implementation of safety verification for discrete-time stochastic systems using a similar technique. The approach is examined through simple illustrative examples and results are provided.