---
_id: '14400'
abstract:
- lang: eng
  text: "We consider the problem of computing the maximal probability of satisfying
    an \r\n-regular specification for stochastic, continuous-state, nonlinear systems
    evolving in discrete time. The problem reduces, after automata-theoretic constructions,
    to finding the maximal probability of satisfying a parity condition on a (possibly
    hybrid) state space. While characterizing the exact satisfaction probability is
    open, we show that a lower bound on this probability can be obtained by (I) computing
    an under-approximation of the qualitative winning region, i.e., states from which
    the parity condition can be enforced almost surely, and (II) computing the maximal
    probability of reaching this qualitative winning region.\r\nThe heart of our approach
    is a technique to symbolically compute the under-approximation of the qualitative
    winning region in step (I) via a finite-state abstraction of the original system
    as a \r\n-player parity game. Our abstraction procedure uses only the support
    of the probabilistic evolution; it does not use precise numerical transition probabilities.
    We prove that the winning set in the abstract -player game induces an under-approximation
    of the qualitative winning region in the original synthesis problem, along with
    a policy to solve it. By combining these contributions with (a) a symbolic fixpoint
    algorithm to solve \r\n-player games and (b) existing techniques for reachability
    policy synthesis in stochastic nonlinear systems, we get an abstraction-based
    algorithm for finding a lower bound on the maximal satisfaction probability.\r\nWe
    have implemented the abstraction-based algorithm in Mascot-SDS, where we combined
    the outlined abstraction step with our tool Genie (Majumdar et al., 2023) that
    solves \r\n-player parity games (through a reduction to Rabin games) more efficiently
    than existing algorithms. We evaluated our implementation on the nonlinear model
    of a perturbed bistable switch from the literature. We show empirically that the
    lower bound on the winning region computed by our approach is precise, by comparing
    against an over-approximation of the qualitative winning region. Moreover, our
    implementation outperforms a recently proposed tool for solving this problem by
    a large margin."
acknowledgement: "We thank Daniel Hausmann and Nir Piterman for their valuable comments
  on an earlier version of the manuscript of our other paper [22] where we present,
  among other things, the parity fixpoint for 2 1/2-player games (for a slightly more
  general class of games) with a different and indirect proof of correctness. Based
  on their comments we observed that, unlike the other fixpoints that we present in
  [22], the parity fixpoint does not follow the exact same structure as its counterpart
  for 2-player games, which we also use int his paper.\r\nWe also thank Thejaswini
  Raghavan for observing that our symbolic parity fixpoint algorithm can be solved
  in quasi-polynomial time using recent improved algorithms for solving \r\n-calculus
  expressions. This significantly improved the complexity bounds of our algorithm
  in this paper.\r\nThe work of R. Majumdar and A.-K. Schmuck are partially supported
  by DFG, Germany project 389792660 TRR 248–CPEC. A.-K. Schmuck is additionally funded
  through DFG, Germany project (SCHM 3541/1-1). K. Mallik is supported by the ERC
  project ERC-2020-AdG 101020093. S. Soudjani is supported by the following projects:
  EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047."
article_number: '101430'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Rupak
  full_name: Majumdar, Rupak
  last_name: Majumdar
- first_name: Kaushik
  full_name: Mallik, Kaushik
  id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
  last_name: Mallik
  orcid: 0000-0001-9864-7475
- first_name: Anne Kathrin
  full_name: Schmuck, Anne Kathrin
  last_name: Schmuck
- first_name: Sadegh
  full_name: Soudjani, Sadegh
  last_name: Soudjani
citation:
  ama: 'Majumdar R, Mallik K, Schmuck AK, Soudjani S. Symbolic control for stochastic
    systems via finite parity games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2023;51.
    doi:<a href="https://doi.org/10.1016/j.nahs.2023.101430">10.1016/j.nahs.2023.101430</a>'
  apa: 'Majumdar, R., Mallik, K., Schmuck, A. K., &#38; Soudjani, S. (2023). Symbolic
    control for stochastic systems via finite parity games. <i>Nonlinear Analysis:
    Hybrid Systems</i>. Elsevier. <a href="https://doi.org/10.1016/j.nahs.2023.101430">https://doi.org/10.1016/j.nahs.2023.101430</a>'
  chicago: 'Majumdar, Rupak, Kaushik Mallik, Anne Kathrin Schmuck, and Sadegh Soudjani.
    “Symbolic Control for Stochastic Systems via Finite Parity Games.” <i>Nonlinear
    Analysis: Hybrid Systems</i>. Elsevier, 2023. <a href="https://doi.org/10.1016/j.nahs.2023.101430">https://doi.org/10.1016/j.nahs.2023.101430</a>.'
  ieee: 'R. Majumdar, K. Mallik, A. K. Schmuck, and S. Soudjani, “Symbolic control
    for stochastic systems via finite parity games,” <i>Nonlinear Analysis: Hybrid
    Systems</i>, vol. 51. Elsevier, 2023.'
  ista: 'Majumdar R, Mallik K, Schmuck AK, Soudjani S. 2023. Symbolic control for
    stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems.
    51, 101430.'
  mla: 'Majumdar, Rupak, et al. “Symbolic Control for Stochastic Systems via Finite
    Parity Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 51, 101430, Elsevier,
    2023, doi:<a href="https://doi.org/10.1016/j.nahs.2023.101430">10.1016/j.nahs.2023.101430</a>.'
  short: 'R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid
    Systems 51 (2023).'
