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.
