research-article

Scalable Underapproximative Verification of Stochastic LTI Systems using Convexity and Compactness

Authors:

Abraham P. Vinod,

Meeko M. K. OishiAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 1 - 10

https://doi.org/10.1145/3178126.3178148

Published: 11 April 2018 Publication History

Abstract

We present a scalable algorithm to construct a polytopic underapproximation of the terminal hitting time stochastic reach-avoid set, for the verification of high-dimensional stochastic LTI systems with arbitrary stochastic disturbance. We prove the existence of a polytopic underapproximation by characterizing the sufficient conditions under which the stochastic reach-avoid set and the proposed open-loop underapproximation are compact and convex. We construct the polytopic underapproximation by formulating and solving a series of convex optimization problems. These set-theoretic properties also characterize circumstances under which the stochastic reach-avoid problem admits a bang-bang optimal Markov policy. We demonstrate the scalability of our algorithm on a 40D chain of integrators, the highest dimensional example demonstrated to date for stochastic reach-avoid problems, and compare its performance with existing approaches on a spacecraft rendezvous and docking problem.

References

[1]

S. Summers and J. Lygeros. Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Automatica, 46(12):1951--1961, 2010.

Digital Library

[2]

A. P. Vinod, B. HomChaudhuri, and M. M. K. Oishi. Forward stochastic reachability analysis for uncontrolled linear systems using Fourier transforms. In Proc. Hybrid Syst.: Comput. and Ctrl., pages 35--44, 2017.

Digital Library

[3]

B. HomChaudhuri, A. P. Vinod, and M. M. K. Oishi. Computation of forward stochastic reach sets: Application to stochastic, dynamic obstacle avoidance. In Proc. American Ctrl. Conf., Seattle, WA, 2017.

[4]

N. Malone, K. Lesser, M. M. K. Oishi, and L. Tapia. Stochastic reachability based motion planning for multiple moving obstacle avoidance. In Proc. Hybrid Syst.: Comput. and Ctrl., pages 51--60, 2014.

Digital Library

[5]

K. Lesser, M. M. K. Oishi, and R. Erwin. Stochastic reachability for control of spacecraft relative motion. In IEEE Conf. Dec. Ctrl., 2013.

[6]

J. Gleason, A. Vinod, and M. M. K. Oishi. Underapproximation of reach-avoid sets for discrete-time stochastic systems via Lagrangian methods. In IEEE Conf. Dec. Ctrl., 2017.

[7]

A. Abate, M. Prandini, J. Lygeros, and S. Sastry. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica, 44(11):2724--2734, 2008.

Digital Library

[8]

A. Abate, S. Amin, M. Prandini, J. Lygeros, and S. Sastry. Computational approaches to reachability analysis of stochastic hybrid systems. In Proc. Hybrid Syst.: Comput. and Ctrl., pages 4--17, 2007.

Digital Library

[9]

N. Kariotoglou, K. Margellos, and J. Lygeros. On the computational complexity and generalization properties of multi-stage and stage-wise coupled scenario programs. Sys. & Ctr. Lett., 94:63--69, 2016.

[10]

G. Manganini, M. Pirotta, M. Restelli, L. Piroddi, and M. Prandini. Policy search for the optimal control of Markov Decision Processes: A novel particle-based iterative scheme. IEEE Trans. Cybern., 2015.

[11]

D. Drzajic, N. Kariotoglou, M. Kamgarpour, and J. Lygeros. A semidefinite programming approach to control synthesis for stochastic reach-avoid problems. In Int'l Wrk. on App. Verif. for Cts. and Hybrid Syst., pages 134--143, 2016.

[12]

A. P. Vinod and M. M. K. Oishi. Scalable Underapproximation for the Stochastic Reach-Avoid Problem for High-Dimensional LTI Systems Using Fourier Transforms. IEEE Control Syst. Lett., 1(2):316--321, 2017.

[13]

S. Boyd and L. Vandenberghe. Convex optimization. Cambridge Univ. Press, 2004.

Digital Library

[14]

T. Tao. Analysis II. Hindustan Book Agency, 2 edition, 2009.

[15]

R. T. Rockafellar. Convex analysis. Princeton Univ. Press, 1970.

[16]

W. Rudin. Real and complex analysis. Tata McGraw-Hill Ed., 1987.

Digital Library

[17]

J. A. Gubner. Probability and random processes for electrical and computer engineers. Cambridge Univ. Press, 2006.

Digital Library

[18]

Y.S. Chow and H. Teicher. Probability Theory: Independence, Interchangeability, Martingales. Springer New York, 1997.

[19]

D. Bertsekas and S. Shreve. Stochastic optimal control: The discrete time case. Academic Press, 1978.

Digital Library

[20]

A. Genz. QSCMVNV. {Online}. Available: http://www.math.wsu.edu/faculty/genz/software/matlab/qscmvnv.m.

[21]

M. L. Putterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, 2005.

Digital Library

[22]

O. Shakernia, G. J. Pappas, and S. Sastry. Decidable controller synthesis for classes of linear systems. In Proc. Hybrid Syst.: Comput. and Ctrl., pages 407--420, 2000.

Digital Library

[23]

Roger Webster. Convexity. Oxford University Press, 1994.

[24]

A. Genz. Numerical computation of multivariate normal probabilities. J. of Comp. and Graph. Stat., 1(2):141--149, 1992.

[25]

