Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/2883817.2883836acmconferencesArticle/Chapter ViewAbstractPublication PagescpsweekConference Proceedingsconference-collections
research-article

Safety Verification of Piecewise-Deterministic Markov Processes

Published: 11 April 2016 Publication History

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.

References

[1]
A. D. Ames, J. Grizzle, and P. Tabuada. Control barrier function based quadratic programs with application to adaptive cruise control. In Proceedings of the 53rd IEEE Conference on Decision and Control, pages 6271--6278, 2014.
[2]
L. M. Bujorianu. Stochastic Reachability Analysis of Hybrid Systems. Springer, 2012.
[3]
L. M. Bujorianu and J. Lygeros. Reachability questions in piecewise deterministic Markov processes. In Proceedings of Hybrid Systems: Computation and Control, pages 126--140, 2003.
[4]
CodeMe. CodeMe - software. http://kom.aau.dk/project/CodeMe/software.html, 2015.
[5]
M. H. A. Davis. Markov models and optimization, volume 49 of Monographs on Statistics and Applied Probability. Chapman & Hall, London, 1993.
[6]
H. Guéguen, M.-A. Lefebvre, J. Zaytoon, and O. Nasri. Safety verification and reachability analysis for hybrid systems. Annual Reviews in Control, 33(1):25--36, 2009.
[7]
K. Helmes, S. Röhl, and R. H. Stockbridge. Computing moments of the exit time distribution for Markov processes by linear programming. Operations Research, 49(4):516--530, 2001.
[8]
D. Henrion and M. Korda. Convex computation of the region of attraction of polynomial control systems. IEEE Transactions on Automatic Control, 59(2):297--312, February 2014.
[9]
D. Henrion, J. B. Lasserre, and J. Loefberg. GloptiPoly 3: moments, optimization and semidefinite programming. Optimization Methods and Software, 24(4--5):761--779, 2009.
[10]
A. Klenke. Probability theory : a comprehensive course. Springer, London, 2008.
[11]
M. Korda, D. Henrion, and C. N. Jones. Inner approximations of the region of attraction for polynomial dynamical systems. In Proceedings of the 9th IFAC Symposium on Nonlinear Control Systems, pages 534--539, 2013.
[12]
T. G. Kurtz and R. H. Stockbridge. Existence of Markov controls and characterization of optimal Markov controls. SIAM Journal on Control and Optimization, 36(2):609--653, 1998.
[13]
J. B. Lasserre. Global optimization with polynomials and the problem of moments. SIAM Journal on Optimization, 11(3):796--817, Mar. 2001.
[14]
J. B. Lasserre. Moments, Positive Polynomials and Their Applications, volume 1 of Imperial College Press Optimization Series. Imperial Collage Press, 2010.
[15]
M. Marshall. Positive Polynomials and Sums of Squares, volume 146. American Mathematical Society, 2008.
[16]
I. Mitchell, A. Bayen, and C. Tomlin. A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Transactions on Automatic Control, 50(7):947--957, 2005.
[17]
B. Øksendal. Stochastic Differential Equations: An Introduction with Applications. Springer-Verlag, 5th edition, 2000.
[18]
S. Prajna, A. Jadbabaie, and G. J. Pappas. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic Control, 52(8):1415--1428, August 2007.
[19]
S. Prajna and A. Rantzer. Convex programs for temporal verification of nonlinear dynamical systems. SIAM Journal on Control and Optimization, 46(3):999--1021, 2007.
[20]
M. Putinar. Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. J., 42(3):969--984, 1993.
[21]
T. Rolski, H. Schmidli, V. Schmidt, and J. Teugels. Stochastic processes for insurance and finance. Wiley Series in Probability and Statistics. John Wiley & Sons, Ltd., Chichester, 1999.
[22]
M. Romdlony and B. Jayawardhana. Uniting control Lyapunov and control barrier functions. In Proceedings of the 53rd IEEE Conference on Decision and Control, pages 2293--2298, 2014.
[23]
C. Sloth and R. Wisniewski. Safety analysis of stochastic dynamical systems. In Proceedings of the IFAC Conference on Analysis and Design of Hybrid Systems, pages 62--67, 2015.
[24]
A. Teel. Lyapunov conditions certifying stability and recurrence for a class of stochastic hybrid systems. Annual Reviews In Control, 37(1):1--24, Apr 2013.
[25]
P. Wieland and F. Allgöwer. Constructive safety using control barrier functions. In Proceedings of the 7th IFAC Symposium on Nonlinear Control Systems, pages 462--467, 2007.
[26]
R. Wisniewski, M. Svenstrup, A. S. Pedersen, and C. S. Steiniche. Certificate for safe emergency shutdown of wind turbines. In Proceedings of American Control Conference, pages 3667--3672, 2013.

Cited By

View all
  • (2023)From MDP to POMDP and Back: Safety and Compositionality2023 European Control Conference (ECC)10.23919/ECC57647.2023.10178169(1-6)Online publication date: 13-Jun-2023
  • (2022)Reachability Estimates of Piecewise Deterministic Markov Processes2022 13th Asian Control Conference (ASCC)10.23919/ASCC56756.2022.9828039(2327-2331)Online publication date: 4-May-2022
  • (2020)Safety Verification for Random Ordinary Differential EquationsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2020.301313539:11(4090-4101)Online publication date: Nov-2020
  • Show More Cited By

Index Terms

  1. Safety Verification of Piecewise-Deterministic Markov Processes

    Recommendations

    Comments

    Please enable JavaScript to view thecomments powered by Disqus.

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control
    April 2016
    324 pages
    ISBN:9781450339551
    DOI:10.1145/2883817
    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

    Sponsors

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 11 April 2016

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. hybrid systems
    2. optimisation
    3. piecewise-deterministic markov processes
    4. sum of squares
    5. verification

    Qualifiers

    • Research-article

    Funding Sources

    Conference

    HSCC'16
    Sponsor:

    Acceptance Rates

    HSCC '16 Paper Acceptance Rate 28 of 65 submissions, 43%;
    Overall Acceptance Rate 153 of 373 submissions, 41%

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)7
    • Downloads (Last 6 weeks)0
    Reflects downloads up to 13 Nov 2024

    Other Metrics

    Citations

    Cited By

    View all
    • (2023)From MDP to POMDP and Back: Safety and Compositionality2023 European Control Conference (ECC)10.23919/ECC57647.2023.10178169(1-6)Online publication date: 13-Jun-2023
    • (2022)Reachability Estimates of Piecewise Deterministic Markov Processes2022 13th Asian Control Conference (ASCC)10.23919/ASCC56756.2022.9828039(2327-2331)Online publication date: 4-May-2022
    • (2020)Safety Verification for Random Ordinary Differential EquationsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2020.301313539:11(4090-4101)Online publication date: Nov-2020
    • (2020)Stochastic Safety for Markov ChainsIEEE Control Systems Letters10.1109/LCSYS.2020.3002475(1-1)Online publication date: 2020
    • (2018)Monitoring CTMCs by Multi-clock Timed AutomataComputer Aided Verification10.1007/978-3-319-96145-3_27(507-526)Online publication date: 18-Jul-2018

    View Options

    Get Access

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Media

    Figures

    Other

    Tables

    Share

    Share

    Share this Publication link

    Share on social media