Probably Approximately Correct Learning in Stochastic Games with Temporal Logic Specifications

1 Introduction

An important goal of reinforcement learning (RL) is to make an agent learn to behave as desired through its experience. For problems modeled as stochastic games, the expectation of the discounted sum of rewards is commonly used as a performance criterion to encode the preference over strategies. It is well known that with discounted-sum objectives, pure memoryless strategies suffice for optimality [Filar and Vrieze, 1996], which significantly simplifies the learning algorithms. However, the discounted-sum objective suffers from several noticeable drawbacks in the task of describing the desired strategies. First, it is not applicable to strategies that require memory. As memoryless strategies are sufficient to achieve optimality, agents lack the incentive to learn the more complicated finite-memory strategies. Second, it cannot restrict behavior during the learning process. With rewards, the agent can only figure out the preferable actions after it actually tries all transitions, even the fatal ones such as crashing into some obstacle, which is obviously unacceptable. Third, there is usually a lack of theoretical proof that any strategy solved with the given reward function is desirable, except in some simple scenarios. For example, multidimensional reward functions are generally necessary to rep-

Ufuk Topcu

University of Texas at Austin utopcu@utexas.edu

resent the conjunction of several requirements, in which case a strategy usually cannot be simultaneously optimized with every single reward. It is hard to know intuitively from the reward function how different the learned strategy is from a desired one.

In order to compensate for these problems, we propose to use linear temporal logic (LTL) specifications to complement the encoding of the desired strategies. Practically, it is relatively straightforward to extract LTL specifications from high-level task requirements in robot planning and control [Kress-Gazit et al., 2007; Smith et al., 2011; Guo et al., 2013; Wolff et al., 2013]. Algorithmically, all LTL formulas can be transformed to deterministic Rabin or parity automata (DRA or DPA), which can be further used to construct product stochastic Rabin or parity games. Strategies synthesized for such product Rabin or parity games are guaranteed to satisfy the corresponding LTL specifications with probability one (i.e. almost surely), treating LTL specifications as 'game rules' that should never be violated. Both the construction of DRA or DPA from LTL formulas and the synthesis can be performed using off-the-shelf tools [Gaiser et al., 2012; Tsai et al., 2013; Klein, 2015; Blahoudek, 2015; Friedmann and Lange, 2009]. Although it has been shown that pure memoryless strategies suffice for almost-sure winning in the product stochastic Rabin or parity games [Chatterjee et al., 2003; 2005a], these strategies use memory in the original stochastic games. In this way, LTL specifications offer a systematic way of designing the memory for the desired strategies. We will show later that with the pre-computation of almost-sure winning regions in the product games, we can keep the agent safe even during the learning procedure.

In this paper we use both discounted rewards and LTL specifications to encode task requirements. In particular, if an LTL specification is realizable and can be transformed into a deterministic Buchi automaton (DBA), we prove the existence of a memoryless strategy which is both almost-sure winning with respect to the Buchi objective and "-optimal with respect to the discounted-sum objective. We also propose a probably approximately correct (PAC) algorithm to learn such a strategy online when the reward function and the transition distributions are both unknown a priori [Strehl et al., 2009; Fu and Topcu, 2014]. To the best of our knowledge, this is the first PAC learning algorithm for stochastic games with independent quantitative and qualitative objectives.

Related work Strategy synthesis in which perfect knowledge of the game is available and the task involves both qualitative and quantitative objectives has been extensively studied. Examples include mean-payoff parity games [Chatterjee et al., 2005b], energy parity games [Chatterjee and Doyen, 2010], their multi-dimension version [Chatterjee et al., 2012] and stochastic version [Chatterjee et al., 2014]. There are also results on strategy synthesis in stochastic games with total reward constraints and LTL specifications [Chen et al., 2013]. However, only limited work has been done when the transition distributions and the rewards are unknown a priori. This paper is an extension of our previous work [Wen et al., 2015], in which we considered a learning problem with both temporal logic constraints and unknown discounted-sum objectives in deterministic games. Our new algorithm here works with general stochastic games and guarantees to learn a nearoptimal strategy with any specified optimality bound.

2 Preliminaries

