# Verification of Switched Stochastic Systems via Barrier Certificates

arXiv: https://arxiv.org/abs/2109.12420 · HTML: https://mlsanity.com/paper/2109.12420/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Sep 2021.

## Built on by (most cited first, 1 of 1)

- [Myopically Verifiable Probabilistic Certificates for Safe Control and Learning](https://mlsanity.com/paper/2404.16883/) (2024)

## Abstract (arXiv)

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.