Safety verification of piecewise-deterministic markov processes

Rafael Wisniewski, Christoffer Sloth, Manuela Bujorianu, Nir Piterman

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

We consider the safety problem of piecewise-deterministic Markov processes (PDMP). These are systems that have deterministic dynamics and stochastic jumps, where both the time and the destination of the jumps are stochastic. Specifically, we solve a p-safety problem, where we identify the set of initial states from which the probability to reach designated unsafe states is at most 1-p. Based on the knowledge of the full generator of the PDMP, we are able to develop a system of partial differential equations describing the connection between unsafe and initial states. We then show that by using the moment method, we can translate the infinite-dimensional optimisation problem searching for the largest set of p-safe states to a finite dimensional polynomial optimisation problem. We have implemented this technique on top of GloptiPoly and show how to apply it to a numerical example.

Original languageEnglish
Title of host publicationProceedings of the 19th International Conference on Hybrid Systems : Computation and Control
Number of pages10
PublisherAssociation for Computing Machinery
Publication date11. Apr 2016
Pages257-266
ISBN (Electronic)9781450339551
DOIs
Publication statusPublished - 11. Apr 2016
Externally publishedYes
Event19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016 - Vienna, Austria
Duration: 12. Apr 201614. Apr 2016

Conference

Conference19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016
Country/TerritoryAustria
CityVienna
Period12/04/201614/04/2016
SponsorACM Special Interest Group on Embedded Systems (ACM SIGBED)

Keywords

  • Hybrid Systems
  • Optimisation
  • Piecewisedeterministic Markov processes
  • Sum of Squares
  • Verification

Fingerprint

Dive into the research topics of 'Safety verification of piecewise-deterministic markov processes'. Together they form a unique fingerprint.

Cite this