For any countable set M, let ♣M♣ be its cardinality, M ! be the set of infinite sequences composed of elements in M, and D(M) be the set of all probability distributions over M.

We first formulate the decision-making problem as a turnbased labeled stochastic game. A turn-based labeled stochastic game between the controlled agent (the 'system') and the uncontrolled agent (the 'environment') is defined as a tuple G = (SG↪ Ss↪G↪ Se↪G↪ IG↪AG↪ TG↪RG↪AP↪ LG), where SG is a finite state space; Ss↪G ✓ SG is the set of states at which the system chooses actions, and Se↪G = SG∩Ss↪G is a set of states at which the environment chooses actions; IG ✓ SG is a set of initial states; AG is a finite action space; TG : SG ⇥AG ! D(SG) is a transition function; RG : SG⇥AG⇥SG !R≥0 is a non-negative reward function; AP is a set of atomic propositions (Boolean variables); LG : SG ! 2AP is a labeling function.

LTL specifications put restrictions on the label sequences corresponding to the infinite state sequences of G. Interested readers may refer to [Baier et al., 2008] for the detailed syntax and semantics of LTL. Instead of treating LTL specifications directly as formulas, we translate them into !-regular automata, or deterministic Buchi automata, to be precise. A deterministic Buchi automaton (DBA) is a tuple A = (QA↪⌃A↪ δA↪Q0↪A↪ FA) where QA is a finite set of states; ⌃A is a finite input alphabet; δA : QA ⇥⌃A ! QA is a transition function; Q0↪A ✓ QA is a set of initial states; FA ✓ QA is a set of accepting states. A run of A over an input sequence (pt)t2N 2 ⌃!A is an infinite sequence (qt)t2N 2 Q!A, where q0 2 Q0↪A and qt+1 = δA(qt↪ pt) for all t 2 N. A run (qt)t2N is accepted by A if ♣¶t 2 N : qt 2 FA♦♣ = 1. Only a subclass of LTL formulas can be transformed into equivalent DBAs, but this subclass of specifications covers a wide range of requirements in robot planning tasks. For example, ⇤safe region (always stay in states labeled as 'safe region'), }goal (eventually reach a state labeled as 'goal'), ⇤(request ! }response) (if a 'request' state is observed, a 'response' state should be visited later), ⇤}charging (always get to the 'charging' state sometime later), ⇤((≻charging) U battery low) (never charge yourself before the battery gets low), just to name a few.

If ⌃A = 2AP , we can compose a turn-based stochastic Buchi game G = (S↪ Ss↪ Se↪ I↪ A↪ T↪ R↪ F ) of G and A with the standard product automata construction:

• ÷ S = SG ⇥QA is a finite state space;
• ÷ Ss = Ss↪G ⇥QA is the set of system states, and Se := S∩Ss is the set of environment states;
• ÷ I = IG ⇥Q0↪A is a set of initial states;
• ÷ A = AG is a finite action space;
• ÷ T : S ⇥A ! D(S) is the transition function such that T ((s↪ q)↪ a)(s0 ↪ δA(q↪ LG(s))) = TG(s↪ a)(s0 );
• ÷ R : S⇥A⇥S ! R≥0 is a non-negative reward function such that R((s↪ q)↪ a↪ (s0 ↪ q0 )) = RG(s↪ a↪ s0 );
• ÷ F = SG ⇥ FA is a set of accepting states.

The product game G inherits the reward from G and the winning condition from A. On the reward side, the system is to maximize its future discounted reward, while the environment is to minimize it. On the winning condition side, the system is to win with probability one, regardless of the behavior of the environment. We define the system strategies and then formulate the almost-sure winning objective as well as the discounted-sum objective.

A (randomized) system strategy is defined as a tuple σs = (σm s ↪ ⇢ms ↪Ms↪m0s ), where Ms is a (possibly countably infinite) set of memory states; m0s 2 Ms is the initial memory state; σm s : Ss⇥Ms !D(A), and ⇢ms : S⇥Ms !Ms is the memory update function. If Ms is a singleton, σs is a memoryless strategy; if Ms is a finite set, σs is a finite-memory strategy. With a slight abuse of notation, we use σs(s↪ a) to represent σm s (s↪m0s )(a) for s 2 Ss, a 2 AG(s) when σs is memoryless. If ♣¶s0 2 S : σs(s↪m)(s0 ) > 0♦♣ = 1 for all s 2 Ss and m 2 Ms, σs is a pure strategy. An environment strategy σe = (σm e ↪ ⇢me ↪Me↪m0e ) can be defined analogously.

