Verification of Switched Stochastic Systems via Barrier Certificates
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.
Keywords
Cite
@article{arxiv.2109.12420,
title = {Verification of Switched Stochastic Systems via Barrier Certificates},
author = {Mahathi Anand and Pushpak Jagtap and Majid Zamani},
journal= {arXiv preprint arXiv:2109.12420},
year = {2021}
}
Comments
arXiv admin note: substantial text overlap with arXiv:1807.00064