---
_id: '14559'
abstract:
- lang: eng
  text: We consider the problem of learning control policies in discrete-time stochastic
    systems which guarantee that the system stabilizes within some specified stabilization
    region with probability 1. Our approach is based on the novel notion of stabilizing
    ranking supermartingales (sRSMs) that we introduce in this work. Our sRSMs overcome
    the limitation of methods proposed in previous works whose applicability is restricted
    to systems in which the stabilizing region cannot be left once entered under any
    control policy. We present a learning procedure that learns a control policy together
    with an sRSM that formally certifies probability 1 stability, both learned as
    neural networks. We show that this procedure can also be adapted to formally verifying
    that, under a given Lipschitz continuous control policy, the stochastic system
    stabilizes within some stabilizing region with probability 1. Our experimental
    evaluation shows that our learning procedure can successfully learn provably stabilizing
    policies in practice.
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093, ERC
  CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation
  programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Matin
  full_name: Ansaripour, Matin
  last_name: Ansaripour
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Mathias
  full_name: Lechner, Mathias
  id: 3DC22916-F248-11E8-B48F-1D18A9856A87
  last_name: Lechner
- first_name: Dorde
  full_name: Zikelic, Dorde
  id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
  last_name: Zikelic
  orcid: 0000-0002-4681-1699
citation:
  ama: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. Learning provably
    stabilizing neural controllers for discrete-time stochastic systems. In: <i>21st
    International Symposium on Automated Technology for Verification and Analysis</i>.
    Vol 14215. Springer Nature; 2023:357-379. doi:<a href="https://doi.org/10.1007/978-3-031-45329-8_17">10.1007/978-3-031-45329-8_17</a>'
  apa: 'Ansaripour, M., Chatterjee, K., Henzinger, T. A., Lechner, M., &#38; Zikelic,
    D. (2023). Learning provably stabilizing neural controllers for discrete-time
    stochastic systems. In <i>21st International Symposium on Automated Technology
    for Verification and Analysis</i> (Vol. 14215, pp. 357–379). Singapore, Singapore:
    Springer Nature. <a href="https://doi.org/10.1007/978-3-031-45329-8_17">https://doi.org/10.1007/978-3-031-45329-8_17</a>'
  chicago: Ansaripour, Matin, Krishnendu Chatterjee, Thomas A Henzinger, Mathias Lechner,
    and Dorde Zikelic. “Learning Provably Stabilizing Neural Controllers for Discrete-Time
    Stochastic Systems.” In <i>21st International Symposium on Automated Technology
    for Verification and Analysis</i>, 14215:357–79. Springer Nature, 2023. <a href="https://doi.org/10.1007/978-3-031-45329-8_17">https://doi.org/10.1007/978-3-031-45329-8_17</a>.
  ieee: M. Ansaripour, K. Chatterjee, T. A. Henzinger, M. Lechner, and D. Zikelic,
    “Learning provably stabilizing neural controllers for discrete-time stochastic
    systems,” in <i>21st International Symposium on Automated Technology for Verification
    and Analysis</i>, Singapore, Singapore, 2023, vol. 14215, pp. 357–379.
  ista: 'Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning
    provably stabilizing neural controllers for discrete-time stochastic systems.
    21st International Symposium on Automated Technology for Verification and Analysis.
    ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379.'
  mla: Ansaripour, Matin, et al. “Learning Provably Stabilizing Neural Controllers
    for Discrete-Time Stochastic Systems.” <i>21st International Symposium on Automated
    Technology for Verification and Analysis</i>, vol. 14215, Springer Nature, 2023,
    pp. 357–79, doi:<a href="https://doi.org/10.1007/978-3-031-45329-8_17">10.1007/978-3-031-45329-8_17</a>.
  short: M. Ansaripour, K. Chatterjee, T.A. Henzinger, M. Lechner, D. Zikelic, in:,
    21st International Symposium on Automated Technology for Verification and Analysis,
    Springer Nature, 2023, pp. 357–379.
conference:
  end_date: 2023-10-27
  location: Singapore, Singapore
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2023-10-24
date_created: 2023-11-19T23:00:56Z
date_published: 2023-10-22T00:00:00Z
date_updated: 2025-07-14T09:09:59Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-031-45329-8_17
ec_funded: 1
intvolume: '     14215'
language:
- iso: eng
month: '10'
oa_version: None
page: 357-379
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '665385'
  name: International IST Doctoral Program
publication: 21st International Symposium on Automated Technology for Verification
  and Analysis
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031453281'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Learning provably stabilizing neural controllers for discrete-time stochastic
  systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14215
year: '2023'
...