The Almost-Sure Winning Objective The winning condition for G is defined on its runs. Let AG : S ! 2A∩; be a mapping from each state to its available actions in G. For each s 2 S, a 2 AG(s), let EG(s↪ a) ✓ S be the set of possible successors by taking a at s in G. A run ⇡ = (st-1 ⇡ ↪ at⇡ )t2N+ of G is an infinite sequence of state-action pairs such that for all t 2 N+, st-1 ⇡ 2 S, at⇡ 2 AG(st⇡ ), and st⇡ 2 EG(st-1 ⇡ ↪ at⇡ ). ⇡ is winning for the system with respect to the Buchi condition if and only if F is visited for infinitely many times in ⇡, i.e. ♣¶t 2 N : si⇡ 2 F♦♣ = 1. A system strategy σs is almost-sure winning at s 2 S if a run ⇡ with s0⇡ = s is winning for the system with probability one when the system takes σs, regardless of the environment strategy. The almost-sure winning region for the system, denoted by Was (or W G as to explicitly indicate G), is the set of states at which the system has almost-sure winning strategies. By definition, there are no outgoing transitions from Se T Was that leaves Was.

The almost-sure winning objective for the system is to always take an almost-sure winning strategy. In other words, the system strategy is supposed to be almost-sure winning at any time in the process of learning.

The Discounted-SumObjective As common in the RL literature, we use state value functions and action value functions to evaluate system strategies. The state value function Vσs : S !R≥0 specifies the worst-case expected discounted reward from each state when the system the strategy σs. The action value function Qσs : S ⇥A!R≥0 shows the worstcase expected discounted reward if the system takes a given action at the current step and follows the strategy σs thereafter. A system strategy σs is optimal if it maximizes the state value functions over all system strategies. When σs is an optimal strategy, its state value function and action value function are called the optimal state value function and the optimal action value function, denoted by V ⇤ and Q⇤ respectively. V ⇤ and Q⇤ satisfy the following optimality conditions [Littman, 2001]:

where γ 2 (0↪ 1) is a discount factor. For any " > 0, a system strategy σs is "-optimal at s 2 S if Vσs (s) ≥ V ⇤ (s) - ". Given ⌃s as a set of system strategies, a system strategy σs 2 ⌃s is optimal over ⌃s at s 2 S if Vσs (s) ≥ maxσ0s2⌃s Vσ0s (s), or "-optimal over ⌃s at s if Vσs (s) ≥ maxσ0s2⌃s Vσ0s (s) - ".

The discounted-sum objective for the system is to be "- optimal over all almost-sure winning system strategies at all states that are visited infinitely often. In other words, eventually the worst-case expected reward at any state that will be visited in future is "-optimal.

3 ProblemFormulation

We make the following assumptions in our formulation.

Assumption 1. Both the environment and the system are aware of their current states, and can observe the reward after a transition is taken. In other words, the game is fully observable for both sides.

Assumption 2. The system knows the correct list of all possible successors for all state-action pairs, but does not know the exact transition distributions a priori.

The knowledge of all existing transitions is critical in order to achieve the almost-sure winning objective. It may seem demanding at the first glance, but it is possible that an almostsure winning strategy can never be learned from experience without the previous knowledge. For example, even if s0 2 S is never witnessed as a successor of a state-action pair (s↪ a), we cannot confirm that T(s↪ a)(s0 ) = 0. Also, without resetting, there can be a positive probability that the system leaves its almost-sure winning region during the exploration period and cannot guarantee almost-sure winning thereafter.

The third assumption is on the unknown reward. The upper bound Rmax can be set easily as it is not required to be tight.

Assumption 3. The reward function is unknown a priori, but is upper bounded by the specified positive number Rmax.

With the above assumptions, we formulate our learning problem as follows.

