@article{14400,
  abstract     = {We consider the problem of computing the maximal probability of satisfying an 
-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.
The 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 
-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 
-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.
We 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 
-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.},
  author       = {Majumdar, Rupak and Mallik, Kaushik and Schmuck, Anne Kathrin and Soudjani, Sadegh},
  issn         = {1751-570X},
  journal      = {Nonlinear Analysis: Hybrid Systems},
  number       = {2},
  publisher    = {Elsevier},
  title        = {{Symbolic control for stochastic systems via finite parity games}},
  doi          = {10.1016/j.nahs.2023.101430},
  volume       = {51},
  year         = {2024},
}

@article{7426,
  abstract     = {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.},
  author       = {Garcia Soto, Miriam and Prabhakar, Pavithra},
  issn         = {1751-570X},
  journal      = {Nonlinear Analysis: Hybrid Systems},
  number       = {5},
  publisher    = {Elsevier},
  title        = {{Abstraction based verification of stability of polyhedral switched systems}},
  doi          = {10.1016/j.nahs.2020.100856},
  volume       = {36},
  year         = {2020},
}