Paper deep dive
Resilient Strategies for Stochastic Systems: How Much Does It Take to Break a Winning Strategy?
Kush Grover, Markel Zubia, Debraj Chakraborty, Muqsit Azeem, Nils Jansen, Jan Kretinsky
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 7/20/2026, 6:38:20 AM
Summary
This paper introduces the concept of resilience for strategies in stochastic systems, specifically Markov Decision Processes (MDPs) and Stochastic Games (SGs). It defines the 'breaking point' as the minimum number of disturbances required to violate a safety or reachability objective. The authors propose algorithms to compute resilience under expected and worst-case semantics, handling both finite and infinite disturbance scenarios by analyzing disturbance frequency. The work extends previous non-stochastic resilience concepts to stochastic settings, providing a framework for evaluating and synthesizing robust strategies.
Entities (10)
Relation Signals (7)
Resilient Strategies โ appliesto โ Markov Decision Processes
confidence 95% ยท Specifically, we discuss such problems for Markov decision processes with reachability and safety objectives
Resilient Strategies โ appliesto โ Stochastic Games
confidence 95% ยท which also smoothly extend to stochastic games.
Breaking Point โ measures โ Resilient Strategies
confidence 92% ยท The resilience of a strategy is measured by calculating its breaking point
Disturbances โ affects โ Resilient Strategies
confidence 90% ยท Resilient strategies enable an agent to make decisions that are robust against disturbances.
Expected Semantics โ aggregates โ Disturbances
confidence 88% ยท we provide various ways of aggregating the amounts of disturbances that may have occurred, for instance, in expectation
Worst-case Semantics โ aggregates โ Disturbances
confidence 88% ยท or in the worst case.
Frequency of Disturbances โ usedfor โ Infinite Disturbances
confidence 85% ยท to reason about infinite disturbances, we use quantitative measures, like their frequency of occurrence.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We study the problem of resilient strategies in the presence of uncertainty. Resilient strategies enable an agent to make decisions that are robust against disturbances. In particular, we are interested in those disturbances that are able to flip a decision made by the agent. Such a disturbance may, for instance, occur when the intended action of the agent cannot be executed due to a malfunction of an actuator in the environment. In this work, we introduce the concept of resilience in the stochastic setting and present a comprehensive set of fundamental problems. Specifically, we discuss such problems for Markov decision processes with reachability and safety objectives, which also smoothly extend to stochastic games. To account for the stochastic setting, we provide various ways of aggregating the amounts of disturbances that may have occurred, for instance, in expectation or in the worst case. Moreover, to reason about infinite disturbances, we use quantitative measures, like their frequency of occurrence.
Tags
Links
- Source: https://arxiv.org/abs/2602.24191v1
- Canonical: https://arxiv.org/abs/2602.24191v1
Trouble viewing inline? Open PDF directly โ
Full Text
102,435 characters extracted from source content.
Expand or collapse full text
Resilient Strategies for Stochastic Systems: How Much Does It Take to Break a Winning Strategy? AAAI Track Kush Grover Fondazione Bruno Kessler Italy Markel Zubia Ruhr University Bochum Germany Debraj Chakraborty Nanyang Technological University, Singapore Muqsit Azeem Technical University of Munich & University of Konstanz Germany Nils Jansen Ruhr University Bochum & Radboud University Nijmegen Germany Jan Kลetinskรฝ Masaryk University Czech Republic ABSTRACT We study the problem of resilient strategies in the presence of un- certainty. Resilient strategies enable an agent to make decisions that are robust against disturbances. In particular, we are interested in those disturbances that are able to flip a decision made by the agent. Such a disturbance may, for instance, occur when the in- tended action of the agent cannot be executed due to a malfunction of an actuator in the environment. In this work, we introduce the concept of resilience in the stochastic setting and present a com- prehensive set of fundamental problems. Specifically, we discuss such problems for Markov decision processes with reachability and safety objectives, which also smoothly extend to stochastic games. To account for the stochastic setting, we provide various ways of aggregating the amounts of disturbances that may have occurred, for instance, in expectation or in the worst case. Moreover, to rea- son about infinite disturbances, we use quantitative measures, like their frequency of occurrence. KEYWORDS Markov Decision Processes; Stochastic Games; Verification ACM Reference Format: Kush Grover, Markel Zubia, Debraj Chakraborty, Muqsit Azeem, Nils Jansen, and Jan Kลetinskรฝ. 2026. Resilient Strategies for Stochastic Systems: How Much Does It Take to Break a Winning Strategy?: AAAI Track. In Proc. of the 25th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2026), Paphos, Cyprus, May 25 โ 29, 2026, IFAAMAS, 21 pages. https://doi.org/10.65109/JAGQ1479 1 INTRODUCTION AND MOTIVATION In many areas such as machine learning, robotics, automated plan- ning, and game theory, a notion of optimality is adopted to argue about the best possible behavior in a given environment. While optimality captures the best possible performance an agent may achieve in a fixed, well-defined environment, real-world settings are This work is licensed under a Creative Commons Attribution Inter- national 4.0 License. Proc. of the 25th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2026), C. Amato, L. Dennis, V. Mascardi, J. Thangarajah (eds.), May 25 โ 29, 2026, Paphos, Cyprus.ยฉ 2026 International Foundation for Autonomous Agents and Multiagent Systems (w.ifaamas.org). https://doi.org/10.65109/JAGQ1479 rarely stable or predictable. Then, resilience becomes a more mean- ingful objective: it reflects the agentโs ability to maintain desirable behavior despite changes or adversarial disturbances. The latter includes notions such as fault tolerance of algorithms, robustness to disturbances in control, or trembling hands equilibria in game theory. As Vardi[29]argues, this notion is spread not only over computer science, but also economics, evolution, or other dynamic systems; and while considerable effort has been spent in the area, still โWe must recognize the trade-off between efficiency and resilience. It is time to develop the discipline of resilient algorithms.โ Resilient Strategies. This paper focuses on resilience of strategies (a.k.a. policies, schedulers, or controllers, depending on the context) in terms of the number of decisions that need to be subverted, which we refer to as disturbances, to violate the property otherwise satisfied by the original strategy. From the control perspective, such disturbances may represent actuator faults, control noise, or environmental perturbations that prevent the agent from executing its intended action. For instance, consider an autonomous drone navigating a grid world toward a target (Figure 1): the strategy corresponding to the red path would reach the target in the ideal situation. However, it passes close to the trees, making it vulnerable to collisions from disturbances (due to wind). A resilient strategy, in contrast, would follow the green path which maintains a buffer from the trees. This leads to the target with probability 1, but it can also handle a disturbance. Understanding how sensitive a strategy is to such disturbances is essential for deploying agents in uncertain or adversarial environments. Figure 1: Drone navigation task with wind disturbances. From a theoretical perspective, analyzing resilience reveals which regions of the state space are critical to maintaining correct behav- ior. That is, it helps identify the brittle points of the agentโs strategy where a few disturbances can lead to failure. This information is arXiv:2602.24191v1 [cs.GT] 27 Feb 2026 relevant in the context of explaining its key decisions [3], in the context of strategy repair [23], and in the modern on-the-fly au- tomated synthesis approaches [15]. Notably, standard modeling approaches such as incorporating noise probabilistically or assum- ing a fully adversarial environment fall short of capturing this nuance. Probabilistic models mask the fragility of decisions by aver- aging over expected behaviors, while adversarial models are overly pessimistic and can rule out efficient paths unnecessarily. In con- trast, our disturbance-based view offers a finer robustness metric by asking how many deviations are needed to cause failure. Resilience in Stochastic Systems. Previous work has investigated the resilience of strategies in (non-quantitative) graph games [21]. While the landscape is rather bland there, it becomes very vibrant in the stochastic context. Indeed, in the former setting, (i) quan- tifying resilience by the number of disturbances (decisions to be subverted) during a play is a straightforward choice, (i) it results in an integer bounded by the size of the state space or infinity, (i) al- gorithmically, it boils down to iterative, graph-search-based proce- dures that identify regions from which an agent can enforce reach- ing a goal regardless of disturbances. In stark contrast, for Markov decision processes and stochastic games, (i) resilience purely in terms of expected disturbance counts may not be adequate, and we also analyze worst cases happening with positive probability; (i) the number of disturbances may now be larger than the state space size and is, in fact, unbounded; in such cases, we refine the resilience measure by considering the frequency of disturbances rather than their total count; (i) algorithmically, only some cases can be easily reduced to simple graph search or mean-payoff computations. Assumptions on Model Availability. Our work relies on the stan- dard assumption in the model-based planning paradigm that the underlying model is available in explicit form or can be obtained through established learning methods. This convention is well doc- umented in the model-checking literature; see, for example [5], where verification algorithms are defined relative to a given system model. When the model is not provided a priori but is learnable from data, statistical model checking offers a widely used path- way for reconstructing or approximating the relevant stochastic behavior [1,4]. Once such an approximation is obtained, the result- ing model fits within the standard verification framework and our method applies directly. Disturbances with Different Costs. In this work, we focus on sym- metric disturbances, i.e. all disturbances have the same cost, for two reasons: (i) Prior work on resilience in non-stochastic settings [11,21] has considered only symmetric disturbances, and we aim to extend that line of work to stochastic settings. (i) From the practical perspective, assigning precise costs to disturbances is of- ten challenging, as it requires detailed domain knowledge. On the other hand, symmetric disturbances appropriately model several realistic scenarios, for example network routing problems [13,24]. Furthermore, our framework can naturally extend to asymmetric disturbance costs by assigning different weights to disturbance transitions. This would change the resilience metric from โhow many disturbancesโ to โtotal disturbance costโ. This would require adapting some algorithms presented here, while the rest would remain unchanged, and we leave this for future work. Summary of Our Contribution: โขWe extend the notion of strategy resilience to the stochas- tic setting with safety and reachability objectives. To that end, we consider expected and positive-measure worst cases. When infinitely many disturbances are required to break a strategy, we refine the notion by computing their frequency. โขWe provide algorithms for computing the resilience of a given strategy (for each definition of resilience introduced) and to compute optimally resilient strategies. From the per- spective of the efficiency-resilience trade-off, these are sat- isfying strategies (satisfy the functional property with at least a given probability threshold) with optimal resilience (requiring the most disturbances to break them, i.e., decrease the probability below the threshold). The resilience of a strategy is measured by calculating its break- ing point, defined as the maximum number of disturbances that are necessary to break it. Table 1 provides an overview of the algorithms to compute the breaking point of a pure memoryless strategy in the worst and expected cases, and for finding a strategy with the maximum breaking point. Definitions of terms used in the tables are provided in Section 2. Related Work. The concept of system robustness against errors has been extensively studied in various contexts. One common approach is to model uncertainties in estimated probabilities using an uncertainty set within which the true probability resides. To ensure absolute safety, a worst-case analysis is often employed, yielding results that are resilient to such disturbances [7]. Another approach is to perform a sensitivity analysis over the uncertainty sets to measure how resilient the system is with respect to different variables [31]. For a comprehensive comparison of different notions of resilience and robustness, we refer the reader to [11, 21]. Apart from uncertainty sets, notions of differential privacy and deception for MDPs have also been explored, which utilize and optimize for different measures of detection and resilience [6,12,18]. Another way to model disturbances is by treating them as random events with small probabilities, often called trembling hand [19,30]. However, this might not always be suitable, and defining an accurate stochastic error model may be challenging, also argued in [21]. Therefore, the idea of strategies that are resilient to unmodeled intermittent disturbances was first introduced in [11] within the context of safety games. This concept was later extended to prefix- independent winning conditions, including parity objectives, in [21]. It was demonstrated that computing optimally resilient strategies for parity conditions incurs only a polynomial overhead compared to solving traditional parity games. These ideas were further applied in [26] to find resilient controllers for a continuous dynamical system. Additionally, the notion of resilient strategies was extended to infinite arenas, particularly pushdown graphs, in [20]. However, none of these works consider the potential benefits of leveraging partial knowledge of stochasticity within the model. To our knowledge, this work is the first to study unmodeled inter- mittent disturbances in the context of stochastic systems such as Markov decision processes and stochastic games. Moreover, prior works do not investigate resilience in terms of the frequency of disturbances required to compromise a strategy, particularly in sce- narios where infinite disturbances can be handled by the controller. Table 1: Overview of strategy evaluation and optimal strategy computation under different semantics and breaking point types. Semantics Breaking Point Type Strategy EvaluationStrategy Synthesis SafetyReachabilitySafetyReachability Expected TransientSSP for MDP (P)SSP for MDP (P)SSP for SGSSP for SG FrequencyCannot happenCollapse MECs+ SSP for MDP (P)Cannot happenCollapse MECs+ SSP for SG Worst-case TransientIterative LP (PSPACE)Iterative LP (PSPACE)Iterative QP (PSPACE)Iterative QP (PSPACE) FrequencyAlways 0Collapse MECs+ Worst-case analysis (P)Always 0Collapse MECs+ Worst-case analysis (NP) 2 PRELIMINARIES For a setํด, we denote its power set byPow(ํด). We use Von Neu- mann ordinals, withโจํโฉ=0, . . .,ํโ1for allํ โ N. The set of all (discrete) probability distributions on the setํis denoted by Dist(ํ). We denote by ํ โ the set of all finite strings over ํ . 2.1 Stochastic Games Definition 1. A (2-player) Stochastic Game (SG) is a tuple G= (ํ,ํ 1 ,ํ 2 ,ํด,ํดํฃ,ํ)whereํis a finite set of states partitioned into Player 1 statesํ 1 and Player 2 statesํ 2 ;ํดis a finite set of actions; ํดํฃ:ํ โ Pow(ํด)is a total function which maps the set of available actions to each state, andํ:ํร ํดโ Dist(ํ)is a partial transition function, which, given a state and an available action, returns a probability distribution over the successor states. We also define an initial state,ํ 0 โ ํfrom which the play starts. With a slight abuse of notation, we useํ(ํ ,ํ,ํ โฒ )to denoteํ(ํ ,ํ)(ํ โฒ ). For this paper, we assume that the stochastic game is turn-based, i.e., in each state, only one player can move. Paths or Runs. The set of successor states forํ โ ํthat can be reached by taking the actionํisPost G (ํ ,ํ)=ํ โฒ | ํ(ํ ,ํ,ํ โฒ )>0. A finite path (or finite run)ํ= ํ 0 ํ 0 ํ 1 . . .ํ ํ of lengthํ โฅ0 is a sequence of states and actions such that for allํก โ [0,ํโ1],ํ ํก โ ํดํฃ(ํ ํก ) andํ ํก+1 โ Post G (ํ ํก ,ํ ํก ). We can define infinite paths (or infinite runs) ํ= ํ 0 ํ 0 ํ 1 ํ 1 ํ 2 . . . analogously. Strategies. A Player 1 strategy is defined as a functionํ:(ํร ํด) โ ร ํ 1 โ Dist(ํด) mapping the history to a distribution over available actions. A strategy is pure if the distribution is always a Dirac delta function, and it is mixed otherwise. Player 2 strategies have analogous definitions. Markov Decision Processes (MDP) and Markov Chains (MC). MDPs are a special case of stochastic games where the states of one player are empty i.e.ํ 2 =โ . If the strategy of Player 1,ํ, is fixed in the SG G, it induces an MDPG ํ . An MC is an MDP with|ํดํฃ(ํ )|=1 for all ํ โ ํ. Fixing a strategyํon an MDPG ํ induces a Markov chain G ํ,ํ . An MCํand an initial stateํ 0 define a unique probability measureP ํ,ํ 0 over infinite paths [25]. For any random variableํ defined over the infinite paths of MCํ, its expected value with respect to P ํ,ํ 0 is E ํ,ํ 0 [ํ]. End Component (EC). A set of states and actions is an end com- ponent if the play never leaves that set and it is a maximal end component (MEC) if it cannot be extended by adding more states and actions. The states in an MDP can be partitioned into MECs, and every play is guaranteed to eventually enter a MEC. We refer to standard literature [25] for the formal definitions. We useMEC(ํ) to denote the set of maximal end components ofํ. This notion of MECs can be extended to SGs. Rewards or Costs. We model the costs associated with each state- action pair using a functionํถ:ํ ร ํด โ N. Given a Markov chain (MC)ํ, letํถ ํ be a random variable that, for an infinite path ํ= ํ 0 ํ 0 ํ 1 ํ 1 . . . , returnsํถ ํ (ํ)=ํถ(ํ ํ ,ํ ํ ); i.e., the cost (or reward) incurred at theํ-th step of the path. The total cost for an infinite path ํis defined asํถ ํ := ร โ ํ=0 ํถ(ํ ํ ,ํ ํ ). The expected total cost forํ starting from stateํ 0 is defined asTR(ํ,ํ 0 ,ํถ):= ร โ ํ=0 E ํ,ํ 0 (ํถ ํ )= E ํ,ํ 0 (ํถ ํ ) . Theํ-step average cost from stateํ 0 inํis defined as ํฃ ํ (ํ 0 ):= E ํ,ํ 0 1 ํ+1 ร ํ ํ=0 ํถ ํ . The expected mean payoff forํfrom stateํ 0 is defined asMP(ํ,ํ 0 ,ํถ):= lim inf ํโโ ํฃ ํ (ํ 0 ). The mean payoff for a pathํis defined asMP(ํ):= lim inf ํโโ 1 ํ+1 ร ํ ํ=0 ํถ(ํ ํ ,ํ ํ ). Specifications. We use the standard temporal operatorsโก(glob- ally) andโฆ(eventually). In an MCํwith initial stateํ 0 , we let P G,ํ 0 (โกยฌํต)denote the probability of never visitingํต โ ํ, and P G,ํ 0 (โฆํบ)denote the probability of eventually reachingํบ โ ํ. We focus on two standard quantitative specifications and their nega- tions: safety, whereํ ํ ํํํํกํฆ := P G,ํ 0 (โกยฌํต)> ํ; and reachability, where ํ ํํํํโ := P G,ํ 0 (โฆํบ)> ํ. The propertiesํ ํ ํํํํกํฆ andํ ํํํํโ could equivalently be stated withโฅ; the analysis carries over with only minor adaptations. Under expected semantics, the same computation yields resilience rather than the breaking point, while the worst-case semantics remains unchanged. W.l.o.g., we assume that all states inํบorํตare sink states with only a self loop. Algorithms to Solve MDPs and SGs. For solving reachability and safety problems in MDPs and SGs, key algorithms includes Value Iteration (VI), Linear (LP) and Quadratic Programming (QP), and Policy Iteration (PI). We refer the reader to standard texts [9,25] for details of these algorithms. For solving stochastic shortest path (SSP) problems, that ask to minimize the cost of reaching a target state, one can use LP for MDPs and VI/PI for SGs. 3 STOCHASTIC GAMES WITH DISTURBANCES In this section, we define stochastic games with disturbances. In these systems, disturbances may occur at runtime and override the decisions of Player 1. For example, as seen in Fig. 1, if the drone wants to move upwards, wind can disturb its actions and push it to the right, completely changing its decision. Definition 2. A Stochastic Game with Disturbances (SGD) is a tupleG=(ํ,ํ 1 ,ํ 2 ,ํด,ํดํฃ,ํ,ํด ํท ,ํดํฃ ํท ,ํ ํท )where(ํ,ํ 1 ,ํ 2 ,ํด,ํดํฃ,ํ) is an SG,ํด ํท is a finite set of disturbance actions (disjoint from ํด),ํดํฃ ํท :ํ 1 โ ํํํค(ํด ํท )is a function specifying the available disturbance actions in Player 1 states, andํ ํท :ํ 1 ร ํด ํท โ Dist(ํ) defines a disturbance transition function. We use|ํ ํท |to denote the number of disturbance transitions in the game. We can define an initial state and strategies for both players in the same way as for an SG. However, since we have disturbance actions here, we also define a disturbance strategy. A disturbance strategy is defined asํฟ:(ํรํด) โ รํ 1 โ ํทํํ ํก(ํด ํท โชโฅ). Here,โฅrepresents that no disturbance action is taken. A run of the game is a sequence of states and actionsํ= ํ 0 ํ 0 ํ 1 ํ 1 . . .where โํ,ํ ํ โ ํ,ํ ํ โ ํดํฃ(ํ ํ ) โช ํดํฃ ํท (ํ ํ ), andํ ํ+1 โ ํ(ํ ํ ,ํ ํ ). For a run ํ= ํ 0 ํ 0 ํ 1 ํ 1 , . . ., we define the total number of disturbances as D ํ (ํ):= ํ ํ | ํ ํ โ ํดํฃ ํท (ํ ํ ) . This number may not be finite, and in that case, we can define the frequency of disturbances as D ํน (ํ):= lim inf ํโโ 1 ํ D ํ (ํ[0,ํ]) , whereํ[0,ํ]denotes the ํ-length prefix of an infinite runํ. We needlim infhere because the limit in general might not exist. Modeling Disturbances as Costs. We can model the disturbances as costs in an SGD by lettingํถ(ํ ,ํ)=1 ifํ โ ํ 1 ,ํ โ ํด ํท , and lettingํถ(ํ ,ํ)= 0 otherwise. Remark 1. Note that for a runํ, the number of disturbances and the frequency of disturbances can be seen as the total cost and the mean payoff of the run respectively, i.e. D ํ (ํ)=ํถ ํ andD ํน (ํ)= MP(ํ) . 3.1 Resilience, Breaking Point, and Their Different Semantics Since disturbances are adversarial, we can assume that they are performed by Player 2. The resilience of a strategy is defined as the maximum number of disturbances that the strategy can withstand while satisfying a given specification. However, this maximum might not exist, for instance if it can withstand<2.5 disturbances on average but cannot withstand 2.5 disturbances. Therefore, a more suitable, well-defined notion would be the breaking point of a strategy, which refers to the minimum number of disturbances required to break it. In this setting, an optimally resilient strategy is a strategy that has the greatest breaking point. There are various natural ways to quantify how many distur- bances are required to break a strategy. One approach is to consider the expected number of disturbances needed to break said strat- egy. Another approach is to determine the maximum number of disturbances required over all possible paths, which we refer to as the worst-case measure throughout this paper. The choice between these measures depends on the application context. Expected re- silience captures average-case behavior and is appropriate when disturbances occur frequently. However, it may obscure rare but critical scenarios in which only a few disturbances suffice to break the strategy. For robustness guarantees, it is often more informative to know how many disturbances the strategy can withstand in the worst case. ํ 0 ํ 1 G B ํ ํ 0.5 0.5 ํ ํ 0.5 0.5 Figure 2: For this SGD, if the objective is to reachํบwith probability>0.4, then the worst-case breaking point is 2, as disturbing just once will not break the policy, and the expected breaking point is 1.1 via an adversary that always disturbs in ํ 0 and with a probability of 0.2 in ํ 1 . 3.2 Induced MDP Under a Player 1 Strategy Given an SGDGand a memoryless Player 1 strategyํ, we useํ ํ to denote the induced MDP underํ, described next. For every state ํ โ ํ 1 , we remove all Player 1 actions except for the one picked by ํ(ํ ), while the disturbance actions remain unchanged. Now, we can think of all states as Player 2 states. Lemma 1. For a memoryless Player 1 strategyํ, there exist a bi- jective functionโthat maps pairs(ํ,ํฟ)of Player 2 and disturbance strategies inG to a strategy ํ in ํ ํ such that โํ โ (ํร ํด) โ ร ํ, P ํ,ํ,ํฟ G,ํ 0 (ํ)= P ํ ํ ํ ,ํ 0 (ํ). This lemma implies that the pair of strategies(ํ,ํฟ)forGis equivalent to strategy ํ for MDP ํ ํ . For a Player 1 strategyํ, a Player 2 strategyํ, a disturbance strategyํฟand an initial stateํ 0 , we can define the induced MC as follows: In Player 2 states, the action is selected byํ. In Player 1 states, ifํฟ(ํ )=โฅthen we pick actionํ(ํ ), whereas we pickํฟ(ํ ) otherwise. We denote the probability measure in the induced MC asP ํ,ํ,ํฟ G,ํ 0 . For any random variableํdefined over infinite paths in G, its expected value with respect to P ํ,ํ,ํฟ G,ํ 0 is E ํ,ํ,ํฟ G,ํ 0 (ํ). 3.3 From SGDs with Finite Disturbances to SGs Here, we show that if the number of disturbances is bounded (by someํ โ N) on all runs, then we can transform an SGDGinto an equivalent SGG โ ํ . This is achieved by unfolding the state space of the SGD to account for the number of disturbances that have already occurred. Specifically, we encode the remaining number of disturbances into the state space, i.e., the new states are of the form (ํ ,ํ), whereํ is a state inGandํ โ โจํ+1โฉrepresents the number of remaining disturbances. Fig. 3 illustrates this transformation. Intuitively, after Player 1 chooses an action in a stateํ โ ํ 1 , a disturbance may or may not occur. To embed this extra step into a standard stochastic game, we create an intermediate state(ํ ,ํ,ํ), controlled by Player 2, that is reached whenever Player 1 plays actionํfromํ . Player 2 then chooses eitherโฅ(no disturbance) or a disturbance actionํ. Ifโฅis chosen, we proceed with the usual transition; ifํis chosen, the transition followsํ ํท and we decre- ment the disturbance counterํ. Hence, each disturbance possibility becomes a normal turn-based move of Player 2, making the distur- bance mechanism explicit in the resulting unfolded game. It can easily be shown that this transformation is sound by showing the equivalence of the two games. ํ ํ โฒ ํ โฒ (ํ ,ํ)(ํ ,ํ,ํ) (ํ โฒ ,ํ โ 1) (ํ โฒ ,ํ) โ ํ ํ ํ 1 ํ 2 ํ ํ 2 โฅ ํ 1 ํ, 1 Figure 3: A gadget in the unfolded stochastic game. Lemma 2. There exist bijective functionsํandํwhereํmaps triplets(ํ,ํ,ํฟ)of strategies inGto pairs( ฬ ํ, ฬ ํ)of strategies in G โ ํ , andํmaps pathsํinGto paths ฬ ํinG โ ํ , such thatโํ โ (ํ ร ํด) โ ร ํ, P ํ,ํ,ํฟ G,ํ 0 (ํ)= P ฬ ํ, ฬ ํ G โ ํ ,(ํ 0 ,ํ) ( ฬ ํ), as long asํฟdisturbs at most ํ times on each run. 4 EXPECTED BREAKING POINT For a given Player 1 strategyํ, we define the set of pairs of strate- gies that breakํasํ ํ := (ํ,ํฟ) | G ํ,ํ,ํฟ ํ 0 |=ยฌํ . We define the expected transient breaking point of ํ as EB ํ G,ํ (ํ) :=inf (ํ,ํฟ)โํ ํ E ํ,ํ,ํฟ G,ํ 0 D ํ (ํ) . When setํ ํ is empty, which means that the strategy cannot be broken, we refer to it asโฎ. When there exist no finite values in ํ ํ , we refer to it asํ. If breaking the strategy requires infinitely many disturbances on average, we can still ask how frequently disturbances are required to break the strategy. For such cases, the expected frequency breaking point is defined as EB ํน G,ํ (ํ) :=inf (ํ,ํฟ)โํ ํ E ํ,ํ,ํฟ G,ํ 0 D ํน (ํ) . Whenํ ํ is empty, we also denote it asโฎ. Definition 3. Given an SGDGand an objectiveํ, the expected breaking point of a Player 1 strategy ํ is given by the pair EB G,ํ (ํ) := EB ํ G,ํ (ํ),EB ํน G,ํ (ํ) . Because of the observation in Remark 1 and Lemma 1, we get the following lemma. Lemma 3. Given an SGD, an objectiveํ, and a memoryless Player 1 strategyํ, it holds thatEB ํ G,ํ (ํ)= inf ํโํ ํ TR(ํ ํ ํ ,ํ 0 ,ํถ), and EB ํน G,ํ (ํ)= inf ํโํ ํ MP(ํ ํ ํ ,ํ 0 ,ํถ). 4.1 Computing the Expected Breaking Point Next, we describe the algorithm for expected transient and fre- quency breaking points for both safety and reachability objectives. We compute the expected breaking point for memoryless strategies here 1 . We use the induced MDPํ ํ and the cost functionํถdefined previously to compute it. Safety. To violate the safety objective, we need to compute the minimum expected cost while reaching states inํตwith probability โฅ1โํ. This is a variant of the standard SSP for which the solution can be found using the LP described in [17]. If there is no solution to the linear program, it is not possible to reachํตwith the required probability, which implies that the expected breaking point does 1 It can easily be extended to finite memory strategies using standard techniques, e.g., encoding the memory in state space by taking product of the game with a finite automaton representing the strategy. not exist. If a solution is found, the frequency breaking point is 0 and the transient breaking point is the solution to the LP. Note that the strategy generated by the LP can be mixed. Reachability. To violate the reachability objective, we need to ensure the avoidance of states in the setํบwith probabilityโฅ1โํ while minimizing cost. We proceed as follows. Defineํตto be the set of MECs inํ ํ \ํบwhere Player 2 can ensure to remain indefinitely without invoking any disturbances. These MECs can be identified by excluding any MEC ofํ ํ \ํบthat have exits via actions suggested by strategy ํ , ํต :=ํ โ MEC(ํ ํ \ํบ) |โํ โฒ โ ํ โฉ ํ 1 : Post ํ ํ (ํ โฒ ,ํ(ํ โฒ )) โ ํ.(1) We also define the setํ of MECs in which Player 2 can remain indefinitely but require disturbance actions to do so 2 , ํ :=ํ โ MEC(ํ ํ \ํบ) |โํ โฒ โ ํ โฉ ํ 1 : Post ํ ํ (ํ โฒ ,ํ(ํ โฒ )) โ ํ=โ ํดํฃ ํท (ํ )โ โ .(2) The probabilities of reachingํตandํ โชํตcan be calculated through standard model checking algorithms. Then, we identify 3 cases: Case 1: Probability to reachํตisโฅ1โํ. The expected cost to reachํตis finite here, making the transient breaking point finite and the frequency breaking point 0. Therefore, the transient breaking point is computed using an SSP formulation with respect to the reachability probability. Case 2: Probability to reachํ โช ํตis<1โ ํ. In this case, it is not possible to break the strategy as the goal states cannot be avoided with the required probability. Both the transient and frequency breaking points areโฎ. Case 3: Probability to reachํตis<1โ ํbutํ โช ํตisโฅ1โ ํ. This is the intermediate case, where finitely many disturbances are not enough to break the strategy. Intuitively, Player 2 cannot force the play to reach states (with the required probability) from which no more disturbances are needed to break the Player 1 strat- egy. Therefore, the transient breaking point isํ, and the expected frequency breaking point is computed as follows. For each MEC inํ , the minimum expected mean payoff of staying inside the MEC is computed. This mean payoff represents the frequency of disturbances required to stay within the MEC. We then construct the weighted MEC quotient ofํ ํ (similar to [2]), by collapsing each MEC inํ to a single abstract state. A new cost function is defined for this quotient MDP. Each collapsed state is augmented with an outgoing transition to a fresh terminal stateํ + , where the new cost of this transition corresponds to the mean payoff of the original MEC. The new cost assigned to all other transitions in the MDP is zero. Finally, we solve an SSP problem with the new cost on this modified MDP to compute the minimum expected cost of reachingํตโชํ + . The solution to this SSP is precisely the expected frequency breaking point of ํ . Theorem 1. Given an SGDG, objectiveํ, Player 1 strategyํ, and pair of values(ํก, ํ), deciding whetherEB G,ํ (ํ) โฅ (ํก, ํ) is in P. ํ ํ โฒ ํ โฒ ํ (ํ ,ํ) ํ โฒ ํ โฒ โ 0 1 ํ ํ ํ 1 ํ 2 ํ ํ 2 โฅ ํ 1 ํ 0 Figure 4: Gadget for converting an SGD into an SG for the Expected Breaking Point. 4.2 Optimal Strategy: Expected Breaking Point The optimally resilient strategy is defined as the strategy that achieves the breaking point EB G,ํ = max ํ EB ํ G,ํ (ํ), max ํ EB ํน G,ํ (ํ) . To compute this, we construct a transformed stochastic game ฬ G from the given SGDGusing the gadget in Fig. 4. This transforma- tion follows the unfolded SG structure introduced in Section 3.3, but omits the use of duplicated copies. Specifically, for each state ํ โ ํ 1 and actionํ โ ํดํฃ(ํ ), we introduce an intermediate Player 2 state(ํ ,ํ), reached deterministically when Player 1 selects action ํ in stateํ . From(ํ ,ํ), Player 2 chooses eitherโฅ, that follows the distributionํ(ํ ,ํ)simulating the undisturbed execution ofํ, or a disturbance actionํ, which follows the distributionํ ํท (ํ ,ํ), simu- lating the effect of a disturbance. To capture the cost, disturbance actions are assigned cost 1, and all others cost 0, as indicated by the boldface labels in Fig. 4. The minimum cost incurred while violating ํin ฬ Gcorresponds to the breaking point. Thus, optimally resilient Player 1 strategies are generally memoryless and randomized for the expected breaking point. Optimal disturbance strategies are also memoryless and randomized; for instance, see Figure 2. Lemma 4. Given an SGDG, objectiveํand memoryless Player 1 strategyํ, it holds thatEB ํ G,ํ (ํ)= inf ํโํ ํ TR( ฬ G ํ,ํ ,ํ 0 ,ํถ)and EB ํน G,ํ (ํ)= inf ํโํ ํ MP( ฬ G ํ,ํ ,ํ 0 ,ํถ). The algorithmโs structure parallels the previous algorithm, with the main difference being that it solves an SG rather than an MDP. Safety. For safety objectives, first the maximum probability to reachํตis computed via a QP with Player 2 as the maximizer. If said probability isโฅ1โ ํ, the problem reduces to solving an SSP problem in the transformed game ฬ G, where the goal is to reach the target setํตwithโฅ1โ ํprobability. The SSP problem can be solved using VI or PI 3 [22]. The SSP problem usually assumes that the target sink (here itโsํต) is reached with probability 1 to ensure that the expected cost is finite. For our case, since there are zero cost paths always available, the same algorithm can be used. Here as soon as the play reachesํบ, the play can be stopped, and the cost is 0. The solution yields the transient breaking point and the frequency breaking point is 0. If the probability to reachํตis<1โํ, it indicates that the strategy is not breakable. 2 We slightly abuse notation by usingํตandํ to also refer to the union of these MECs. 3 The current algorithms for SSP using VI and PI only give approximate solutions with convergence guarantees in the limit. We do not get the exact breaking point in this case, however, if exact solvers for SSP are found in the future, our approach can use them off-the-shelf. Reachability. For reachability objectives, the algorithm first iden- tifies the set of states in ฬ Gfrom which Player 2 can ensure that the target setํบis avoided with probability 1. This is done via a backward fixed-point computation, starting with the setํธ= ํ\ํบ and iteratively removing states according to the following rules until convergence: โขA Player 1 state is removed if there exists an action leading outside ํธ with positive probability. โข A Player 2 state is removed if all available actions lead outside ํธ with positive probability. Next, we compute the maximum probability of reachingํธin ฬ Gusing QP. If the reachability probability is<1โ ํ, the strategy cannot be broken, and the algorithm returns(โฎ,โฎ). If the reachability probability isโฅ1โ ํ, we proceed to analyze the MECs contained inํธ. For each MEC, we compute its minimum mean payoff, which corresponds to the minimal average disturbance cost required to remain within that component indefinitely [8]. Letํต โ ํธdenote the set of MECs with zero mean payoff. Ifํตis reachable with probabilityโฅ1โ ํ, the transient breaking point is finite and the frequency breaking point is 0, indicating that the strategy can be broken with finitely many disturbances. This is computed by solving an SSP problem in ฬ Gwith the target set ํตand probability threshold 1โ ํ. In the other case, the transient breaking point isํ, and the frequency breaking point requires the use of weighted quotient stochastic game that is constructed by collapsing each MEC into a single state. A new terminal stateํ + is introduced and an outgoing transition from all collapsed states toํ + is added, with the cost of this transition equal to the mean payoff of the corresponding MEC. The cost of all other transitions is set to zero. Finally, we solve an SSP problem in this quotient SG to compute the frequency breaking point. Theorem 2. Given an SGDG, objectiveํ, and pair of values(ํก, ํ), deciding whetherEB G,ํ โฅ (ํก, ํ) is as hard as solving SSP for SGs. 5 WORST-CASE BREAKING POINT In contrast to the expected case, we now consider the worst-case number of disturbances required to break a strategy over all possible paths. Now, the worst-case transient breaking point of a strategy is B ํ G,ํ (ํ) :=inf (ํ,ํฟ)โํ ํ inf n ํฅ โ โจํโฉ ํ ํ,ํ,ํฟ G,ํ 0 ํ | D ํ (ํ) โค ํฅ = 1 o . We only require that almost all paths (i.e., with probability 1) have fewer thanํdisturbances, reflecting the common probabilistic convention of ignoring measure-zero events that do not affect the typical behaviors. Recall again that when the setํ ํ is empty, we defineB ํ G,ํ (ํ)to beโฎ, and when there exist no finite values in this set, we denoteB ํ G,ํ (ํ) to beํ. When the transient breaking point isํ, we can compute the frequency of disturbances required. The worst-case frequency breaking point of a Player 1 strategy ํ is B ํน G,ํ (ํ) :=inf (ํ,ํฟ)โํ ํ inf n ํฅ โ [0, 1] ํ ํ,ํ,ํฟ G,ํ 0 ํ | D ํน (ํ) โค ํฅ = 1 o . We can now combine the two values and define the worst-case breaking point of a strategy. Definition 4. Given a SGDGand an objectiveํ, the worst- case breaking point of a Player 1 strategyํis given by the pair B G,ํ (ํ) := B ํ G,ํ (ํ),B ํน G,ํ (ํ) . 5.1 Computing the Worst-Case Breaking Point We describe the algorithm for transient and frequency worst-case breaking points for both safety and reachability objectives. We compute the breaking points for a memoryless strategyํhere, but it can easily be extended to finite-memory strategies by encoding the memory in the state space, similar to the expected case. First, we provide an overview of the key steps, deferring the detailed algorithms for computing the transient and frequency breaking points to later in this section. Ifํis a safety objective, setํตis given as input. And, ifํis a reachability objective, we compute the setํต as defined in Eq. (1). We now compute the maximum probability in the induced MDPํ ํ of reachingํตusing LP. Based on the result, we distinguish three cases: the probability is either>1โํ,<1โํ, or= 1โ ํ. Case 1: Probability to reachํตis>1โ ํ. In this case, the strategy is breakable with finitely many disturbances. Case 2: Probability to reachํตis=1โ ํ. In this case, if the strategy is breakable in a finite number of disturbances, this number should be bounded byํ: the number of disturbance actions present in the graph. We run the procedure to compute the worst-case transient breaking point for|ํ ํท |iterations. Based on the outcome of this procedure, it is further divided into two subcases: a.If the procedure terminates at theํ ํกโ iteration for someํ, we haveB ํ G,ํ (ํ)= ํ. b.If it does not terminate within|ํ ํท |iterations, it requires infinitely many disturbances, making the transient breaking pointํand the frequency breaking point 0. This is due to the fact that there are probabilistic loops that are required to reachํตwith a 1โ ํprobability, whereas the frequency of taking that action in the long term would still be 0. Case 3: Probability to reachํตis<1โ ํ. Here, ifํis a safety objective, the strategy is not breakable with any amount of disturbances. Ifํis a reachability objective, we compute the setํ using Eq. (2). If the probability of reachingํ โช ํตis<1โ ํ, again, the strategy is not breakable with any amount of disturbances and the algorithm returns(โฎ,โฎ). If the probability of reachingํ โช ํต isโฅ1โ ํ, the strategy is breakable but requires infinitely many disturbances. This results in the transient breaking point being ํand the frequency breaking point being computed using the procedure described later. 5.1.1 Transient Breaking Point. Givenํ, 4 we want to verify if B ํ G,ํ (ํ) โค ํ . We define a sequence ofํreachability LPs where theํ ํกโ LP checks if the strategyํcan be broken using at mostํ disturbances. Theํ ํกโ LP uses the solution of the(ํโ1) ํ ํก LP and allows one more disturbance to compute the probability of reaching ํตwith at mostํdisturbances. If the solution ofํ ํกโ LP isโฅ1โ ํ,ํ is breakable usingํdisturbances. For completeness, the explicit LP can be found in the supplementary material. 4 An upper bound here, if it is finite, can be computed by counting the number of iterations required by VI for MDPs to go beyond probability 1โ ํ of reaching ํต. ํ 0 ํ 1 ํ 2 ํ 3 G B ํ ํ ํ 1 ํ 2 ํ 0.5 0.5 ํ ํ 0.5 0.5 ํ 1 ํ 2 ํ 3 G B ํ ํ ํ ํ ํ ํ 0.5 0.5 0.5 0.5 Figure 5: An SGD where the most resilientํmust have mem- ory even ifํฟis memoryless (left), and one where the optimal ํฟ must rely on memory even if ํ is memoryless (right). Each LP is solved in polynomial time, and each iteration only re- quires the result of the previous LP. This gives us an algorithm that is polynomial in terms of|G|andํ. This gives us a parametrized polytime complexity whereํis given in unary, and in general a PSPACEalgorithm. It can also be shown that the optimal distur- bance strategy here may require memory of size ํ . 5.1.2 Frequency Breaking Point. Recall that the frequency breaking point is only computed when the specification is reachability and the probability of reachingํตis<1โ ํbut the probability of reaching ํ โช ํต isโฅ 1โ ํ. As in the expected case, the procedure assigns a frequency of disturbances required to stay within the setํตas 0 and assigns the mean payoff for the MECs in the setํ as their frequency. In contrast to the expected case, where we solved a SSP to find the final expected value, we need to consider the worst case. Here, we iteratively remove a MEC with the highest disturbance frequency. After each removal, it recomputes the probability of reaching the remaining MECs inํ โช ํต. This process continues until the prob- ability of reaching the remaining MECs drops below 1โ ํ. The frequency of disturbances required to remain in the last removed MEC is then returned as the frequency breaking point. Theorem 3. Given an SGDG, objectiveํ, Player 1 strategyํ, and pair of values(ํก, ํ), deciding ifB G,ํ (ํ) โฅ (ํก, ํ) is in PSPACE. 5.2 Optimal Strategy: Worst-Case Breaking Point An optimally resilient strategy is a strategy that achieves the fol- lowing worst-case breaking point: B G,ํ = max ํ B ํ G,ํ (ํ), max ํ B ํน G,ํ (ํ) We first discuss memory requirements for transient and frequency breaking points, and later provide the algorithm to compute them. 5.2.1 Memory Requirements for Transient Breaking Point. Making use of the reduction to standard stochastic games from Section 3.3, we next show that deciding the worst-case transient breaking point is equivalent to solving the unfolded stochastic game. This allows us to use results concerning stationarity in standard SGs to reason about memory requirements in SGDs. Lemma 5. LetGbe an SGD andG โ ํ its correspondingํ-unfolded stochastic game, for someํ โ โจํโฉ. Then, for all Player 1 strategiesํ, we haveB ํ G,ํ (ํ) โค ํ if and only if sup ฬ ํ P ฬ ํ, ฬ ํ G โ ํ ,(ํ 0 ,ํ) (ยฌํ) โฅ 1โ ํ. If we letํbe the optimal breaking point,ํ= max ํโฮ B ํ G,ํ (ํ), then the unfolded gameG โ ํ is a standard stochastic game, and the optimal strategies for both players are therefore memoryless [27]. Lemma 5, together with Lemma 2, implies that an SGDGis station- ary with respect to the state-counter pair(ํ ,ํ). Here,ํrepresents the number of disturbances remaining, and the pair(ํ ,ํ)uniquely identifies a state in the corresponding unfolded game. Consequently, we can derive the following two corollaries. Corollary 1. For any SGDG, there exists an optimally resilient Player 1 strategy of the form ํ โ : ํรโจํ+ 1โฉ โ ํด. Corollary 2. For any SGDG, there exists an optimalํ-disturbance strategy of the form ํฟ โ : ํรโจํ+ 1โฉ โ ํด. In the next two examples, we construct SGDs where the optimal strategies require memory. Example 1. LetGbe as in Figure 5 (left) withํ= ํ โฅ0.75 (โฆG). There is a step-counting strategy of the formํ โ :ํรโจ2โฉ โ ํดwith a worst-case transient breaking point of 2:ํ โ (ํ 0 , _)= ํ,ํ โ (ํ 1 ,0)= ํ,ํ โ (ํ 1 ,1)= ํ,ํ โ (ํ 3 , _)= ํ, andํ โ (ํ 2 , _)= ํ. In contrast, no memoryless Player 1 strategy can achieve a breaking point of 2. Example 2. LetGbe as in Figure 5 (right) withํ= ํ โฅ0.5 (โฆG). De- fine the memoryless Player 1 strategyํ(ํ )= ํfor every stateํ . Then, ํhas the worst-case transient breaking point of 3, as the following step-counting 3-disturbance strategy breaks it:ํฟ(ํ 1 ,3)=โฅ,ํฟ(ํ 1 ,2)= ํฟ(ํ 1 ,1)=ํ,ํฟ(ํ 2 , _)=ํ,ํฟ(_,0)=โฅ. Yet, no memoryless disturbance strategy that disturbs at most 3 times can break ํ. In general, it is necessary for optimal strategies to perform step counting (i.e., their memory is of the formํรโจํ+1โฉ), as seen in Examples 1 and 2, while Corollaries 1 and 2 show this is sufficient. Thus, we always assume that optimal strategies have this form in the case of worst-case transient resilience without loss of generality. 5.2.2 Memory Requirements for Frequency Breaking Point. In con- trast to the transient case, memoryless strategies are sufficient for the frequency breaking point. We discuss this for reachability ob- jectives; in the case of safety objectives either it can be broken with finite disturbances or it cannot be broken at all. Lemma 6. Ifํis reachability, and it is not possible to break the strat- egy with finite disturbances, then the optimal disturbance strategy is memoryless. The intuition behind Lemma 6 is that, since the strategy cannot be broken with finite disturbances, the disturbance strategy must rely on staying in some MECs of the MDP induced by the Player 1 strategy. In these MECs, the optimal disturbance strategy to mini- mize the mean payoff is memoryless. Thus, the overall disturbance strategy can be chosen to be memoryless. 5.2.3 Computing Optimally Resilient Strategies. The procedure here is similar to the procedure in Section 4.2. Here also, we use the transformation to ฬ G. Ifํis safety, then the probability of reaching ํตis computed. If it is<1โํ, then the strategy is not breakable. In the other case, the frequency breaking point is 0 and the transient breaking point is computed as described later in this section. Ifํis reachability, then the algorithm computes the set of states ํธ from which Player 2 can force the play to never reach ํบ . This can be computed using the fix-point computation as de- scribed in Section 4.2. If the maximum probability of reachingํธis <1โํ, then the strategy is again not breakable. If it isโฅ1โํ, the minimum mean payoff of each MEC inํธis computed, which gives us the minimum frequency of disturbances required to stay in that MEC. Letํตbe the set of MECs inํธwith 0 mean payoff and ifํตis reachable with probabilityโฅ1โ ํ, then the frequency breaking point is 0 and the transient breaking point is computed as described next. Otherwise, the algorithm iteratively removes a MEC with the highest disturbance frequency. After each removal, it recomputes the probability of reaching the remaining MECs inํธ. This process continues until the probability of reaching the remaining MECs drops below 1โ ํ. The frequency required to remain in the last removed MEC is then returned as the frequency breaking point. 5.2.4 Transient Breaking Point. Givenํ, we want to verify whether B ํ G,ํ โค ํ. We define a sequence ofํQPs where theํ ํกโ QP checks if all strategiesํcan be broken using at mostํdisturbances. Here too, theํ ํกโ QP uses the solution of the(ํโ1) ํกโ QP, and by allowing one more disturbance, it computes the probability of reachingํต withํdisturbances. Intuitively, theํ ํกโ QP solves for the maximum probability of reaching bad states using the method in [10] in the game unfolded forํdisturbances (Section 3.3) but reuses results from the game unfolded forํโ1 disturbances. Description of these QPs is provided in the Supplementary Material. Note that the decision problem corresponding to these specific QPs can be solved in NP [10], but in our case we also need to find the solution of the QP. This can be extracted using polynomially manyNPqueries, where inํ ํกโ query we will ask whether theํ ํกโ bit of the solution is 1. Also, in each iteration, we only need to remember the solution of the last iteration. Thus, we can solve this in polynomial time with anNPoracle ifํis given in unary. In practice, theNP-oracle complexity would involve querying a SAT solver polynomially many times to extract the solution bit-by-bit, and we would expect the state-of-the-art SAT-solvers to scale well. Theorem 4. Given an SGDG, an objectiveํ, and a pair of values (ํก, ํ), deciding whetherB G,ํ โฅ (ํก, ํ) is in PSPACE. 6 CONCLUSIONS AND FUTURE WORK In this work, we explored the concept of resilient strategies in stochastic systems to analyze their robustness against disturbances. We introduced novel formulations for resilience by considering both expected and worst-case breaking points, and refined the notion of resilience through measures such as frequency-based disturbances. We provided algorithms for computing resilience, offering solutions for both expected and worst-case scenarios, and highlighted the trade-offs between optimality and resilience. By introducing this mathematical framework, as well as providing proofs of properties of general theoretical interest, our work can serve as a foundation for developing practical solutions to real-world problems. Future work includes extending these concepts to partially observable Markov decision processes (POMDPs), multi-agent settings, and alternative objectives beyond reachability and safety. ACKNOWLEDGMENTS Kush Grover was partially supported by the STEP-RL project funded by the European Research Council under GA number 101115870. Markel Zubia and Nils Jansen were partially supported by the Euro- pean Research Council Starting Grant 101077178 (DEUCE). Debraj Chakraborty was partially supported by the National Research Foundation, Singapore, under its RSS Scheme (NRF-RSS2022-009), and the Intelligence-Oriented Verification & Controller Synthe- sis (InOVationCS) project funded by the European Union under Grant Agreement number 101171844. Jan Kลetinskโy was partially supported by the DFG project GOPro funded by the German Re- search Foundation (DFG) under project number 427755713, the MUNI Award in Science and Humanities (MUNI/I/1757/2021), and the Intelligence-Oriented Verification & Controller Synthesis (In- OVationCS) project funded by the European Union under Grant Agreement number 101171844. REFERENCES [1]Gul Agha and Karl Palmskog. 2018. A survey of statistical model checking. ACM Transactions on Modeling and Computer Simulation (TOMACS) 28, 1 (2018), 1โ39. [2]Pranav Ashok, Krishnendu Chatterjee, Przemysลaw Daca, Jan Kลetรญnskรฝ, and Tobias Meggendorfer. 2017. Value Iteration for Long-Run Average Reward in Markov Decision Processes. In Computer Aided Verification, Rupak Majumdar and Viktor Kunฤak (Eds.). Springer International Publishing, Cham, 201โ221. [3] Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap, Jan Kลetรญnsk ` y, Maximilian Weininger, and Majid Zamani. 2020. dtControl: decision tree learning algorithms for controller representation. In Proceedings of the 23rd international conference on hybrid systems: Computation and control. 1โ7. [4] Pranav Ashok, Jan Kลetรญnsk ` y, and Maximilian Weininger. 2019. PAC statisti- cal model checking for Markov decision processes and stochastic games. In International Conference on Computer Aided Verification. Springer, 497โ519. [5] Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press. [6] Alexander Benvenuti, Calvin Hawkins, Brandon Fallin, Bo Chen, Brendan Bialy, Miriam Dennis, and Matthew Hale. 2024. Differentially Private Reward Functions for Markov Decision Processes. In 2024 IEEE Conference on Control Technology and Applications (CCTA). 631โ636. https://doi.org/10.1109/CCTA60707.2024.10666610 [7]Roderick Paul Bloem, Rรผdiger Ehlers, Swen Jacobs, and Robert Kรถnighofer. 2014. How to Handle Assumptions in Synthesis. In Proceedings 3rd Workshop on Synthe- sis (SYNT 2014) (EPTCS). Electronic Proceedings in Theoretical Computer Science, 34โ50. https://doi.org/10.4204/EPTCS.157.7 Workshop on Synthesis (SYNT 2014) ; Conference date: 23-07-2014 Through 24-07-2014. [8]Endre Boros, Khaled Elbassioni, Vladimir Gurvich, and Kazuhisa Makino. 2017. A convex programming-based algorithm for mean payoff stochastic games with perfect information. Optimization Letters 11, 8 (2017), 1499โ1512. https://doi. org/10.1007/s11590-017-1140-y [9]Anne Condon. 1990. On Algorithms for Simple Stochastic Games. Advances in computational complexity theory 13 (1990), 51โ72. [10]Anne Condon. 1992. The complexity of stochastic games. Information and Computation 96, 2 (1992), 203โ224. [11]Eric Dallal, Daniel Neider, and Paulo Tabuada. 2016. Synthesis of safety controllers robust to unmodeled intermittent disturbances. In 2016 IEEE 55th Conference on Decision and Control (CDC). 7425โ7430. https://doi.org/10.1109/CDC.2016. 7799416 [12]Parham Gohari, Matthew Hale, and Ufuk Topcu. 2020. Privacy-Preserving Policy Synthesis in Markov Decision Processes. In 2020 59th IEEE Conference on Decision and Control (CDC) (Jeju Island, Korea (South)). IEEE Press, 6266โ6271. https: //doi.org/10.1109/CDC42340.2020.9304015 [13] C Hopps. 2000. Rfc2992: Analysis of an equal-cost multi-path algorithm. [14] Andrey Kolobov, Mausam, and Daniel S. Weld. 2012. A theory of goal-oriented MDPs with dead ends. In Proceedings of the Twenty-Eighth Conference on Un- certainty in Artificial Intelligence (Catalina Island, CA) (UAIโ12). AUAI Press, Arlington, Virginia, USA, 438โ447. [15]Jan Kลetรญnskรฝ, Tobias Meggendorfer, Maximilian Prokop, and Sabine Rieder. 2023. Guessing winning policies in LTL synthesis by semantic learning. In International Conference on Computer Aided Verification. Springer, 390โ414. [16] Jan Kลetรญnsk ` y, Emanuel Ramneantu, Alexander Slivinskiy, and Maximilian Weininger. 2022. Comparison of algorithms for simple stochastic games. Infor- mation and Computation 289 (2022), 104885. [17]Isabella Kuo and Valdinei Freire. 2021. Probability-to-Goal and Expected Cost Trade-Off in Stochastic Shortest Path. In Computational Science and Its Applica- tions โ ICCSA 2021, Osvaldo Gervasi, Beniamino Murgante, Sanjay Misra, Chiara Garau, Ivan Bleฤiฤ, David Taniar, Bernady O. Apduhan, Ana Maria A. C. Rocha, Eufemia Tarantino, and Carmelo Maria Torre (Eds.). Springer International Pub- lishing, Cham, 111โ125. [18]Zhengshang Liu, Yue Yang, Tim Miller, and Peta Masters. 2021. Deceptive Rein- forcement Learning for Privacy-Preserving Planning. In Proceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems (Virtual Event, United Kingdom) (AAMAS โ21). International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC, 818โ826. [19]Alberto Marchesi and Nicola Gatti. 2021. Trembling-Hand Perfection and Cor- relation in Sequential Games. Proceedings of the AAAI Conference on Artificial Intelligence 35, 6 (May 2021), 5566โ5574. https://doi.org/10.1609/aaai.v35i6.16700 [20]Daniel Neider, Patrick Totzke, and Martin Zimmermann. 2020. Optimally Resilient Strategies in Pushdown Safety Games. In 45th International Sympo- sium on Mathematical Foundations of Computer Science, MFCS 2020, August 24- 28, 2020, Prague, Czech Republic (LIPIcs, Vol. 170), Javier Esparza and Daniel Krรกlโ (Eds.). Schloss Dagstuhl - Leibniz-Zentrum fรผr Informatik, 74:1โ74:15. https://doi.org/10.4230/LIPICS.MFCS.2020.74 [21]Daniel Neider, Alexander Weinert, and Martin Zimmermann. 2020. Synthesizing optimally resilient controllers. Acta Informatica 57, 1-2 (2020), 195โ221. https: //doi.org/10.1007/S00236-019-00345-7 [22]Stephen D Patek and Dimitri P Bertsekas. 1999. Stochastic shortest path games. SIAM Journal on Control and Optimization 37, 3 (1999), 804โ824. [23]Shashank Pathak, Erika รbrahรกm, Nils Jansen, Armando Tacchella, and Joost- Pieter Katoen. 2015. A Greedy Approach for the Efficient Repair of Stochastic Models. In NFM (Lecture Notes in Computer Science, Vol. 9058). Springer, 295โ309. [24]Vern Paxson. 1997. End-to-end Internet packet dynamics. In Proceedings of the ACM SIGCOMMโ97 conference on Applications, technologies, architectures, and protocols for computer communication. 139โ152. [25]Martin L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming (1st ed.). John Wiley & Sons, Inc., USA. [26]Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck, and Daniel Neider. 2020. Resilient Abstraction-Based Controller Design. In 2020 59th IEEE Conference on Decision and Control (CDC). 2123โ2129. https://doi.org/10.1109/CDC42340.2020. 9303932 [27]Lloyd S Shapley. 1953. Stochastic games. Proceedings of the national academy of sciences 39, 10 (1953), 1095โ1100. [28]Felipe W. Trevizan, Florent Teichteil-Kรถnigsbuch, and Sylvie Thiรฉbaux. 2017. Efficient solutions for Stochastic Shortest Path Problems with Dead Ends. In Proceedings of the Thirty-Third Conference on Uncertainty in Artificial Intelligence, UAI 2017, Sydney, Australia, August 11-15, 2017, Gal Elidan, Kristian Kersting, and Alexander Ihler (Eds.). AUAI Press. http://auai.org/uai2017/proceedings/papers/ 280.pdf [29]Moshe Y. Vardi. 2020. Efficiency vs. resilience: what COVID-19 teaches computing. Commun. ACM 63, 5 (April 2020), 9. https://doi.org/10.1145/3388890 [30]Pian Yu, Shufang Zhu, Giuseppe De Giacomo, Marta Kwiatkowska, and Moshe Vardi. 2024. The Trembling-Hand Problem for LTLf Planning. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI- 24, Kate Larson (Ed.). International Joint Conferences on Artificial Intelligence Organization, 3631โ3641. https://doi.org/10.24963/ijcai.2024/402 Main Track. [31] Yuanhui Zhang, Haipeng Wu, Brian T Denton, James R Wilson, and Jennifer M Lobo. 2019. Probabilistic sensitivity analysis on Markov models with uncertain transition probabilities: an application in evaluating treatment decisions for type 2 diabetes. Health Care Manag. Sci. 22, 1 (March 2019), 34โ52. A STOCHASTIC GAMES WITH DISTURBANCES (SECTION 3) A.1 Induced MDP under a Player 1 Strategy Definition 5. For a Player 1 memoryless strategyํin an SGD G, the induced MDP is defined as ํ ํ =( ฬ ํ, ฬ ํด, ฬ ํดํฃ, ฬ ํ), where โข ฬ ํ= ํ 1 โช ํ 2 โข ฬ ํด= ํดโช ํด ํท โข ฬ ํดํฃ(ํ )= ( ํ(ํ )โช ํดํฃ ํท (ํ ) ํ โ ํ 1 ํดํฃ(ํ )ํ โ ํ 2 โข ฬ ํ(ํ ,ํ,ํ โฒ )= ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃณ ํ(ํ ,ํ,ํ โฒ ) ํ โ ํ 1 ,ํ= ํ(ํ ) ํ ํท (ํ ,ํ,ํ โฒ ) ํ โ ํ 1 ,ํ โ ํดํฃ ํท (ํ ) ํ(ํ ,ํ,ํ โฒ ) ํ โ ํ 2 ,ํ โ ํดํฃ(ํ ) Lemma 1. For a memoryless Player 1 strategyํ, there exist a bi- jective functionโthat maps pairs(ํ,ํฟ)of Player 2 and disturbance strategies inG to a strategy ํ in ํ ํ such that โํ โ (ํร ํด) โ ร ํ, P ํ,ํ,ํฟ G,ํ 0 (ํ)= P ํ ํ ํ ,ํ 0 (ํ). Proof. Forward direction: Given induced MDPํ ํ and strate- giesํ,ํฟ,โmaps them to a strategyํofํ ํ which is defined as follows: ํ(ํค ยท ํ )= ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃณ ํ(ํค ยท ํ ) ํ โ ํ 1 ,ํฟ(ํค ยท ํ )=โฅ ํฟ(ํค ยท ํ ) ํ โ ํ 1 ,ํฟ(ํค ยท ํ )โ โฅ ํ(ํค ยท ํ ) ํ โ ํ 2 Therefore, โ(ํ,ํฟ)= ํ. Note that for each finite path ofG ํ,ํ,ํฟ ํ 0 there is an equivalent path inํ ํ ํ,ํ 0 that has the same probability and reaches the same state. This gives us that for all paths inG ํ,ํ,ํฟ ํ 0 that reachesํต, there are equivalent paths inํ ํ ํ,ํ 0 that reachesํต. This also shows that the probability of reaching ํต is the same in both. Backward direction: Given a strategyํforํ ํ , we construct a Player 2 strategy and a disturbance strategy as follows: ํ(ํค ยท ํ )= ํ(ํค ยท ํ ) ํ โ ํ 2 ํฟ(ํค ยท ํ )= ( โฅํ โ ํ 1 , ํ(ํค ยท ํ ) โ ํดํฃ(ํ ) ํ(ํค ยท ํ ) ํ โ ํ 1 , ํ(ํค ยท ํ ) โ ํดํฃ ํท (ํ ) Again, for each path ofํ ํ,ํ 0 there is an equivalent path inG ํ,ํ,ํฟ ํ 0 that reaches the same state with same probability. With the same argument as the previous case, the probability of reachingํตis same in both. Note that in this case,โ(ํ,ํฟ)= ํ, proving thatโis a bijection.โก This immediately gives us the following corollary. Corollary 3. Given a set of statesํต โ ํ. For each set of game strategies(ํ,ํ,ํฟ), there exist a strategyํforํ ํ such thatํ ํ,ํ,ํฟ G,ํ 0 (โฆํต) = ํ ํ ํ ํ ,ํ 0 (โฆํต) and vice versa. A.2 Converting SGDs with Finite Disturbances to SGs Definition 6. LetG= (ํ,ํ 1 ,ํ 2 , ํด,ํดํฃ,ํ,ํด ํท ,ํดํฃ ํท ,ํ ํท )be an SGD and letํ โ โจํโฉ. Its correspondingํ-unfolded stochastic game is an SGG โ ํ =(ํ โ ํ ,ํ โ ํ 1 ,ํ โ ํ 2 ,ํด โ ํ ,ํดํฃ โ ํ ,ํ โ ํ ) where โข ํ โ ํ 1 = ํ 1 รโจํ+ 1โฉ. โข ํ โ ํ 2 = ํ 2 รโจํ+ 1โฉโช ํ 1 รโจํ+ 1โฉร ํด. โข ํ โ ํ = ํ โ ํ 1 โช ํ โ ํ 2 . โข ํด โ ํ = ํดโช ํด ํท โชโฅ. โข ํดํฃ โ ํ (ํ )= ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃณ ํดํฃ( ฬ ํ )if ํ =( ฬ ํ ,ํ), ฬ ํ โ ํ 1 ํดํฃ( ฬ ํ )if ํ =( ฬ ํ ,ํ), ฬ ํ โ ํ 2 ํดํฃ ํท ( ฬ ํ )โชโฅ if ํ =( ฬ ํ ,ํ,ํ), ฬ ํ โ ํ 1 โข ํ โ ํ (ํ ,ํ,ํ โฒ )= ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃณ ํ( ฬ ํ ,ํ, ฬ ํ โฒ ) ํ =( ฬ ํ ,ํ), ฬ ํ โ ํ 2 ,ํ โฒ =( ฬ ํ โฒ ,ํ) 0ํ =( ฬ ํ ,ํ), ฬ ํ โ ํ 2 ํ( ฬ ํ ,ํ, ฬ ํ โฒ ) ํ =( ฬ ํ , 0), ฬ ํ โ ํ 1 ,ํ โฒ =( ฬ ํ โฒ , 0) 0ํ =( ฬ ํ , 0), ฬ ํ โ ํ 1 1ํ =( ฬ ํ ,ํ+ 1), ฬ ํ โ ํ 1 ,ํ โฒ =( ฬ ํ ,ํ+ 1,ํ) 0ํ =( ฬ ํ ,ํ+ 1), ฬ ํ โ ํ 1 ํ( ฬ ํ , ฬ ํ, ฬ ํ โฒ ) ํ =( ฬ ํ ,ํ, ฬ ํ),ํ=โฅ,ํ โฒ =( ฬ ํ โฒ ,ํ) 0ํ =( ฬ ํ ,ํ, ฬ ํ),ํ=โฅ ํ ํท ( ฬ ํ , ฬ ํ, ฬ ํ โฒ ) ํ =( ฬ ํ ,ํ+ 1, ฬ ํ), ฬ ํ โ ํด ํท ,ํ โฒ =( ฬ ํ โฒ ,ํ) 0ํ =( ฬ ํ ,ํ, ฬ ํ), ฬ ํ โ ํด ํท Lemma 2. There exist bijective functionsํandํwhereํmaps triplets(ํ,ํ,ํฟ)of strategies inGto pairs( ฬ ํ, ฬ ํ)of strategies in G โ ํ , andํmaps pathsํinGto paths ฬ ํinG โ ํ , such thatโํ โ (ํ ร ํด) โ ร ํ, P ํ,ํ,ํฟ G,ํ 0 (ํ)= P ฬ ํ, ฬ ํ G โ ํ ,(ํ 0 ,ํ) ( ฬ ํ) , as long asํฟdisturbs at most ํ times on each run. Proof. Notice that the difference betweenGandG โ ํ is the use of the gadget shown in Figure 3 that converts disturbance edges into Player 2 states. Given a pathํinG, we can getํ(ํ)= ฬ ํby doing the following: โข Each Player 2 stateํ inํis replaced with a tuple(ํ ,ํ), where ํis the number of disturbance edgesํ โ ํด ํท present inํup until ํ , โขEach Player 1 stateํ inํis replaced with a tuple(ํ ,ํ), simi- larly to the previous step. Ifํ is followed up inํby a player actionํ โ ํด, we can replace it by the actionํ, a visit to the node(ํ ,ํ,ํ), and actionโฅ. Otherwise, ifํ is followed up by a disturbance actionํ โ ํด ํท , we must replace it by the actionํ(ํ), a visit to node(ํ ,ํ,ํ), actionํ, and decrement the counter of the successor state by 1. Sinceํฟdisturbs at mostํtimes by assumption, the counter can never go below 0. We obtain ฬ ํby just letting ฬ ํ( ฬ ํ)= ํ(ํ), while ฬ ํ( ฬ ํ)is just a combination ofํandํฟ, depending on whether we are on a(ํ ,ํ)or a(ํ ,ํ,ํ)node. By construction ofG โ ํ , it is clear thatํand ฬ ํhave the same probabilities under the respective policies.โก B EXPECTED BREAKING POINT (SECTION 4) Lemma 3. Given an SGD, an objectiveํ, and a memoryless Player 1 strategyํ, it holds thatEB ํ G,ํ (ํ)= inf ํโํ ํ TR(ํ ํ ํ ,ํ 0 ,ํถ) , and EB ํน G,ํ (ํ)= inf ํโํ ํ MP(ํ ํ ํ ,ํ 0 ,ํถ). Proof. โข EB ํ G,ํ (ํ) : From the cost functionํถ, we get that for each runํ, the number of disturbances is equal to the cost of that run, i.e. ํถ ํ = ํท ํ (ํ) Therefore, the expected cost of a runํinํ ํ ํ is equal to the expected number of disturbances. E ํ ํ ํ ,ํ 0 (ํถ ํ )= E ํ ํ ํ ,ํ 0 (ํท ํ (ํ)) inf ํโํ ํ E ํ ํ ํ ,ํ 0 (ํถ ํ )= inf ํโํ ํ E ํ ํ ํ ,ํ 0 (ํท ํ (ํ)) EB ํ G,ํ (ํ)= inf ํโํ ํ ํํ (ํ ํ ํ ,ํ 0 ,ํถ) Hence, the minimum expected cost to violateํis equal to the minimum expected number of disturbances required to violate ํ . โข EB ํน G,ํ (ํ): This is similar to the previous case, but here we use the equivalence of mean payoff on a run to the frequency of disturbances on that run and get the following: EB ํน G,ํ (ํ)= inf ํโํ ํ ํํ(ํ ํ ํ ,ํ 0 ,ํถ)โก B.1 Solving Stochastic Shortest Path Problems In its usual setting, the SSP assumes that the probability of reaching the target states is 1. This assumption is required because if the run reaches any other end component with any positive proba- bility where the minimum cost is infinite, the total expected cost becomes infinite. To handle cases where probability to reach the required states is not one, several other criteria have been explored in the literature, for example, SSP with Unavoidable Dead Ends (iSSPUDE) [14] and Minimum Cost Given Maximum Probability (MCMP) [28]. In iSSPUDE, the probability to reach the target is maximized with higher priority and the cost is minimized later. However, in this setting, only the costs for paths that reach the target states count. Other paths, that do not reach the target states are not counted, or equivalently they are assigned zero cost. In MCMP, the priority is still maximizing the probability however the cost for runs that do not reach the target state is also counted up until the point when it is not possible to reach the target anymore. The intuition behind this is that once the run reaches these end components, the play is stopped and more cost does not accumu- late. This is handled by allowing a giving up action that ends the run once it reaches a state that cannot reach the target anymore, making sure that no more cost is accumulated. Our setting is quite similar to MCMP, since violatingํis a hard constraint and there- fore prioritized. Also, the giving up action is always present since there is always a non-disturbance action with zero cost from every state, defined by the Player 1 strategyํ. This can ensure zero cost runs once the run reaches end components from which it is not possible to reach the target anymore. To solve the MCMP case, solutions using Linear Programs have been explored in [17]. To write the linear program, we first need to define variablesํฅ ํ ,ํ that represents the probability of picking actionํfrom stateํ . These variables are used to define the flow of probability mass. The constraints of the linear program are defined using flow equations and the objective is to minimize the cost function. The inward and outward flows of a state are defined as: ํํ(ํ )= โ๏ธ ํ โฒ โ ฬ ํ,ํโ ฬ ํด ํฅ ํ โฒ ,ํ ํ(ํ ,ํ,ํ โฒ ) ํํขํก(ํ )= โ๏ธ ํโ ฬ ํดํฃ(ํ ) ํฅ ํ ,ํ . The linear program is defined as follows: min ํฅ ํ ,ํ โ๏ธ ํ โ ฬ ํ,ํโ ฬ ํด ํฅ ํ ,ํ ํถ(ํ ,ํ)(3) s.t.ํฅ ํ ,ํ โฅ 0โํ โ ฬ ํ,ํ โ ฬ ํด(4) ํํขํก(ํ )โํํ(ํ ) โค 0 โํ โ ฬ ํ\(ํตโชํ 0 )(5) ํํขํก(ํ 0 )โํํ(ํ 0 ) โค 1(6) โ๏ธ ํ ํ โํต ํํ(ํ ํ ) โฅ 1โ ํ(7) Note that this gives the values ofํฅ ํ ,ํ in[0,1]which are the probability of picking actionํfrom stateํ . Thus, the resulting policy is randomized. B.2 Weighted MEC Quotient Letํbe an MDP with MECsํํธํถ(ํ)=(ํ 1 ,ํ 1 ), . . .,(ํ ํ ,ํ ํ ). Fur- ther, defineํํธํถ ํ = ร ํ ํ=1 ํ ํ as the set of all states contained in some MEC. The MEC quotient ofํis defined as the MDP ห ํ=( ห ํ, ห ํด, ห ํดํฃ, ห ํ), where: โข ห ํ= ํ\ ํํธํถ ํ โช ห ํ 1 , . . . ห ํ ํ , โข ห ํด=(ํ ,ํ) | ํ โ ํ,ํด โ ํดํฃ(ํ ), โข ห ํดํฃ(ํ )= ( (ํ ,ํ) | ํ โ ํดํฃ(ํ )โํ โ ํ\ ํํธํถ ํ (ํ ,ํ) | ํ โ ํ ํ ,ํ โ ํดํฃ(ํ )\ ํ ํ โ1โค ํ โค ํ , โข ห ํ( ห ํ ,(ํ ,ํ), ห ํ โฒ )= ( ร ํ โฒ โํ ํ ํ(ํ ,ํ,ํ โฒ ) ห ํ โฒ = ห ํ ํ ํ(ํ ,ํ, ห ํ โฒ ) ห ํ โฒ โ ํ\ ํํธํถ ํ Ifํ 0 is in someํ ํ , then ห ํ ํ is the initial state of ห ํ, otherwiseํ 0 is the initial state of ห ํ . Let ห ํbet the MEC quotient ofํand letํํธํถ ห ํ = ห ํ 1 , . . . ห ํ ํ be the set of collapsed states. Further, letํ:ํํธํถ ห ํ โ [0,1]be a function assigning a value to every collapsed state. We define the weighted MEC quotient ofํas the MDPํ ํ = (ํ ํ , ห ํดโชํ ํกํํฆ,ํดํฃ ํ ,ํ ํ ), where โข ํ ํ = ห ํโชํ + , โข ํดํฃ ํ ( ห ํ ) is defined as โ ห ํ โ ห ํ. ํดํฃ ํ ( ห ํ )= ( ห ํดํฃ( ห ํ )โชํ ํกํํฆ ห ํ โ ํํธํถ ห ํ ห ํดํฃ( ห ํ )otherwise ํดํฃ ํ (ํ + )=โ โข ํ ํ is defined as โ ห ํ โ ห ํ, ห ํ โ ห ํด.ํ ํ ( ห ํ , ห ํ)= ห ํ( ห ํ , ห ํ)(8) โ ห ํ ํ โ ํํธํถ ห ํ .ํ ํ ( ห ํ ํ ,ํ ํกํํฆ,ํ + )= 1(9) (10) Figure 6: An example of how the MEC quotient is constructed. By ํ, r we denote that the action ํ yields a cost of r Algorithm 1 Computing Expected Breaking Point of a Player 1 Strategy 1: Input: G,ํ,ํ 2: Output: (EB ํ G,ํ (ํ),EB ํ G,ํ (ํ)) 3: ํ ํ โ ํผํํํขํํํํํทํ(G,ํ) 4: if ํ= ํ >ํ (โกยฌํต) then// Safety 5: ํต โ Input from ํ 6: else if ํ= ํ >ํ (โฆํบ) then// Reachability 7: ํต โ Compute Using Eq. (1) 8: end if 9: ํ ํ โ Reachability-LP(ํ ํ ,ํ โฅ1โํ (โฆํต) ) 10: if ํ ํ 0 โฅ 1โ ํ then 11: EB ํ โ SSP-LP(ํ ํ ,ํต, 1โ ํ) 12: return (EB ํ , 0) 13: else if ํ= ํ >ํ (โกยฌํต) then// safety=โ unbreakable 14: return (โฎ,โฎ) 15: else// reachability=โ frequency 16:for all ํ โ ํต, ํํ(ํ ) โ 0 17: ํ โ Compute ํ Using Eq. (2) 18: ํ โฒ ํ 0 โ Reachability-LP(ํ ํ ,ํ โฅ1โํ (โฆ(ํตโชํ )) ) 19: if ํ โฒ ํ 0 < 1โ ํ then// unbreakable with ํ too 20:return (โฎ,โฎ) 21: end if 22: for ํ โ ํ do 23:ํํ(ํ) โ MinMeanPayoff(ํ ) 24: end for 25: ํ ํ ํ โ ComputeWeightedQuotientMDP(ํ ํ ,ํ , ํํ ) 26: ํ + โ NewTerminalState(ํ ํ ํ ) 27: EB ํน โ SSP-LP(ํ ํ ํ ,ํตโชํ + , 1โ ํ) 28: return (ํ,EB ํน ) 29: end if Figure 7: The weighted MEC quotient of the MDP in Fig- ure 6(a) and functionํ= ห ํด โ 4 10 , ห ํต โ 5 10 , ห ํถ โ 10 10 .ํ ํกํํฆ action labels omitted for readability. The new cost function is defined asํถ ํ ( ห ํ ํ ,ํ ํกํํฆ)= ํํ(ํ ํ ,ํ ํ ) for all ห ํ ํ โ ํํธํถ ห ํ and 0 otherwise. Hereํํ(ํ ํ ,ํ ํ )is the minimum mean payoff of the MEC(ํ ํ ,ํ ํ ). Lemma 7. The minimum expected cost of reachingํตโชํ + in the weighted MEC quotientํ ํ is equal to the minimum mean payoff of violating ํ in the MDP ํ. Proof.Correctness of this lemma follows from the correctness of the transformation in [2]. We can show that for every strategy ํ ํ inํ ํ and strategies for MECsํ ํ ํ , there is a strategyํinํ that has the mean payoff equal to the expected cost of reaching ํตโชํ + inํ ํ . Using this equivalence, we can take minimum over all strategiesํ โ ํ ํ that gives us the expected frequency breaking point. โก B.3 Computing the Expected Breaking Point (Section 4.1) Theorem 1. Given an SGDG, objectiveํ, Player 1 strategyํ, and pair of values(ํก, ํ), deciding whetherEB G,ํ (ํ) โฅ (ํก, ํ) is in P. Proof.Safety: The algorithm terminates because all the steps terminate and there are no infinite loops present. For the correctness of this case, we need to show that if the maximum probability of reachingํตis<1โ ํ, it is not breakable and if it isโฅ1โ ํ, the breaking point is finite and equal to the solution of SSP. โข Case 1:ํ ํ 0 โฅ 1โ ํ In this case, the expected cost to reachํตwithโฅ1โ ํprob- ability becomes finite. Minimum expected cost here can be computed using the SSP for MDPํ ํ for the statesํตgiv- ing us the transient breaking point ofํ. Since the transient breaking point is finite, the frequency breaking point auto- matically becomes 0. โข Case 2:ํ ํ 0 < 1โ ํ Note that in this case, it is not even possible for Player 2 to reachํตwith the required probability, therefore the strategy is not breakable and the set of strategiesํ ํ is empty. Reachability: Here too, the algorithm terminates because all the steps terminate and there are no infinite loops present. We first compute the set of winning statesํตfor Player 2 using Eq. (1). Note that Player 1 cannot reach ํบ once the play reaches ํต. โข Case 1:ํ ํ 0 โฅ 1โ ํ If the probability of reachingํตisโฅ1โ ํ, the expected cost to reachํตwithโฅ1โํprobability becomes finite. Minimum expected cost here can be computed using the SSP for MDP ํ ํ for the statesํตgiving us the transient breaking point of ํ. Since the transient breaking point is finite, the frequency breaking point automatically becomes 0. โข Case 2:ํ ํ 0 < 1โ ํ The probability of eventually reaching an end component is always 1. ํ(โฆ(ํบ โช ํตโช ํ ))= 1 ํ(โฆํบ)+ ํ(โฆ(ํตโช ํ ))= 1 1โ ํ(โฆํบ)= ํ(โฆ(ํตโช ํ )) ํ(โกยฌํบ)= ํ(โฆ(ํตโช ํ )) If the probability of reachingํ โชํตis<1โํ, it means that no strategy would violateํand thereforeํ ํ =โ . The algorithm correctly returnsโฎ,โฎin this case. If it isโฅ1โ ํ, we need to compute the frequency breaking point which is equivalent to the minimum expected mean payoff. For a play to stay forever in a MEC, the minimum frequency of disturbances must be equal to the minimum mean payoff of that MEC. Using Lemma 7, we can compute the minimum expected mean payoff of violatingํin the MDPํ ํ by computing the SSP for the weighted MEC quotient ํ ํ ํ .โก B.4 Optimal Strategy: Expected Breaking Point (Section 4.2) B.4.1 Transformation of SGD to SG. We start by defining transfor- mation of SGD to an SG as shown in Fig. 4. The SG is defined as ฬ G=( ฬ ํ, ฬ ํ 1 , ฬ ํ 2 , ฬ ํด, ฬ ํดํฃ, ฬ ํ) where โข ฬ ํ 1 = ํ 1 , โข ฬ ํ 2 = ํ 2 โช(ํ ,ํ) | ํ โ ํ 1 ,ํ โ ํดํฃ(ํ ), โข ฬ ํ= ฬ ํ 1 โช ฬ ํ 2 , โข ฬ ํด= ํดโชโฅ, โข ฬ ํดํฃ is defined as ( ฬ ํดํฃ(ํ )= ํดํฃ(ํ )ํ โ ํ ฬ ํดํฃ((ํ ,ํ))=โฅ,ํ ํ โ ํ 1 ,ํ โ ํดํฃ(ํ ) โข ฬ ํ is defined as ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃณ ฬ ํ(ํ ,ํ)=ํ(ํ ,ํ)ํ โ ํ 2 ,ํ โ ํดํฃ(ํ ) ฬ ํ(ํ ,ํ,(ํ ,ํ))= 1ํ โ ํ 1 ,ํ โ ํดํฃ(ํ ) ฬ ํ((ํ ,ํ),โฅ,ํ โฒ )=ํ(ํ ,ํ,ํ โฒ ) ํ โ ํ 1 ,ํ โ ํดํฃ(ํ ),ํ โฒ โ ํ ฬ ํ((ํ ,ํ),ํ,ํ โฒ )=ํ(ํ ,ํ,ํ โฒ ) ํ โ ํ 1 ,ํ โ ํดํฃ ํท (ํ ),ํ โฒ โ ํ Lemma 8. There exist bijective functionsํandํwhereํmaps triplets(ํ,ํ,ํฟ)of strategies inGto pairs( ฬ ํ, ฬ ํ)of strategies in ฬ G, and ํ maps paths ํ inG to paths ฬ ํ in ฬ G, such that โํ โ (ํร ํด) โ ร ํ, P ํ,ํ,ํฟ G,ํ 0 (ํ)= P ฬ ํ, ฬ ํ ฬ G,ํ 0 ( ฬ ํ) Proof. We define a bijectionํthat maps a runํinGto a run ฬ ํ in ฬ G. We construct ฬ ํ by using the following rules for all ํ โฅ 0: โข If ํ ํ โ ํ 1 and ํ ํ โ ํดํฃ(ํ ํ ): replace ํ ํ ,ํ ํ by ํ ํ ,ํ ํ ,(ํ ํ ,ํ ํ ),โฅ โข If ํ ํ โ ํ 1 and ํ ํ โ ํดํฃ ํท (ํ ํ ): replace ํ ํ ,ํ ํ by ํ ํ ,ํ ํ ,(ํ ํ ,ํ ํ ),ํ Note that this is a bijection, because every run in ฬ G can be mapped back to a run inGby simply removing the additional states(ํ ํ ,ํ ํ ) and their following actions. Forward direction: For given ํ,ํ,ํฟ inG, we construct equiv- alent strategies ฬ ํ, ฬ ํfor ฬ Gunder which every path has the same probability. For some historyํคinG, let ฬ ํคbe the corresponding history in ฬ G. ฬ ํ( ฬ ํค ยท ํ ) := ํ(ํค ยท ํ ) for ํ โ ฬ ํ 1 . ฬ ํ is defined as ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃณ ฬ ํ( ฬ ํค ยท ํ )= ํ(ํค ยท ํ ) ํ โ ํ 2 ฬ ํ( ฬ ํค ยท(ํ ,ํ))=ํ ํ โ ํ 1 ,ํ โ ํดํฃ(ํ ),ํฟ(ํค ยท ํ )โ โฅ ฬ ํ( ฬ ํค ยท(ํ ,ํ))=โฅ ํ โ ํ 1 ,ํ โ ํดํฃ(ํ ),ํฟ(ํค ยท ํ )=โฅ Note that the probability of any path under these strategies is the same. Backward direction: Given a pair of strategies ฬ ํ, ฬ ํin ฬ G , we construct equivalent strategiesํ,ํforGunder which every path has the same probability. For some history ฬ ํค in ฬ G, letํคbe the corresponding history inG. ํ(ํค ยท ํ ) := ฬ ํ( ฬ ํค ยท ํ ) for ํ โ ํ 1 . ํ(ํค ยท ํ ) := ฬ ํ( ฬ ํค ยท ํ ) for ํ โ ํ 2 . ํฟ(ํค ยท ํ ) := ( โฅํ โ ํ 1 ,ํ= ํ(ํ ), ฬ ํ( ฬ ํค ยท(ํ ,ํ)=โฅ) ฬ ํ( ฬ ํค ยท(ํ ,ํ)) ํ โ ํ 1 ,ํ= ํ(ํ ), ฬ ํ( ฬ ํค ยท(ํ ,ํ)=ํ) Note that the prob- ability of any path under these strategies is the same and that these two constructions are inverses of each other proving that a bijection exists. โก This gives us the following corollary. Corollary 4. For any set of statesํด, and strategiesํ,ํ,ํฟ,P ํ,ํ,ํฟ G,ํ 0 (โฆํด)= P ฬ ํ, ฬ ํ ฬ G,ํ 0 (โฆํด). This immediately gives us the following lemma. Lemma 4. Given an SGDG, objectiveํand memoryless Player 1 strategyํ, it holds thatEB ํ G,ํ (ํ)= inf ํโํ ํ TR( ฬ G ํ,ํ ,ํ 0 ,ํถ)and EB ํน G,ํ (ํ)= inf ํโํ ํ MP( ฬ G ํ,ํ ,ํ 0 ,ํถ). Algorithm 2 Compute Optimal Strategy w.r.t Expected Breaking Point 1: Input:G,ํ 2: Output:EB G,ํ 3: ฬ G โ ExpectedSG(G) 4: if ํ= ํ >ํ (โกยฌํต) then// Safety 5: ํต โ Input from ํ 6: else if ํ= ํ >ํ (โฆํบ) then// Reachability 7: ํต โ Compute Player 2 winning states 8: end if 9: ํ ํ โ ReachabilityQP(ํ ํ ,ํ โฅ1โํ (โฆํต)) 10: if ํ ํ < 1โ ํ then// breaking not possible 11: return(โฎ,โฎ) 12: else 13: ํป โโ 14: ํ โ MEC( ฬ Gโฉ ํต) 15: for ํง โ ํ do 16:ํํ(ํง) โ MinMeanPayoff(ํง) 17:if ํํ(ํง)= 0 then 18:ํป โ ํป โชํง 19:end if 20: end for 21: ํ ํป ํ โ ReachabilityQP(ํ ํ ,ํ โฅ1โํ (โฆํป)) 22: if ํ ํป ํ โฅ 1โ ํ then // breaking with finitely many steps possible 23: EB ํ โ SSP-SG( ฬ G,ํป, 1โ ํ) 24:return(EB ํ , 0) 25: end if 26: ฬ G ํ โ ComputeWeightedQuotientSG( ฬ G, ํํ ) 27: ํ + โ NewTerminalState( ฬ G ํ ) 28: EB ํน โ SSP-SG( ฬ G ํ ,ํ + , 1โ ํ) 29: return(ํ,EB ํน ) 30: end if B.4.2 Algorithm to Synthesize Optimal Strategies w.r.t Expected Breaking Point and its Correctness. Theorem 2. Given an SGDG, objectiveํ, and pair of values(ํก, ํ), deciding whetherEB G,ํ โฅ (ํก, ํ) is as hard as solving SSP for SGs. Proof.Termination of Algorithm 2 is guaranteed because all the steps terminate and there are no infinite loops present. To prove correctness of Algorithm 2, we analyze the two cases of safety and reachability separately. Safety: Based on the probability of reachingํตthere are two cases. โข Case 1:ํ ํ 0 โฅ 1โ ํ In this case, the expected cost to reachํตwithโฅ1โ ํprob- ability becomes finite. To compute the minimum expected cost to reachํต, we use the SSP for SG ฬ Gfor statesํต. The algorithms suggested in [22], namely, VI and PI only con- verge in the limit to the true value. Therefore, we can only compute an approximation of the transient breaking point. However, since the expected cost is finite, we can compute the frequency breaking point as 0. Note that as better meth- ods become available to solve the SSP problem, we can use those methods to compute the transient breaking point. โข Case 2:ํ ํ 0 < 1โ ํ Note that in this case, it is not even possible for Player 2 to reachํตwith the required probability, therefore the set of strategiesํ ํ is empty for allํ. Hence, it is not breakable and the algorithm correctly returns(โฎ,โฎ). Reachability: In this case, first we compute the winning statesํธ for Player 2 using the backward fix-point computation. Because of the construction, note that, Player 2 can always force the play to avoidํบonce it reachesํธ. Also, since plays reach an end component with probability 1, we know that it either reachesํบ,ํธor some other end component. If it reaches some other end component, Player 1 would never play actions to keep it there, therefore, only Player 2 would have the option to keep the play inside it if possible. But by construction, this end component would be in the setํธ. Therefore, all plays would either reachํบorํธwith probability 1 under optimal strategies for both players. Now, based on the maximum probability of reaching ํธ there are two cases. โข Case 1:ํ ํ 0 < 1โ ํ In this case, it is not possible to reachํธwith the required probability in ฬ Gwhich means that even with as many dis- turbances actions as possible, the strategy is not breakable. Hence, the set of strategiesํ ํ is empty for allํ. The algo- rithm correctly returns(โฎ,โฎ). โข Case 2:ํ ํ 0 โฅ 1โ ํ If the probability of reachingํธisโฅ1โ ํ, we compute the setํตwhere the mean payoff is 0, i.e. the frequency of disturbances required is 0 in those MECs. If the probability of reachingํตisโฅ1โ ํ, the expected cost to reachํตwithโฅ1โํprobability becomes finite since after reachingํต, no disturbances are required and the expected disturbances to reachํตwould be finite. The minimum ex- pected cost can be computed using SSP algorithm for the SG ฬ Gfor statesํตgiving us the optimal transient breaking point. The frequency breaking point would be 0 in this case. If the probability to reachํตis<1โ ํ, we need to find the right MECs to stay in. For this, the weighted MEC quotient MDP has cost associated with each MEC (transition to a new terminal state) equal to its mean payoff. Therefore, the minimum mean payoff to avoidํบis equal to the minimum mean payoff to reachํธwithโฅ1โ ํprobability. The mini- mum mean payoff can be computed using SSP algorithm for the SG ฬ G ํ for the new terminal state, giving us the optimal frequency breaking point. The transient breaking point isํ in this case.โก Note that the solution of the SSP for SGs only provides anํ- approximation of the true value. Therefore, the computed breaking points are alsoํ-approximations of the true breaking points. How- ever, as better methods become available to solve the SSP problem for SGs, we can use those methods to compute better approxi- mations of the breaking points. Moreover, the complexity of the algorithm remains the same as that of solving the SSP for SGs. C WORST-CASE BREAKING POINT (SECTION 5) C.1 Difference between Realistic Worst-Case and Absolute Worst-Case ํ 1 ํ 2 G ํ 0.1 0.9 ํ ํ Figure 8: Disturbance frequency is 1 in the absolute worst case (always stay inํ 1 ) but it is realized with 0 probability. Here, if the actionํis always played in stateํ 1 , the steady state distribution is 10 19 and 9 19 in stateํ 1 andํ 2 respectively. This gives us the realistic worst case frequency as 10 19 . Here we show what happens if we consider the absolute worst case disturbance frequency instead of the realistic worst case. For example, see Figure 8 where the absolute worst case would give a disturbance frequency of 1 (because of paths that always stay inํ 1 after some finite time) however, a more useful information would be that the disturbance frequency is 10 19 . We call this the realistic worst case in contrast. C.2 Memory Requirements for Worst-Case Breaking Point Lemma 5. LetGbe an SGD andG โ ํ its correspondingํ-unfolded stochastic game, for someํ โ โจํโฉ. Then, for all Player 1 strategiesํ, we haveB ํ G,ํ (ํ) โค ํ if and only if sup ฬ ํ P ฬ ํ, ฬ ํ G โ ํ ,(ํ 0 ,ํ) (ยฌํ) โฅ 1โ ํ. Proof.(โ) AssumeB ํ G,ํ (ํ) โค ํ. Then, by definition of break- ing point, there exists a player 2 strategyํand aํ-disturbance strategyํฟthat breaksํ. Here,ํ-disturbance strategy means that every path under that strategy has at most ํ disturbances. Let( ฬ ํ, ฬ ํ)= ํ(ํ,ํ,ํฟ), with functionํfrom Lemma 2 then sup ฬ ํ P ฬ ํ, ฬ ํ G โ ํ ,(ํ 0 ,ํ) (ยฌํ) โฅ P ํ,ํ,ํฟ G,ํ 0 (ยฌํ) โฅ 1โ ํ. (โ) Assumesup ฬ ํ P ฬ ํ, ฬ ํ G โ ํ ,(ํ 0 ,ํ) (ยฌํ) โฅ1โ ํ. Functionํ โ1 from Lemma 2 gives us a disturbance strategyํฟinGthat breaksํusing at most ํ disturbances, that is,B ํ G,ํ (ํ) โค ํ .โก Lemma 6. Ifํis reachability, and it is not possible to break the strat- egy with finite disturbances, then the optimal disturbance strategy is memoryless. Proof.We start by showing that the optimal disturbance strat- egy that forces the run to stay inside a MEC is memoryless. Let ํ โ ,ํฟ โ be the strategies that achieves the breaking point, i.e. B ํ G,ํ (ํ) := inf n ํฅ โ [0, 1] ํ ํ,ํ โ ,ํฟ โ G,ํ 0 ํ โ ํนํํํ โคํฅ = 1 o Now, since the cost on a path is the same as number of disturbances, we can write it as = inf n ํฅ โ [0, 1] ํ ํ,ํ โ ,ํฟ โ G,ํ 0 ํ โ ํํ โคํฅ = 1 o Where ํํ โคํฅ is the set of paths with mean payoffโค ํฅ . Letํbe the minimum expected mean payoff. The worst case will always be greater than the expected value. B ํ G,ํ (ํ) โฅ ํ Letํis achieved by a memoryless strategyํ โ . Using Lemma, we can find equivalent ํ โ ,ํฟ โ that achieves ํ. Now, ํ ํ,ํ โ ,ํฟ โ G,ํ 0 ํํ(ํ)= ํ = 1 ํ ํ,ํ โ ,ํฟ โ G,ํ 0 ํ โ ํํ โคํ = 1 This gives us that B ํ G,ํ (ํ) โค ํ We now show that since almost all runs reach an end component, the optimal strategy is to choose the right MECs where you always stay and maximize the probability of reaching those MECs. Letโs assume our algorithm returnsํฅas the breaking point and ํถ โ be the set of end components that have frequencyโค ํฅ. This implies all the remaining MECs inํถ\ํถ โ have frequencyโฅ ํฅ. It also means that the algorithm produces a value that can be achieved, i.e. ํํขํกํํขํก โฅB ํ G,ํ (ํ). โก C.3 Computing the Worst-Case Breaking Point (Section 5.1) Algorithm 3 Worst-case Breaking Point of a Strategy 1: Input: G,ํ,ํ 2: Output: (B ํ G,ํ ,B ํน G,ํ ) 3: ํ ํ โ InducedMDP(G,ํ ) 4: if ํ= ํ >ํ (โกยฌํต) then// Safety 5: ํต โ Input from ํ 6: else if ํ= ํ >ํ (โฆํบ) then// Reachability 7: ํต โ Compute Using Eq. (1) 8: end if 9: ํ ํ โ UseReachabilityLP(ํ ํ ,ํต, 1โ ํ)// Eq. (??) 10: if ํ ํ 0 > 1โ ํ then// Case 1 11: ํ โ ComputeUpperBoundTransient(ํ ํ ,ํต, 1โ ํ) 12: B ํ = ComputeTransient(ํ ํ ,ํต, 1โ ํ,ํ ) 13: B ํน = 0 14: else if ํ ํ 0 = 1โ ํ then 15: B ํ = ComputeTransient(ํ ํ ,ํต, 1โ ํ,|ํ ํท |) 16: if B ํ โ โ then// Case 2(a) 17:return (B ํ , 0) 18: else// Case 2(b) 19:return (ํ, 0) 20: end if 21: else// Case 3 22: if ํ= ํ >ํ (โกยฌํต) then// Safety=โ Not breakable 23:return (โฎ,โฎ) 24: else 25:ํถ โ MEC(ํ ํ )\(ํบ โช ํต)// Other MECs 26:ํ โฒ ํ โ UseReachabilityLP(ํ ํ ,ํถโช ํต, 1โ ํ) 27:if ํ โฒ ํ 0 โฅ 1โ ํ then// Need infinite disturbances 28:B ํน โ ComputeFrequency(ํ ํ ,ํบ,ํต, 1โ ํ) 29:return (ํ,B ํน ) 30:end if 31: end if 32: end if 33: return (B ํ ,B ํน ) We first prove that ifํis reachability and it is possible to break the strategy in finitely many disturbances, then we still need to solve reachability for the set ํต (as computed in Equation (1)), i.e. Lemma 9. Ifํis reachability andํis breakable with finite distur- bances then there exists ํ such that P ํ ํ ํ ,ํ 0 (โกยฌํบ)= P ํ ํ ํ ,ํ 0 (โฆํต). Proof.We compute the setํตusing Eq. (1) and we know that ํบis not reachable fromํต. Therefore, the probability of staying out ofํบis equal to the probability of reachingํตor the probability of reaching some other end component where the play can stay forever. Under any strategy, the probability of reaching a MEC and staying there is 1 [25], ํ ํ ํ ํ ,ํ 0 (โฆํบ โจ โฆํ โจ โฆํต)=1 Sinceํบandํตare sink states/end components. We also compute the setํ using Equation (2). From the definition ofํ , you need infinitely many disturbances to stay inํ , this implies P ํ,ํฟ ํ ํ ,ํ 0 (โฆํ )=0. Also, since Player 1 would never want to stay inํ \ ํ , it will take the exit action whenever the play reaches ํ \ ํ . This mean that the probability of staying forever inํ \ ํ is 0. Therefore,P ํ,ํฟ ํ ํ ,ํ 0 (โฆํบ)= 1โ ํ ํ,ํฟ ํ ํ ,ํ 0 (โฆํต) . Also, by definition, P ํ,ํฟ ํ ํ ,ํ 0 (โฆํบ)= 1โ ํ ํ,ํฟ ํ ํ ,ํ 0 (โกยฌํบ).โก We now discuss whenํ ํ 0 =1โํand we need to split it into two cases because it could either mean that this probability is reached only in the limit after infinitely many disturbances, or after a finite number of disturbances. For the following, we assume thatํ ํ (ํ )denotes the probability to reachํตwithํdisturbances from stateํ and arbitrarily many from all other states. Lemma 10. If the probability of reachingํตis exactly 1โ ํthen for all ํ> 0 it holds thatํ ํ+1 (ํ )> ํ ํ (ํ ) impliesํ ํ+2 (ํ )> ํ ํ+1 (ํ ). Proof.Letํbe a disturbance action in stateํ and letํbe the probability mass of coming back to stateํ after pickingํ. Ifํ=0, thenํ ํ+1 (ํ )=ํ ํ (ํ ), a contradiction. Thus,ํ>0, which means that there is a pathํ= ํ ,ํ, . . .,ํ (starting and ending inํ ) with probability massํ. Letํฟ โฒ (ํ ,ํ +2)= ํ, and followํafterwards. Then,ํ ํ+2 (ํ ) โฅ ํ ํฟ โฒ (ํ )> ํ ํ+1 (ํ ).โก Lemma 11. Ifํ ํ 0 =1โ ํ, then there is a disturbance strategyํฟ and a natural numberํ โ โจํโฉsuch thatํฟbreaksํwith at mostํ disturbances if and only if there is a disturbance strategy that breaks ํ using each disturbance edge at most once. Proof. (โ) This is immediate. (โ) Assume thatํฟbreaksํusingํ โ โจํโฉdisturbances, and assume that there is a disturbance edgeํ โ ํ ํท that is takenํ>1 times. There are two cases: โข Caseํ ํ โค ํ ํโ1 . Then, define ํฟ โฒ to never take ํ . โขCaseํ ํ > ํ ํโ1 . Then,ํ ํ+1 > ํ ํ by Lemma 10, meaning that there exists a disturbance strategy that achievesํ ํ 0 > ํ by using ํ+ 1 disturbances, a contradiction. โก These lemmas tell us that ifํcannot be broken using|ํ ํท |dis- turbances then it cannot be broken with finitely many disturbances. We are now ready to prove the correctness of our algorithm. Theorem 3. Given an SGDG, objectiveํ, Player 1 strategyํ, and pair of values(ํก, ํ), deciding ifB G,ํ (ํ) โฅ (ํก, ํ) is in PSPACE. Proof.We prove the correctness of Algorithm 3, which runs in PSPACE. Since reachability is reduced to safety, we just argue in terms of probability of reaching the set ํต. We have four cases: Case 1:ํ ํ 0 > 1โ ํ Letํ 0 ํ 0 ,ํ 1 ํ 0 , . . .is the sequence of values produced by value iteration. It is a non-decreasing sequence that converges to the true value ํฃ ํ 0 >1โ ํin the limit (by correctness of value iteration). There existํ โ Nsuch thatํ ํ ํ 0 >1โ ํ. This value iteration uptoํsteps would also give a strategyํฟ:( ฬ ํร ฬ ํด) โ ร ฬ ํ โ ฬ ํดthat defines which action to take from every state after each time step. Thisํฟbreaks ํ inโค ํ steps, therefore, ํ is an upper bound. We give this upper bound to the procedure to compute tran- sient breaking point and for its correctness, we refer to the next subsection. Case 2:ํ ํ 0 = 1โ ํ. As we check for the transient breaking point up until the number of disturbances|ํ ํท |, we have two subcases. โขIt breaks within|ํ ํท |disturbances, and the transient break- ing point is already computed. We leave the correctness of computing the transient breaking point to be shown later in Lemma 12. In this case, the frequency is 0 by definition. โขIf it does not break within|ํ ํท |disturbances, we know that it is not possible to break it with finitely many disturbances using Lemma 11. To show correctness of computing the frequency in this case, we refer to Lemma 15. Case 3:ํ ํ 0 < 1โ ํ If the specification is safety, the probability to reachํตis<1โ ํ and therefore it would never be possible to break it and therefore the breaking point is(โฎ,โฎ). If the specification is reachability, we compute the set of MECs ํ that are notํตorํบ. Here, it is possible that some runs stay inํ and some runs stay inํตto avoid reachingํบ. Here, the amount of disturbances required is infinite since if it was finite, the runs would reach a state from which no more disturbances are required with probabilityโฅ1โํ, since this is also the definition ofํต, probability to reach ํต would beโฅ 1โ ํ, a contradiction.โก C.4 Algorithm for Computing Worst-Case Transient Breaking Point and its Correctness min โ๏ธ ํ โํ ํ ํ ,0 ํ ํ ,0 = 1 โํ โ ํต ํ ํ ,0 โฅ 0 โํ โ ํ ํ ํ ,0 โฅ โ๏ธ ํ โฒ โํ ฬ ํ(ํ ,ํ,ํ โฒ )ํ ํ โฒ ,0 โํ= ํ(ํ ) (11) min โ๏ธ ํ โํ ํ ํ ,ํ ํ ํ ,ํ = 1 โํ โ ํต ํ ํ ,ํ โฅ 0 โํ โ ํ ํ ํ ,ํ โฅ โ๏ธ ํ โฒ โํ ฬ ํ(ํ ,ํ,ํ โฒ )ํ ํ โฒ ,ํ โํ= ํ(ํ ) ํ ํ ,ํ โฅ โ๏ธ ํ โฒ โํ ฬ ํ(ํ ,ํ,ํ โฒ )ํ ํ โฒ ,ํโ1 โํ โ ํดํฃ(ํ )\ ํ(ํ ) (12) Algorithm 4 Compute Transient Breaking Point 1: Given ํ ํ ,ํต,ํ 2: ํ ํ ,0 โ LP 0 (ํ ํ ,ํต)// Using Eq. (11) 3: ํ= 0 4: while ํ โค ํ do 5: ํ ํ ,ํ+1 โ LP ํ+1 (ํ ํ ,ํต,ํ ํ ,ํ )// Using Eq. (12) 6: if ํ ํ ,ํ+1 โฅ 1โ ํ then 7:return i+1// breaking point is ํ+ 1 8: end if 9: ํ++ 10: end while 11: returnโ// transient breaking point is not smaller than ํ Lemma 12. Algorithm 4 terminates and returnsB ํ G,ํ ifB ํ G,ํ โค ํ. Proof.We first prove decidingํ-resilience (transient) in SGD would be the same as solving the unfolding of the MDP obtained by treating Player 1 states as Player 2 states (see Lemma 13). This requires evaluating the system under all possibleํ-disturbance strategies of Player 2. Second, we show solving this unfolding is same as solving the iterative LP (see Lemma 14). โก C.4.1 Construction of Unfolding of an MDP. We reduce the prob- lem of finding breaking point of strategy to solving an unfolded MDP. In this section, we explain the construction of the unfolded MDP incorporating disturbances. To analyze the resilience of the strategyํ, we define the unfolded MDP as an extension of the MDPํ ํ . The unfolded MDP introduces a disturbance counter that tracks the number of disturbances applied. Moreover, no distur- bance actions can be chosen when the counter reaches its maximum number of allowed disturbances ํ . We define the unfolded MDP asํ โ ํ =(ํ โ ,ํด โ , Av โ ,ํ โ ), where: โข ํ โ = ํร0, . . .,ํ is the augmented state space, where: โ ํ= ํ 1 โช ํ 2 is the state space of ํ ํ , โ ํ โ 0, . . .,ํis the disturbance counter, representing the number of disturbances applied so far. โข ํด โ = ํด= ํดโช ํด ํท is the action space, unchanged from ํ ํ . โข ํดํฃ โ ((ํ ,ํ))= ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃณ ํ(ํ )โช ํดํฃ ํท (ํ ),if ํ โ ํ 1 and ํ< ํ, ํ(ํ ),if ํ โ ํ 1 and ํ= ํ, ํดํฃ(ํ ),if ํ โ ํ 2 . โข ํ โ ((ํ ,ํ),ํ,(ํ โฒ ,ํ โฒ )) = ๏ฃฑ ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด๏ฃฒ ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃด ๏ฃณ ํ(ํ ,ํ,ํ โฒ ) ยท ํฟ ํ (ํ โฒ =ํ),if ํ โ ํ 1 ,ํ= ํ(ํ ), ํ ํท (ํ ,ํ,ํ โฒ ) ยท ํฟ ํ (ํ โฒ =ํ+ 1),if ํ โ ํ 1 ,ํ โ ํดํฃ ํท (ํ ) and ํ< ํ, 0,if ํ โ ํ 1 ,ํ โ ํดํฃ ํท (ํ ) and ํ=ํ, ํ(ํ ,ํ,ํ โฒ ) ยท ํฟ ํ (ํ โฒ =ํ),if ํ โ ํ 2 ,ํ โ ํดํฃ(ํ ). One can solve this unfolded MDP to get the transient breaking point of ํ if it is smaller than ํ . LP for unfolded MDP.. Now the LP to solve the unfolding MDP can be give as follows. min โ๏ธ (ํ ,ํ)โํ โ Val (ํ ,ํ) subject to: Val (ํ ,ํ) = 1,for all(ํ ,ํ) โ ํต โ ; Val (ํ ,ํ) โฅ 0,for all(ํ ,ํ) โ ํ โ ; Val (ํ ,ํ) โฅ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ(ํ ),ํ โฒ )Val (ํ โฒ ,ํ) , โ(ํ ,ํ) โ ํ โ ,ํ โ ํ 1 ; Val (ํ ,ํ) โฅ โ๏ธ ํ โฒ โํ ํ ํท (ํ ,ํ,ํ โฒ )Val (ํ โฒ ,ํโ1) , โ(ํ ,ํ) โ ํ โ ,ํ โ ํดํฃ ํท (ํ ), 1< ํ โค ํ ; Val (ํ ,ํ) โฅ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ(ํ ),ํ โฒ )Val (ํ โฒ ,ํ) , โ(ํ ,ํ) โ ํ โ ,ํ โ ํ 1 ; Val (ํ ,ํ) โฅ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ,ํ โฒ )Val (ํ โฒ ,ํ) , โ(ํ ,ํ) โ ํ โ ,ํ โ ํดํฃ(ํ ),ํ โ ํ 2 . (13) Lemma 13. Given a set of statesํต โ ํ, a strategy with memory ํ : ํร0, . . .,ํโ ํด for the MDP ํ ํ , there exists a strategy ํ โ for the unfolded MDP ํ โ ํ such that: ํ ํ,ํฟ ํ ํ ,(ํ 0 ,0) (โฆํต)= ํ ํ โ ํ โ ํ ,(ํ 0 ,0) (โฆํต โ ), Here,ํต โ =(ํ ,ํ) | ํ โ ํต,ํ โ 0, . . .,ํis the corresponding set of target states in the unfolded MDP. Proof.We aim to show that for a given strategy in one MDP, we can construct a strategy in the other MDP that ensures equivalent probabilities of reaching the target set of states. Constructing a strategy in the unfolded MDP. Letํ:ํร0, . . .,ํโ ํด be the memory-based strategy for Player 1 in ํ ํ . We construct a corresponding strategyํ โ for the unfolded MDPํ โ ํ as follows: โข For each state(ํ ,ํ) โ ํ โ , define ํ โ ((ํ ,ํ))= ํ(ํ ,ํ). This strategy ensures that the decisions made in the unfolded MDP align with those in the original MDP under the strategy ํ. Reaching the target setํต. Suppose there exists a strategyํinํ ํ such that the probability of reachingํต โ ํfrom(ํ 0 ,0)isํ. That is, ํ ํ,ํฟ ํ ํ ,(ํ 0 ,0) (โฆํต)= ํ. We claim that under the constructed strategyํ โ , the same prob- abilityํis achieved in the unfolded MDP for reaching the corre- sponding target set ํต โ . Specifically, ํ ํ โ ํ โ ํ ,(ํ 0 ,0) (โฆํต โ )= ํ. The equivalence follows from the fact that the dynamics of the unfolded MDP are designed to mirror the augmented state space of the original MDP. In particular: โขThe states inํ โ correspond exactly to the augmented states ํร0, . . .,ํ of ํ ํ . โขThe transitions inํ โ ํ underํ โ are equivalent to the transi- tions in ํ ํ under ํ. โขThe target setํต โ corresponds directly toํตin the original MDP, extended with all memory labels ํ โ 0, . . .,ํ. Since the strategyํ โ replicates the decisions ofํand the structure ofํ โ ํ mirrors the augmented state space ofํ ํ , the probability of reachingํต โ inํ โ ํ underํ โ matches the probability of reachingํต in ํ ํ under ํ. Constructing a strategy in the original MDP.. Conversely, suppose there exists a strategyํ โ inํ โ ํ that ensures a probabilityํof reaching ํต โ from(ํ 0 , 0). That is, ํ ํ โ ํ โ ํ ,(ํ 0 ,0) (โฆํต โ )= ํ. We can construct a corresponding strategy ํ in ํ ํ by defining: โข ํ(ํ ,ํ)= ํ โ ((ํ ,ํ)) for all(ํ ,ํ) โ ํ โ . By similar reasoning, this strategyํensures that the probability of reachingํตinํ ํ matches the probability of reachingํต โ inํ โ ํ under ํ โ .โก Lemma 14. Solving the incremental LP is equivalent to solving the unfolded MDP. Proof.We prove, by induction onํ, that the minimized sum of the objective in the incremental LP in Eq.(12)coincides with the minimized sum in the unfolded MDPโs LP in Eq.(13). Specifically, we aim to show: min โ๏ธ ํ โํ ํ ํ ,ํ = min โ๏ธ (ํ ,ํ)โํ โ Val (ํ ,ํ) . Base Case. For ํ= 0, the incremental LP (Eq. (11)) minimizes: โ๏ธ ํ โํ ํ ํ ,0 ,subject to: ํ ํ ,0 = 1 for all ํ โ ํต; ํ ํ ,0 โฅ 0, ํ ํ ,0 โฅ โ๏ธ ํ โฒ โํ ฬ ํ(ํ ,ํ(ํ ),ํ โฒ )ํ ํ โฒ ,0 . The unfolded MDP LP for ํ= 0 minimizes: โ๏ธ (ํ ,0)โํ โ Val (ํ ,0) ,subject to: Val (ํ ,0) = 1 for all(ํ , 0) โ ํต โ ; Val (ํ ,0) โฅ 0, Val (ํ ,0) โฅ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ(ํ ),ํ โฒ )Val (ํ โฒ ,0) . The constraints and objective in Equation (11) and the unfolded MDP LP are identical whenํ=0, as both minimize the sum over the same state values under the same set of constraints. Therefore: min โ๏ธ ํ โํ ํ ํ ,0 = min โ๏ธ (ํ ,0)โํ โ Val (ํ ,0) . Induction Hypothesis. Assume that forํ โฅ0, the minimized sums in the incremental LP and the unfolded MDP LP are equal: min โ๏ธ ํ โํ ํ ํ ,ํ = min โ๏ธ (ํ ,ํ)โํ โ ,ํโคํ Val (ํ ,ํ) . Inductive Step. We now prove that the equivalence holds forํ+1. The incremental LP for ํ+ 1 minimizes: โ๏ธ ํ โํ ํ ํ ,ํ+1 ,subject to: ํ ํ ,ํ+1 = 1 for all ํ โ ํต, ํ ํ ,ํ+1 โฅ 0, ํ ํ ,ํ+1 โฅ โ๏ธ ํ โฒ โํ ฬ ํ(ํ ,ํ(ํ ),ํ โฒ )ํ ํ โฒ ,ํ+1 , ํ ํ ,ํ+1 โฅ โ๏ธ ํ โฒ โํ ฬ ํ(ํ ,ํ,ํ โฒ )ํ ํ โฒ ,ํ ,for all ํ โ ํดํฃ(ํ )\ ํ(ํ ). The unfolded MDP LP for ํ+ 1 minimizes: โ๏ธ (ํ ,ํ)โํ โ ,ํโคํ+1 Val (ํ ,ํ) ,subject to: Val (ํ ,ํ) = 1 for all(ํ ,ํ) โ ํต โ , Val (ํ ,ํ) โฅ 0, Val (ํ ,ํ+1) โฅ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ(ํ ),ํ โฒ )Val (ํ โฒ ,ํ+1) , Val (ํ ,ํ+1) โฅ โ๏ธ ํ โฒ โํ ํ ํท (ํ ,ํ,ํ โฒ )Val (ํ โฒ ,ํ) ,for all ํ โ ํดํฃ ํท (ํ ). Matching the Minimized Sums. โข Structure of the Recursion: Both the incremental LP and the unfolded MDP LP minimize over values that depend on contributions from two sources: โ Values propagated via ฬ ํ(ํ ,ํ(ํ ),ํ โฒ ) (Player 1โs strategy). โ Values propagated via ฬ ํ(ํ ,ํ,ํ โฒ )orํ ํท (ํ ,ํ,ํ โฒ )(Player 2โs disturbances). These contributions are identical in both LPs, with the un- folded MDP LP explicitly encoding the disturbance levelํ, and the incremental LP aggregating these contributions. โข By the inductive hypothesis: min โ๏ธ ํ โํ ํ ํ ,ํ = min โ๏ธ (ํ ,ํ)โํ โ ,ํโคํ Val (ํ ,ํ) . Substituting this into the constraints forํ+1, we see that the constraints enforce the same balance between Player 1โs strategy and Player 2โs disturbances in both LPs. โข The additional terms forํ+1 disturbances are minimized in the same way in both formulations. Therefore: min โ๏ธ ํ โํ ํ ํ ,ํ+1 = min โ๏ธ (ํ ,ํ)โํ โ ,ํโคํ+1 Val (ํ ,ํ) .โก C.5 Algorithm for Computing Worst-Case Frequency Breaking Point and its Correctness Algorithm 5 Compute Frequency Breaking Point 1: Input: ํ ํ ,ํบ,ํต, 1โ ํ 2: for all ํ โ ํต, ํํ(ํ ) โ 0 3: ํ โ Compute ํ 4: for ํ โ ํ do 5: ํํ(ํ) โ ComputeFrequencyMEC(ํ) 6: end for 7: ํ โ ํ 8: while true do 9: ํ โ MaxFreqMEC(ํ) 10: ํ โ ํ \ํ 11: if ํ(โฆํ)< 1โ ํ then 12:return ํํ(ํ) 13: end if 14: end while Lemma 15. Algorithm 5 terminates and returnsB ํน G,ํ (ํ) in poly- nomial time. Proof. From the definition of frequency breaking point B ํ G,ํ (ํ)= inf ํ,ํฟโํ ํ n ํฅ ํ ํ,ํ,ํฟ G,ํ 0 ํ โ ํนํํํ โคํฅ = 1 o From Lemma 1, we get ํ ํ,ํ,ํฟ G,ํ 0 ํ โ ํนํํํ โคํฅ = ํ ํ,ํฟ ํ ํ ,ํ 0 ํ โ ํนํํํ โคํฅ From here onwards, we drop the sub- and superscript ofํfor ease of notation ํ ํ โ ํนํํํ โคํฅ = ํ ํ โ ํํ โคํฅ where, ํํ โคํฅ is the set of runs that have mean payoffโค ํฅ . Letํถ=ํถ 1 ,ํถ 2 , . . .ํถ ํ are the MECs ofํ ํ . Under memoryless strategiesํ,ํฟ, the probability of a path reaching a MEC and staying there forever is 1. This gives us, = ํ ํ โ ํํ โคํฅ ร ร ํ โฆํถ ํ Whereโฆํถ ํ denotes the set of runs eventually reaching the MECํถ ํ and staying there forever. Now, since all the MECs are disjoint, we get = โ๏ธ ํ ํ ํ โ ํํ โคํฅ โฉ โฆํถ ํ For someํถ ํ ,ํ ํ โ ํํ โคํฅ โฉ โฆํถ ํ > 0 only if the mean payoff of ํถ ํ isโค ํฅ . = โ๏ธ ํ ํ ํ โ โฆํถ ํ [ํํ(ํถ ํ ) โค ํฅ] where[]is the bracket notation andํํ(ํถ ํ )is the mean payoff of ํถ ํ . = ํ ํ โ โฆํถ ํ | ํํ(ํถ ํ ) โค ํฅ Since this probability should be 1 according to the definition, almost all the runs should reach only the end components that have mean payoffโค ํฅ .โก C.6 Optimal Strategy: Worst-Case Breaking Point (Section 5.2) Reachability. Initially, we also assume that the SGD has a special structure: we have three assumptions on the structure of the SGD: โข (A1.) For each state ํ โ ํ ,|ํดํฃ(ํ )|= 2. โข (A2.) For each state ํ โ ํ 1 ,|ํดํฃ ํท (ํ )|= 1. โข(A3.) For each state,for every action, with a small probability ํ, the game leads to ํต. The intuition behind it is that, with these restrictions, itsํ-unfolding will be a special type of stopping stochastic game [10], for which it is easier to formulate a QP. Note that [10] considers the probability values to be in0,0.5,1, but this restriction can be ignored without any loss of generality (as discussed in [16, Lemma 3]). We discuss how to accommodate the general case later. Iterative Quadratic Programming. In this section, for a stateํ โ ํ 1 , we denote the only disturbance action inํดํฃ ํท (ํ )asํ ํ . We define a sequence of QPs, namely(ํํ 0 ,ํํ 1 , . . .ํํ ํ ), where inํํ ํ we Algorithm 6 Compute Worst-case Transient Breaking Point 1: GivenG,ํ,ํ 2: ํ= 0 3:ํ โ QP0(G,ํ)// Eq. (16) 4: while ํ โค ํ do 5: ํ โ QP(G,ํ,ํ)// Eq. (17) 6: if ํ ํ ,ํ+1 โฅ 1โ ํ then 7:return i+1// breaking point is ํ+ 1 8: end if 9: ํ++ 10: end while 11: returnโ minimize the objective function ํน ํ w.r.t. a constraint setํถ ํ . ํน 0 = โ๏ธ ํ โํ ร ํโํดํฃ(ํ ) ํ ํ ,0 โ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ,ํ โฒ )ยทํ ํ โฒ ,0 ! (14) ํน ํ = โ๏ธ ํ โํ 1 ร ํโํดํฃ(ํ ) ํ ํ ,ํ โํ ํ ,ํ,ํ + โ๏ธ ํ โํ 2 ร ํโํดํฃ(ํ ) ํ ํ ,ํ โ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ,ํ โฒ )ยทํ ํ โฒ ,ํ ! + โ๏ธ ํ โํ 1 โ๏ธ ํโํดํฃ(ํ ) ํ ํ ,ํ,ํ โ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ,ํ โฒ )ยทํ ํ โฒ ,ํ ! ยท ํ ํ ,ํ,ํ โ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ ํ ,ํ โฒ )ยทํ ํ โฒ ,ํโ1 ! (15) minํน 0 subject to: ํ ํ ,0 = 1 โํ โ ํบ ; ํ ํ ,0 = 0 โํ โ ํต; ํ ํ ,0 โฅ โ๏ธ ํ โฒ โํ ํ(ํ ,ํ,ํ โฒ ) ยทํ ํ โฒ ,0 โํ โ ํ 1 ,ํ โ ํดํฃ(ํ ) ; ํ ํ ,0 โค โ๏ธ ํ โฒ โํ ํ(ํ ,ํ,ํ โฒ ) ยทํ ํ โฒ ,0 โํ โ ํ 2 ,ํ โ ํดํฃ(ํ ). (16) minํน ํ subject to: ํ ํ ,ํ = 1 โํ โ ํบ ; ํ ํ ,ํ = 0 โํ โ ํต; ํ ํ ,ํ โฅ ํ ํ ,ํ,ํ โํ โ ํ 1 ,ํ โ ํดํฃ(ํ ) ; ํ ํ ,ํ,ํ โค โ๏ธ ํ โฒ โํ ํ(ํ ,ํ,ํ โฒ ) ยทํ ํ โฒ ,ํ โํ โ ํ 1 ,ํ โ ํดํฃ(ํ ) ; ํ ํ ,ํ,ํ โค โ๏ธ ํ โฒ โํ ํ(ํ ,ํ ํ ,ํ โฒ ) ยทํ ํ โฒ ,ํโ1 โํ โ ํ 1 ,ํ โ ํดํฃ(ํ ) ; ํ ํ ,ํ โค โ๏ธ ํ โฒ โํ ํ(ํ ,ํ,ํ โฒ ) ยทํ ํ โฒ ,ํ โํ โ ํ 2 ,ํ โ ํดํฃ(ํ ) ; (17) where the values ofํ ํ ,ํโ1 inํถ ํ comes from the solution ofํํ ํโ1 . For a state ํ , ํ ํ is the only disturbance action in ํดํฃ ํท (ํ ). Safety. For a stopping SG, for any pair of strategies, with proba- bility 1, eventually one of the sink state is reached. Without loss of generality, the SG has two sink statesํบandํต. Then the objective ํ= ํ โฅํ (โกยฌํต)can be converted toํ= ํ โคํ (โฆํบ). Then, for safety objective, the existence of aํ-resilient strategy can be checked by checking ifํ ํ 0 ,ํ โค ํ. Lemma 16. Algorithm 6 terminates and returnsmax ํ B ํ G,ํ ifmax ํ B ํ G,ํ โค ํ. Proof.Because of our assumptions,G โ ํ is a stopping game, i.e., i) each state has only two available actions and i) for every action, with a small probability ํ, the game leads to ํต. Using the method of solving stopping SGs [9], we can design a QP forG โ ํ (hereafter referred to asํํ โ ํ ). Note that in this QP, we will minimizeํน= ร ํ ํน ํ w.r.t.ํถ= ร ํ ํถ ํ (Forํ โ ํ, 0โค ํ โค ํ, ํ โ ํดํฃ(ํ ),ํ ํ ,ํ andํ ํ ,ํ,ํ are the variables corresponding to the states (ํ ,ํ)and(ํ ,ํ,ํ)respectively). Also, from [9],ํํ โ ํ has a unique optimal solutionํฃ. Also, for this optimal solution every summand inํนis 0, in particular,ํน ํ is 0 for allํ. In this solution the value of ํ ํ 0 ,ํ ismax ํ P ํ G โ ํ ,(ํ 0 ,ํ) (ํ) โฅ ํ. For 0โค ํ โค ํ, we defineํฃ ํ as the projection ofํฃ corresponding to the variablesํ ํ ,ํ โs andํ ํ ,ํ,ํ โs. To proof the correctness of Algorithm 6, we will show thatํฃis the unique solution of the iterativeํํ. Sinceํฃin the constraint set ํถ,ํฃ ํ is inํถ ํ . For any assignment satisfyingํถ ํ , every summand in ํน ํ is non-negative as they are products of two terms that are either both non-negative or both non-positive. Since, for the assignment ํฃ,ํน ํ =0,ํฃ ํ is indeed an optimal solution. To show the uniqueness, assume there is another solutionํขโ ํฃ, such thatํข ํ is inํถ ํ and ํน ํ =0. But thenํขis inํถfor whichํน=0, contradicting the fact that ํํ โ ํ has an unique solution.โก This proves the following: Lemma 17. Givenํ โ Nin unary, checking ifmax ํ B ํ G,ํ โค ํis in P NP . Proof.Note that the decision problem corresponding to these specific QPs defined above can be solved inNP[10], but in our case we also need to find the solution of the QP as we are using them in the next QP. This can be extracted using polynomially manyNP queries, where inํ ํกโ query we will ask whether theํ ํกโ bit of the solution is 1. Also, in each iteration, we only need to remember the solution of the last iteration. Thus, we can solve this in polynomial time with an NP oracle if ํ is given in unary.โก C.6.1 Iterative QP in the General Case. Here we will show how to generalize these restrictions: Dealing with A1 and A2. If there are more than two actions at a state, the objective functions are not quadratic, but we can make them quadratic by adding intermediary states. For example, suppose from a Player 1 stateํ , we haveํactions ํ 0 ,ํ 1 , . . .ํ ํโ1 andํdeviation actionsํ 0 ,ํ 1 , . . .ํ ํโ1 . First, from stateํ , we only allowํ 0 and have two new actions that will lead to a new intermediary stateํ 1 . Again from this stateํ 1 , we will allow ํ 1 and have two new actions that will lead to a new intermediary stateํ 2 . Once, we cover all deviation actions usingํstates, we add additional states for the actions atํ to cover the actions. Two actions are taken and given to a new vertexํ ํ+1 . Stateํ ํ has then one action leading to an additional stateํ ํ+1 instead of its previous two actions. This can be done iteratively until there is a binary tree withํ ํ the root and has only two actions. For this |ํดํฃ(ํ )|+|ํดํฃ ํท (ํ )|โ 2 more states for every state. Dealing with A3. Any arbitrary stochastic game can be converted to a polynomially larger stopping game using the construction in [27]. The idea is to add a transition with a small probabilityํ leading to a non-target sink-state for to every action. If theํis chosen sufficiently small, one can infer the value in the original SG from the modified SG [10, Lemma 8]. Theorem 4. Given an SGDG, an objectiveํ, and a pair of values (ํก, ํ), deciding whetherB G,ํ โฅ (ํก, ํ) is in PSPACE. Proof.If the probability of reachingํตisโฅ1โ ํ, then the frequency breaking point is 0 and the transient breaking point is computed using Algorithm 6 whose correctness follows from Lemma 17. If the probability of reachingํ โช ํตis<1โ ํ, then it is not possible to break the strategy because the probability to reach ํบ under any strategies is> ํ. If the probability of reachingํตis<1โ ํ, and the probability of reachingํ โช ํตisโฅ1โ ํ, then the transient breaking point is infinite since staying outside ofํบrequired staying is some other end component and just staying in end components with zero cost (ํต) is not enough. Therefore, to break the strategy Player 2 has to force the play to reach other end components and stay there. Now, staying in the end components that have minimal cost is the same as the breaking point. โก