Problem 1. Given a turn-based stochastic Buchi game Gin = (Sin ↪ Sin s ↪ Sin e ↪ I in ↪Ain ↪ T in ↪Rin ↪ F in ) satisfying Assumptions 1 - 3, a discount factor γ 2 (0↪ 1) and suboptimality bound " > 0, learn a memoryless system strategy σs↪" that satisfies both the almost-sure winning objective and the discounted-sum objective.

4 Main Approach

We now develop the main algorithm to solve Problem 1. The first step is to compute the almost-sure winning region W in as for the system. By definition of almost-sure winning regions, the system can only win almost-surely if it always stays within W in as . The definition guarantees that for any s 2 Sin s T W in as , there exists an action a 2 AGin (s) such that EGin (s↪ a) ✓ W in as ; for any s 2 Sin e T W in as , EGin (s↪ a) ✓ W in as for all a 2 AGin (s). In other words, the system has a strategy to force the environment to stay within W in as once it is entered. Therefore we can construct a new game G from Gin as follows to ensure that the visited states are always restricted to W in as in G. G = Gin ↾ W in as = (S↪ Ss↪ Se↪ I↪ A↪ T↪ R↪ F ) such that:

Algorithm 1 HatGame and RecoverHatStrategy

• 1: function HatGame(G, Q⇤ , "1, p"1 )
• 2: For i 2 ¶1↪ 2♦, Sis ¶si ♣s 2 Ss♦▷
• 4: ˆ Ss Ss S S1 s S S2 s , ˆ S ˆ Ss S Se. 5: Define A⇤"1 : Ss ! 2A∩; such that for all s 2 Ss, A⇤"1 (s) = ¶a 2 AG(s)♣maxa02AG(s) Q(s↪ a0 ) - Q(s↪ a)  "1♦.
• 3: Define B : S1 s S S2 s ! Ss such that for all si 2 Sis and i 2 ¶1↪ 2♦, B(si ) = s holds.
• 6: ˆ A A S¶ˆa♦. 7: Define the set of available actions for all s 2 ˆ S: A ˆG(s) = 8>><>>: AG(s) if s 2 Se↪ ¶ˆa♦ if s 2 Ss↪ AG(B(s)) if s 2 S1 s ↪ A⇤"1 (B(s)) if s 2 S2 s ▷
• 9: return ˆG = ( ˆ S↪ ˆ Ss↪ ˆ Se↪ I↪ ˆ T ↪ R↪ F ).
• 8: Define the transition function for all s↪ s0 2 ˆ S and a 2 A ˆG(s): ˆ T(s↪ a)(s0 ) = 8>><>>: p"1 if s 2 Ss↪ s0 = s1 ↪ 1 - p"1 if s 2 Ss↪ s0 = s2 ↪ T (s↪ a)(s0 ) if s 2 Se↪ s0 2 S↪ T(B(s)↪ a)(s0 ) if s 2 S1 s S S2 s ↪ s0 2 S▷
• 10: end function
• 11: function RecoverHatStrategy( ˆG, ˆσs)
• 12: For all s 2 Ss and a 2 A ¯G(s), ¯σs(s↪ a) ˆ T (s↪ ˆa)(s1 )ˆσs(s1 ↪ a) + ˆ T(s↪ ˆa)(s2 )ˆσs(s2 ↪ a), where ˆ T is the transition function of ˆG.
• 13: return ¯σs.
• 14: end function

• ÷ S = W in as , Ss = Sin s T W in as , Se = Sin e T W in as , I = I in T W in as , and F = F in T W in as .
• ÷ For all s 2 Ss, AG(s) = ¶a 2 AGin (s) : EGin (s↪ a) ✓ W in as ♦; for all s 2 Se, AG(s) = AGin (s).
• ÷ For all transition (s↪ a↪ s0 ) in G, T(s↪ a)(s0 ) = T Gin (s↪ a)(s0 ), R(s↪ a↪ s0 ) = Rin (s↪ a↪ s0 ).

The set of almost-sure winning system strategies in Gin is a subset of the system strategies in G. Therefore if a system strategy σs is "-optimal at s 2 S, it is also "-optimal over all almost-sure winning strategies at s in Gin . So we transform Problem 1 into learning a memoryless almost-sure winning system strategy that is "-optimal in G.

We first consider the two objectives in Problem 1 when the reward functions and transition distributions are known. Without the Buchi objective, the discounted-sum objective degenerates to learning a system strategy that is "-optimal at the infinitely-often-visited states, which can be solved with some slight modification of the R-max algorithm [Brafman and Tennenholtz, 2003]. However, R-max is not applicable to the normal discounted-sum objective, as the Buchi condition is given independently from the reward function, and there is no standard parameterization of the space of all almost-sure winning strategies. This difficulty is common for all RL algorithms that were designed to optimize a reward function.

To avoid this difficulty, we consider the discounted-sum objective first. For discounted rewards, a memoryless system strategy σs is optimal if and only if Qσs (s↪ a) = V ⇤ (s) holds for all s 2 Ss and a 2 ¶a0 2 AG(s) : σs(s↪ a0 ) > 0♦ [Filar and Vrieze, 1996]. In other words, σs is optimal when it only takes the optimal actions. We construct a game G0 from G such that the two games are identical except that all actions available to the system states in G0 are optimal actions in G. Thus any system strategy in G0 is optimal in G. If W G0 as coincides with W G as , there exists a memoryless almost-sure winning strategy σs in G0 , which is also almost-sure winning in G as there are no restrictions to the environment in G0 . Then σs is an optimal almost-sure winning system strategy in G.

However, W G0 as may be a proper subset of W G as , as the system has fewer actions available in G0 . If such is the case, we would have to allow the system to take some suboptimal actions in G in order to preserve the almost-sure winning region. Intuitively, if a system strategy σ0s specifies only a small probability to the suboptimal actions, Vσs can still be nearoptimal. The following lemma shows that there exists such a σ0s that is almost-sure winning in G.

Lemma 1. Let Gin = (Sin ↪ Sin s ↪ Sin e ↪ I in ↪Ain ↪ T in ↪ F in ) be a turn-based Buchi game, and W in as be the almostsure winning region of Gin . Let G = Gin ↾ W in as = (S↪ Ss↪ Se↪ I↪A↪ T↪ F). Then a memoryless system strategy σs such that σs(s↪ a) > 0 for all s 2 Ss, a 2 AG(s) is almost-sure winning in G.

To bound the probability of taking suboptimal actions, we construct a game ˆG = HatGame(G↪Q⇤ ↪ "1↪ p"1 ) as in Algorithm 1. For each system state s, we have an additional action ˆa and two additional system states s1 and s2 in ˆG such that ˆa is the unique available action at s and

Algorithm 2 Overall algorithm for Problem 1

• Input: A turn-based Buchi game Gin = (Sin ↪ Sin s ↪ Sin e ↪ I in ↪Ain ↪ T in ↪Rin ↪ F in ) satisfying Assumptions 1 - 3, reward upper bound Rmax > 0, a discount factor γ 2 (0↪ 1), a suboptimality bound " > 0, a confidence bound δc 2 (0↪ 1).
• 1: Compute the almost-sure winning region W in as and a memoryless almost-sure winning strategy σs for the system in Gin .
• 2: G := Gin ↾ W in as = (S↪ Ss↪ Se↪ I↪ A↪ T↪ R↪ F ).
• 3: Initialize the game model ¯G (S↪ Ss↪ Se↪ I↪A↪ ¯ T↪ ¯R↪ F) such that ¯G shares the same set of transitions with G and all transition distributions in ¯ T are uniform; ¯R(s↪ a↪ s0 ) Rmax 1-γ for all transition (s↪ a↪ s0 ).
• 4: σs↪" σs.
• 5: For all existing transition (s↪ a↪ s0 ) in ¯G, k(s↪ a↪ s0 ) 0, L(s↪ a) 0, ¯Q⇤ (s↪ a) Rmax (1-γ)2 .
• 8: while TRUE do

• 9: if s 2 Ss then
• 10: Take σs↪" for one step.
• 11: else
• 12: Environment takes a transition.
• 13: end if

14: Observe the transition (s↪ a↪ s0 ) and the reward r.

19:

20:

21:

22:

