[{"oa_version":"Published Version","citation":{"short":"R. Majumdar, K. Mallik, A.K. Schmuck, S. Soudjani, Nonlinear Analysis: Hybrid Systems 51 (2023).","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>","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.","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>","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.","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>.","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>."},"day":"27","month":"09","volume":51,"article_processing_charge":"No","arxiv":1,"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."}],"doi":"10.1016/j.nahs.2023.101430","title":"Symbolic control for stochastic systems via finite parity games","author":[{"first_name":"Rupak","last_name":"Majumdar","full_name":"Majumdar, Rupak"},{"orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","first_name":"Kaushik","full_name":"Mallik, Kaushik","last_name":"Mallik"},{"last_name":"Schmuck","full_name":"Schmuck, Anne Kathrin","first_name":"Anne Kathrin"},{"last_name":"Soudjani","full_name":"Soudjani, Sadegh","first_name":"Sadegh"}],"_id":"14400","status":"public","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.","publication_status":"epub_ahead","ec_funded":1,"publication_identifier":{"issn":["1751-570X"]},"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"date_published":"2023-09-27T00:00:00Z","external_id":{"isi":["001093188100001"],"arxiv":["2101.00834"]},"date_created":"2023-10-08T22:01:15Z","scopus_import":"1","department":[{"_id":"ToHe"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","isi":1,"language":[{"iso":"eng"}],"type":"journal_article","quality_controlled":"1","publisher":"Elsevier","main_file_link":[{"url":"https://doi.org/10.1016/j.nahs.2023.101430","open_access":"1"}],"intvolume":"        51","year":"2023","oa":1,"article_number":"101430","article_type":"original","publication":"Nonlinear Analysis: Hybrid Systems","date_updated":"2023-12-13T12:58:56Z"},{"type":"journal_article","quality_controlled":"1","language":[{"iso":"eng"}],"isi":1,"publisher":"Elsevier","intvolume":"        36","date_created":"2020-02-02T23:00:59Z","scopus_import":"1","external_id":{"isi":["000528828600003"]},"date_published":"2020-05-01T00:00:00Z","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","department":[{"_id":"ToHe"}],"article_number":"100856","article_type":"original","date_updated":"2023-08-17T14:32:54Z","publication":"Nonlinear Analysis: Hybrid Systems","year":"2020","oa":1,"volume":36,"article_processing_charge":"No","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode"},"file":[{"file_id":"8688","date_created":"2020-10-21T13:16:45Z","file_name":"2020_NAHS_GarciaSoto.pdf","relation":"main_file","creator":"dernst","file_size":818774,"embargo":"2022-05-15","access_level":"open_access","content_type":"application/pdf","checksum":"560abfddb53f9fe921b6744f59f2cfaa","date_updated":"2022-05-16T22:30:04Z"}],"oa_version":"Submitted Version","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","month":"05","file_date_updated":"2022-05-16T22:30:04Z","ddc":["000"],"citation":{"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>.","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>.","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>","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.","short":"M. Garcia Soto, P. Prabhakar, Nonlinear Analysis: Hybrid Systems 36 (2020).","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>"},"day":"01","status":"public","publication_status":"published","project":[{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"publication_identifier":{"issn":["1751-570X"]},"doi":"10.1016/j.nahs.2020.100856","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."}],"issue":"5","_id":"7426","title":"Abstraction based verification of stability of polyhedral switched systems","author":[{"orcid":"0000−0003−2936−5719","full_name":"Garcia Soto, Miriam","last_name":"Garcia Soto","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","first_name":"Miriam"},{"first_name":"Pavithra","full_name":"Prabhakar, Pavithra","last_name":"Prabhakar"}]}]