Verification of Switched Stochastic Systems via Barrier Certificates

TL;DR

This paper introduces a method for verifying complex temporal properties of continuous-time switched stochastic systems by combining automata-based techniques with barrier certificates to compute probability bounds.

Contribution

It proposes a novel approach that decomposes automata for negated specifications into reachability tasks and uses barrier certificates to bound probabilities, enhancing verification of stochastic systems.

Findings

Successfully computes lower bounds on satisfaction probabilities.

Demonstrates effectiveness on counter-example guided synthesis.

Integrates automata and barrier certificates for verification.

Abstract

The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a complex temporal property is satisfied over a finite time horizon. The required temporal properties of the system are expressed using a fragment of linear temporal logic, called safe-LTL with respect to finite traces. Our approach combines automata-based verification and the use of barrier certificates. It relies on decomposing the automaton associated with the negation of specification into a sequence of simpler reachability tasks and compute upper bounds for these reachability probabilities by means of common or multiple barrier certificates. Theoretical results are illustrated by applying a counter-example guided inductive synthesis framework to find barrier certificates.