For all s0 2 S, ¯

Ps02S k(s↪a↪s0 ) .

T(s↪ a)(s0 )

k(s↪a↪s0 )

Update the optimal action value function ¯Q⇤ .

Construct ˆG HatGame( ¯G↪ ¯Q⇤ ↪ "1↪ p"1 ).

Compute a memoryless almost-sure winning

strategy ˆσs for the system in ˆG.

• 23: σs↪" RecoverHatStrategy( ˆG↪ ˆσs). 24: end if 25: end if 26: end while

E ˆG(s↪ ˆa) = ¶s1 ↪ s2 ♦. At s1 the system can take all actions in AG(s); at s2 the system can only take the optimal actions. The transition probability from s to s1 is confined to be a small number p". For each memoryless system strategy ˆσs in ˆG, we can construct a memoryless system strategy σs = RecoverHatStrategy( ˆG↪ ˆσs) in G. As expected, such σs is near-optimal in G, as shown in Lemma 2.

Lemma 2. Let G and ˆG be two turn-based Buchi games such that ˆG = HatGame(G↪ Q⇤ ↪ "1↪ p"1 ), where Q⇤ is the optimal action value function of G, and "1 > 0↪ p"1 2 (0↪ 1) are constants. The reward function R in G is bounded by Rmax 1-γ , where γ 2 (0↪ 1) is the discount factor. If ˆσs is a strategy for the system in ˆG, then σs = RecoverHatStrategy( ˆG↪ ˆσs) is ("1(1 - p"1 ) + p"1 Rmax (1-γ)2 )-optimal in G.

The following lemma guarantees that the strategies σs and ˆσs can only be almost-sure winning simultaneously.

Lemma 3. The games G, ˆG and the strategies σs, ˆσs are defined as in Lemma 2. Then ˆσs is almost-sure winning for the system in ˆG if and only if the constructed σs is almost-sure winning for the system in G.

Therefore, given the optimal action value function Q⇤ , we can solve a memoryless "-optimal almost-sure winning strategy in G as follows: first properly construct a game ˆG, then synthesize a memoryless almost-sure winning strategy ˆσs in ˆG (whose existence is shown in Lemma 1), and eventually recover a memoryless strategy σs in G from ˆσs. The constructed game ˆG changes when the optimal actions identified by Q⇤ changes. But the recovered strategy σs is always almost-sure winning in G, no matter what Q⇤ is.

Now we return to Problem 1, where both the reward function and the transition distributions are unknown. As in the Rmax algorithm, we refine an optimistically-initialized game model ¯G in an online manner. With the help of Algorithm 1, we can update the system strategy σs↪" every time a new transition is learned, and always keep σs↪" to be both almost-sure winning and "-optimal with respect to its current model ¯G. The overall algorithm is shown in Algorithm 2, and Theorem 1 follows from an argument similar to the correctness proof of the R-max algorithm. A complete proof can be found in the technical version at https://www.ae.utexas.edu/ facultysites/topcu/archive/ijcai16.html.

Theorem 1. Let Gin be a turn-based Buchi game, Rmax be a positive upper bound of the reward, γ 2 (0↪ 1) be a discount factor, " > 0 be a suboptimality bound and 1 - δc 2 (0↪ 1) be a confidence lower bound, as given in the input of Algorithm 2. The system strategy σs↪" in Algorithm 2 is always memoryless and almost-sure winning. With probability no less than 1 - δc, by taking σs↪", the future discounted reward from the current state s is at least V ⇤ (s)-", except for some number of steps polynomial in ♣S♣↪ ♣A♣↪ 1" and 1 δc .

5 Example

We show the usage of our algorithm with a robot motion planning problem which involves simultaneous resource collection and surveillance. This example was run on a laptop with an 8 Intel(R) Core(TM) 2.40GHz CPU and 8 GB memory.

We first introduce the turn-based game and task requirements. The system moves in a 3-by-3 grid world, and it has to move to an adjacent block if the current state is a system state. The environment is a signal light that indicates the dangerous area in the world at the current step which needs to be monitored closely. If the environment light is on, the upper left four blocks are dangerous; otherwise, the lower right four blocks are dangerous. The environment can arbitrarily decide the status of the light in the next step if the current state is an environment state. Furthermore, the lower left block and the upper right block are labeled as post offices. For ease of demonstration, we assume that all transitions are deterministic, i.e. ♣EG(s↪ a)♣ = 1 for all state-action pair (s↪ a).

