Publication Details

Reachability Computation for Switching Diffusions:Finite Abstractions with Certifiable and Tuneable Precision

LAURENTI Luca, ABATE Alessandro, BORTOLUSSI Luca, CARDELLI Luca, ČEŠKA Milan and KWIATKOWSKA Marta. Reachability Computation for Switching Diffusions:Finite Abstractions with Certifiable and Tuneable Precision. In: Proceedings of the 20th ACM International Conference on Hybrid Systems: Computation and Control. ACM. New York: Association for Computing Machinery, 2017, pp. 55-64. ISBN 978-1-4503-4590-3.
Czech title
Vypočet Dosažitelnosti v Hybridnich Systémech:Konečná Abstrakce s Garantovanou Chybou
Type
conference paper
Language
english
Authors
Laurenti Luca (UOx)
Abate Alessandro (UOx)
Bortolussi Luca (UNITS)
Cardelli Luca (MSR)
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT)
Kwiatkowska Marta (UOx)
Keywords

Switching diffusions; stochastic hybrid models; reachability and safety analysis; finite abstractions; time and space dis- cretisation; numerical computations 

Abstract

We consider continuous time stochastic hybrid systems with no resets and continuous dynamics described by linear stochastic differential equations -- models also known as switching diffusions. We show that for this class of models reachability (and dually, safety) properties can be studied on an abstraction defined in terms of a discrete time and finite space Markov chain (DTMC), with provable error bounds. The technical contribution of the paper is a characterization of the uniform convergence of the time discretization of such stochastic processes with respect to safety properties. This allows us to newly provide a complete and sound numerical procedure for reachability and safety computation over switching diffusions.

Published
2017
Pages
55-64
Proceedings
Proceedings of the 20th ACM International Conference on Hybrid Systems: Computation and Control
Series
ACM
Conference
ACM International Conference on Hybrid Systems: Computation and Control, Pittsburgh, US
ISBN
978-1-4503-4590-3
Publisher
Association for Computing Machinery
Place
New York, US
DOI
10.1145/3049797.3049812
UT WoS
000615962400007
EID Scopus
2-s2.0-85019051467
BibTeX 
@INPROCEEDINGS{FITPUB11368,
   author = "Luca Laurenti and Alessandro Abate and Luca Bortolussi and Luca Cardelli and Milan \v{C}e\v{s}ka and Marta Kwiatkowska",
   title = "Reachability Computation for Switching Diffusions:Finite Abstractions with Certifiable and Tuneable Precision",
   pages = "55--64",
   booktitle = "Proceedings of the 20th ACM International Conference on Hybrid Systems: Computation and Control",
   series = "ACM",
   year = 2017,
   location = "New York, US",
   publisher = "Association for Computing Machinery",
   ISBN = "978-1-4503-4590-3",
   doi = "10.1145/3049797.3049812",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11368"
}
Back to top