Verification of Switched Stochastic Systems via Barrier Certificates

Autor:	Anand, Mahathi, Jagtap, Pushpak, Zamani, Majid
Rok vydání:	2021
Předmět:	Computer Science - Logic in Computer Science Electrical Engineering and Systems Science - Systems and Control
Zdroj:	IEEE 58th Conference on Decision and Control (CDC), 2019, pp. 4373-4378
Druh dokumentu:	Working Paper
DOI:	10.1109/CDC40024.2019.9028862.
Popis:	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. Comment: arXiv admin note: substantial text overlap with arXiv:1807.00064
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2109.12420 Zobrazit plný text záznamu View this record from Arxiv