We want to learn a strategy for the system to both patrol the dangerous areas and persistently visit the two post offices. We first interpret the task requirements as a almost-sure winning objective and a discounted-sum objective, encode them as inputs to our algorithm, and then show the results.

Almost-Sure Winning Objective The task of visiting the two post offices can be expressed by the four-state DBA in Figure 1. The initial state is q1, and the set of accepting states is ¶q4♦. The upper right block is labeled by 'p1' ('post office #1') and the lower left block is labeled by 'p2' ('post office #2'). We show that the Buchi condition is satisfied if and only if both p1 and p2 are visited infinitely often. Starting from the initial state, the system transits to q2 if it visits p1, or transits to q3 if it visits p2. If it visits neither of them, it stays at q1. From q2 and q3, the system should visit the other post office (p2 for q2 and p1 for q3) in order to enter q4. q4 has the same outgoing transitions as q1. The transitions show that one new visit to q4 requires at least one new visit to p1 and one new visit to p2. Therefore to satisfy the Buchi condition, i.e. to visit q4 infinitely often, the system has to visit p1 and p2 infinitely often. All initial states are with DBA state q1.

The Discounted-Sum Objective The task of monitoring the dangerous area is interpreted as a discounted-sum objective. A reward function is designed to encourage the system to patrol the dangerous area. The system will be rewarded by 1 in the following cases: (1) when the system transits into the dangerous area; (2) when the light is on and the system moves counterclockwise in the dangerous area; (3) when the light is off and the system moves clockwise in the dangerous area. For all other system transitions and all environment transitions, there is no reward. Throughout this example, the discount factor γ is 0▷6, and Rmax = 1.

The system does not know this reward function ahead of time, but eventually manages to learn a strategy with optimal worst-case discounted reward. As shown in Figure 2, the system learns to approach the area specified by the environment as soon as possible and then move in the corresponding direction to maximize the reward.

We get the product of the original turn-based game and the DBA, which results in a turn-based Buchi game Gin . The almost-sure winning region W in as and a memoryless almostsure winning strategy σs are computed with the off-the-shelf tool PGSolver [Friedmann and Lange, 2015]. It turns out that W in as is the whole state space, and σs is illustrated in Figure 3. The suboptimality bound " is set to be 0▷0001. To output the learned strategy in a timely manner, we added a terminating condition to the while loop in Algorithm 2 such that the algorithm stops if there are no updates in the last 10,000 steps.

Upon termination, the learned strategy for the system is shown in Figure 4. The strategy is randomized and allows two actions at each system state, one with probability (1 - p"1 ) and the other with probability p"1 , represented by the big triangles and small triangles respectively. The worst-case value functions for the learned strategy, the initial almost-sure winning strategy, and an optimal strategy are shown in Figure 5. These value functions are evaluated with the true reward function, and thus are not accessible to the system. It can be found that the value of the learned strategy is much better than that of the initial strategy, although it is not at all close to the optimal strategy. In Figure 4, we marked all states where the learned strategy is "-optimal with yellow background. It turns out that all system states are marked with yellow, i.e. are "- optimal, except those that are not reachable from the initial states. The product Buchi game has 144 states, 72 system states and 192 transitions. On average of ten repetitive experiments, the algorithm terminates at 58.05 seconds with the last update occurs at 29.77 seconds.

6 Conclusion

We studied the strategy synthesis in turn-based stochastic games with both qualitative Buchi objectives and quantitative discounted-sum objectives. A PAC learning algorithm is proposed to learn a memoryless "-optimal almost-sure winning strategy when the reward function and transition distributions are unknown a priori. We also demonstrated the algorithm on an example involving resource-collection and surveillance tasks.

Acknowledgments

This work was partially supported by awards AFRL FA865015-C-2546, ONR N000141310778, ARO W911NF-15-10592, NSF 1550212 and DARPA W911NF-16-1-0001.