date_created: 2023-10-08T22:01:15Z
date_published: 2023-09-27T00:00:00Z
date_updated: 2023-12-13T12:58:56Z
day: '27'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2023.101430
ec_funded: 1
external_id:
  arxiv:
  - '2101.00834'
  isi:
  - '001093188100001'
intvolume: '        51'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1016/j.nahs.2023.101430
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_identifier:
  issn:
  - 1751-570X
publication_status: epub_ahead
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic control for stochastic systems via finite parity games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 51
year: '2023'
...
---
_id: '7426'
abstract:
- lang: eng
  text: This paper presents a novel abstraction technique for analyzing Lyapunov and
    asymptotic stability of polyhedral switched systems. A polyhedral switched system
    is a hybrid system in which the continuous dynamics is specified by polyhedral
    differential inclusions, the invariants and guards are specified by polyhedral
    sets and the switching between the modes do not involve reset of variables. A
    finite state weighted graph abstracting the polyhedral switched system is constructed
    from a finite partition of the state–space, such that the satisfaction of certain
    graph conditions, such as the absence of cycles with product of weights on the
    edges greater than (or equal) to 1, implies the stability of the system. However,
    the graph is in general conservative and hence, the violation of the graph conditions
    does not imply instability. If the analysis fails to establish stability due to
    the conservativeness in the approximation, a counterexample (cycle with product
    of edge weights greater than or equal to 1) indicating a potential reason for
    the failure is returned. Further, a more precise approximation of the switched
    system can be constructed by considering a finer partition of the state–space
    in the construction of the finite weighted graph. We present experimental results
    on analyzing stability of switched systems using the above method.
article_number: '100856'
article_processing_charge: No
article_type: original
author:
- first_name: Miriam
  full_name: Garcia Soto, Miriam
  id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
  last_name: Garcia Soto
  orcid: 0000−0003−2936−5719
- first_name: Pavithra
  full_name: Prabhakar, Pavithra
  last_name: Prabhakar
citation:
  ama: 'Garcia Soto M, Prabhakar P. Abstraction based verification of stability of
    polyhedral switched systems. <i>Nonlinear Analysis: Hybrid Systems</i>. 2020;36(5).
    doi:<a href="https://doi.org/10.1016/j.nahs.2020.100856">10.1016/j.nahs.2020.100856</a>'
  apa: 'Garcia Soto, M., &#38; Prabhakar, P. (2020). Abstraction based verification
    of stability of polyhedral switched systems. <i>Nonlinear Analysis: Hybrid Systems</i>.
    Elsevier. <a href="https://doi.org/10.1016/j.nahs.2020.100856">https://doi.org/10.1016/j.nahs.2020.100856</a>'
  chicago: 'Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification
    of Stability of Polyhedral Switched Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>.
    Elsevier, 2020. <a href="https://doi.org/10.1016/j.nahs.2020.100856">https://doi.org/10.1016/j.nahs.2020.100856</a>.'
  ieee: 'M. Garcia Soto and P. Prabhakar, “Abstraction based verification of stability
    of polyhedral switched systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol.
    36, no. 5. Elsevier, 2020.'
  ista: 'Garcia Soto M, Prabhakar P. 2020. Abstraction based verification of stability
    of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 36(5), 100856.'
  mla: 'Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification
    of Stability of Polyhedral Switched Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>,
    vol. 36, no. 5, 100856, Elsevier, 2020, doi:<a href="https://doi.org/10.1016/j.nahs.2020.100856">10.1016/j.nahs.2020.100856</a>.'
  short: 'M. Garcia Soto, P. Prabhakar, Nonlinear Analysis: Hybrid Systems 36 (2020).'
date_created: 2020-02-02T23:00:59Z
date_published: 2020-05-01T00:00:00Z
date_updated: 2023-08-17T14:32:54Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2020.100856
external_id:
  isi:
  - '000528828600003'
file:
- access_level: open_access
  checksum: 560abfddb53f9fe921b6744f59f2cfaa
  content_type: application/pdf
  creator: dernst
  date_created: 2020-10-21T13:16:45Z
  date_updated: 2022-05-16T22:30:04Z
  embargo: 2022-05-15
  file_id: '8688'
  file_name: 2020_NAHS_GarciaSoto.pdf
  file_size: 818774
  relation: main_file
file_date_updated: 2022-05-16T22:30:04Z
has_accepted_license: '1'
intvolume: '        36'
isi: 1
issue: '5'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_identifier:
  issn:
  - 1751-570X
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstraction based verification of stability of polyhedral switched systems
tmp:
  image: /images/cc_by_nc_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
    (CC BY-NC-ND 4.0)
  short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 36
year: '2020'
...