T. G. Kolda, R. M. Lewis, and V. Torczon. Optimization by direct search: New perspectives on some classical and modern methods. SIAM review, 45(3):385--482, 2003.

[26]

B. Schurmann and M. Althoff. Convex Interpolation Control with Formal Guarantees for Disturbed and Constrained Nonlinear Systems. In Proc. Hybrid Syst.: Comput. and Ctrl., pages 121--130, 2017.

Digital Library

[27]

M. Herceg, M. Kvasnica, C.N. Jones, and M. Morari. Multi-Parametric Toolbox 3.0. In Proc. of the European Control Conference, pages 502--510, Zürich, Switzerland, July 17-19 2013. http://control.ee.ethz.ch/~mpt.

[28]

W. Wiesel. Spaceflight Dynamics. McGraw-Hill, New York, 1989.

Cited By

Fatnassi WShoukry Y(2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632970
Lavaei ASoudjani SAbate AZamani M(2022)Automated verification and synthesis of stochastic hybrid systems: A surveyAutomatica10.1016/j.automatica.2022.110617146(110617)Online publication date: Dec-2022
https://doi.org/10.1016/j.automatica.2022.110617
Thorpe ASivaramakrishnan VOishi M(2021)Approximate Stochastic Reachability for High Dimensional Systems2021 American Control Conference (ACC)10.23919/ACC50511.2021.9483404(1287-1293)Online publication date: 25-May-2021
https://doi.org/10.23919/ACC50511.2021.9483404
Show More Cited By

Index Terms

Scalable Underapproximative Verification of Stochastic LTI Systems using Convexity and Compactness
1. Computing methodologies
  1. Artificial intelligence
    1. Control methods
      1. Computational control theory
2. Theory of computation
  1. Design and analysis of algorithms
    1. Mathematical optimization
      1. Continuous optimization
        Convex optimization
        Stochastic control and optimization

Recommendations

Forward Stochastic Reachability Analysis for Uncontrolled Linear Systems using Fourier Transforms
HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control

We propose a scalable method for forward stochastic reachability analysis for uncontrolled linear systems with affine disturbance. Our method uses Fourier transforms to efficiently compute the forward stochastic reach probability measure (density) and ...
Adaptive Control for Semilinear Stochastic Systems

An adaptive, ergodic cost stochastic control problem for a partially known, semilinear, stochastic system in an infinite dimensional space is formulated and solved. The solutions of the Hamilton--Jacobi--Bellman equations for the discounted cost and the ...
Pathwise Optimality in Stochastic Control

We introduce a notion of pathwise optimality for stochastic control problems over an infinite time horizon, and give sufficient conditions for the existence of pathwise optimal controls. We analyze both diffusion processes and processes with discrete ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Copyright © 2018 ACM.

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 ACM 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

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
225
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)2

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Fatnassi WShoukry Y(2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632970
Lavaei ASoudjani SAbate AZamani M(2022)Automated verification and synthesis of stochastic hybrid systems: A surveyAutomatica10.1016/j.automatica.2022.110617146(110617)Online publication date: Dec-2022
https://doi.org/10.1016/j.automatica.2022.110617
Thorpe ASivaramakrishnan VOishi M(2021)Approximate Stochastic Reachability for High Dimensional Systems2021 American Control Conference (ACC)10.23919/ACC50511.2021.9483404(1287-1293)Online publication date: 25-May-2021
https://doi.org/10.23919/ACC50511.2021.9483404
Haesaert SNilsson PSoudjani S(2021)Formal Multi-Objective Synthesis of Continuous-State MDPs2021 American Control Conference (ACC)10.23919/ACC50511.2021.9482873(3428-3433)Online publication date: 25-May-2021
https://doi.org/10.23919/ACC50511.2021.9482873
Haesaert SSoudjani S(2021)Robust Dynamic Programming for Temporal Logic Control of Stochastic SystemsIEEE Transactions on Automatic Control10.1109/TAC.2020.301049066:6(2496-2511)Online publication date: Jun-2021
https://doi.org/10.1109/TAC.2020.3010490
Haesaert SNilsson PSoudjani S(2021)Formal Multi-Objective Synthesis of Continuous-State MDPsIEEE Control Systems Letters10.1109/LCSYS.2020.30442635:5(1765-1770)Online publication date: Nov-2021
https://doi.org/10.1109/LCSYS.2020.3044263
Gleason JVinod AOishi M(2021)Lagrangian approximations for stochastic reachability of a target tubeAutomatica10.1016/j.automatica.2021.109546128(109546)Online publication date: Jun-2021
https://doi.org/10.1016/j.automatica.2021.109546
Vinod AOishi M(2021)Stochastic reachability of a target tube: Theory and computationAutomatica10.1016/j.automatica.2020.109458125(109458)Online publication date: Mar-2021
https://doi.org/10.1016/j.automatica.2020.109458
Majumdar RMallik KSoudjani SAmes ASeshia SDeshmukh J(2020)Symbolic controller synthesis for Büchi specifications on stochastic systemsProceedings of the 23rd International Conference on Hybrid Systems: Computation and Control10.1145/3365365.3382214(1-11)Online publication date: 22-Apr-2020
https://dl.acm.org/doi/10.1145/3365365.3382214
Thorpe AOishi M(2020)Model-Free Stochastic Reachability Using Kernel Distribution EmbeddingsIEEE Control Systems Letters10.1109/LCSYS.2019.29541024:2(512-517)Online publication date: Apr-2020
https://doi.org/10.1109/LCSYS.2019.2954102
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten