Transfer of Temporal Logic Formulas in Reinforcement Learning

1 Introduction

Reinforcement learning (RL) has been successful in numerous applications. In practice though, it often requires extensive exploration of the environment to achieve satisfactory performance, especially for complex tasks with sparse rewards [Wang and Taylor, 2017].

The sampling efficiency and performance of RL can be improved if some high-level knowledge can be incorporated in the learning process [Toro Icarte et al., 2018a]. Such knowledge can be also transferred from a source task to a target task if these tasks are logically similar [Taylor and Stone, 2007]. For example, propositional logic and first-order logic have been used as representations of knowledge in the form of logical structures for transfer learning [Mihalkova et al., 2007]. They showed that incorporating such logical similarities can expedite RL for the target task [Torrey et al., 2008].

The transfer of high-level knowledge can be also applied to tasks where the timing of the events matters. We call such tasks as temporal tasks. Consider the gridworld example in Figure 1. In the source task, the robot should first reach a green region GS and stay there for at least 4 time units, then reach another yellow region Y S within 40 time units. In the target task, the robot should first reach a green region GT and stay there for at least 5 time units, then reach another yellow region Y T within 40 time units. In both tasks, the green and yellow regions are a priori unknown to the robot. After 40 time units, the robot obtains a reward of 100 if it has completed the task and obtains a reward of -10 otherwise. It is intuitive that the two tasks are similar at a high level despite the differences in the specific regions in the workspace and timing requirements.

Transfer learning between temporal tasks is complicated due to the following factors: (a) No formally defined criterion exists for logical similarities between temporal tasks. (b) Logical similarities are often implicit and need to be identified from data. (c) There is no known automated mechanism to transfer the knowledge based on logical similarities.

In this paper, we propose a transfer learning approach for temporal tasks in two levels: transfer of logical structures and transfer of low-level implementations. For ease of presentation, we focus on Q-learning [Watkins and Dayan, 1992], while the general methodology applies readily to other forms of RL.

In the first level, we represent the high-level knowledge in temporal logic [Pnueli, 1977], which has been used in many applications in robotics and artificial intelligence [KressGazit et al., 2011; To et al., 2016]. Specifically, we use a fragment of metric interval temporal logic (MITL) with bounded time intervals. We transfer such knowledge from a source task to a target task based on the hypothesis of logical transferability (this notion will be formalized in Section 4.1) between the two tasks.

To identify logical transferability, we develop an inference technique that extracts informative MITL formulas (formalized in Section 3) in sequential disjunctive normal form. If the inference process indeed identifies logical transferability, we construct a timed automaton for each sequential conjunctive subformula of the inferred MITL formulas. We combine the locations and clock valuations of the timed automaton with the state of the robot to form an extended state, and perform RL in the extended state space for the target task.

In the second level, we transfer the extended Q-functions (i.e., Q-function on the extended states) from the source task to the target task if logical transferability is identified in the first level. We first perform RL in the extended state space for the source task. Next, we establish mappings between the corresponding components (clocks, locations, etc.) of the timed automata from the two tasks based on the identified logical transferability. Finally, we transfer the obtained optimal extended Q-functions from the source task to the target task based on these mappings, and perform RL for the target task starting with the transferred extended Q-functions.

The implementation of the proposed approach shows, in both levels, that the sampling efficiency is significantly improved for RL of the target task.

1.1 RelatedWork

Our work is closely related to the work on RL with temporal logic specifications [Aksaray et al., 2016; Li et al., 2017; Toro Icarte et al., 2018b; Fu and Topcu, 2014; Wen et al., 2017; Alshiekh et al., 2018]. The current results mostly rely on the assumption that the high-level knowledge (i.e., temporal logic specifications) are given, while in reality they are often implicit and need to be inferred from data.

The methods for inferring temporal logic formulas from data can be found in [Hoxha et al., 2017; Kong et al., 2017; Bombara et al., 2016; Neider and Gavran, 2018; Xu et al., 2018; Xu and Julius, 2018; Vazquez-Chanlatte et al., 2018; Xu et al., 2019; Shah et al., 2018]. The inference method used in this paper is inspired from [Bombara et al., 2016] and [Xu et al., 2019].

While there has been no existsing work on RL-based transfer learning utilizing similarity between temporal logic formulas, the related work on transferring first-order logical structures or rules for expediting RL can be found in [Taylor and Stone, 2007; Torrey and Shavlik, 2010; Torrey et al., 2008], and the related work on transferring logical relations for action-model acquisition can be found in [Zhuo and Yang, 2014].

2 Preliminaries

2.1 Metric Interval Temporal Logic

Let B = {⊤,⊥} (tautology and contradiction, respectively) be the Boolean domain and T = {0, 1, 2, . . . } be a discrete set of time indices. The underlying system is modeled by a Markov decision process (MDP) M = (S,A, P), where the state space S and action set A are finite, P : S × A × S → [0, 1] is a transition probability distribution. A trajectory s0:L = s0s1 · · · sL describing an evolution of the MDP M is a function from T to S. Let AP be a set of atomic predicates.

The syntax of theMITLf fragment of time-boundedMITL formulas is defined recursively as follows 1 :

where ρ ∈ AP is an atomic predicate; ¬ (negation), ∧ (conjunction), ∨ (disjunction) are Boolean connectives; ♦ (eventually) and □ (always) are temporal operators; and I is a bounded interval of the form I = [i1, i2] (i1 < i2, i1, i2 ∈ T). For example, the MITLf formula □[2,5](x > 3) reads as "x is always greater than 3 during the time interval [2, 5]".

A timed word generated by a trajectory s0:L is defined as a sequence (L(st1 ), t1), . . . , (L(stm ), tm), where L : S → 2AP is a labeling function assigning to each state s ∈ S a subset of atomic predicates in AP that hold true at state s, t1 = 0, tm = L, tk-1 < tk (k ∈ [2,m]) and for k ∈ [1,m1], tk+1 is the largest time index such that L(st) = L(stk ) for all t ∈ [tk, tk+1). The satisfaction of an MITLf formula by timed words as Boolean semantics can be found in [Alur et al., 1996]. We say that a trajectory s0:L satisfies an MITLf formula φ, denoted as s0:L |= φ, if and only if the timed word generated by s0:L satisfies φ. As the time intervals I in MITLf formulas are bounded intervals, MITLf formulas can be satisfied and violated by trajectories of finite lengths.

2.2 Timed Automaton

Let C be a finite set of clock variables. The set CC of clock constraints is defined by [Ouaknine and Worrell, 2005]

Definition 1. [Alur and Dill, 1994] A timed automaton is a tuple A = (Σ, Q, q0 , C, F, ∆), where Σ is a finite alphabet of input symbols, Q is a set of locations, q0 ∈ Q is the initial location, C is a finite set of clocks, F ⊂ Q is a set of accepting locations, ∆ ⊂ Q × Σ × Q × CC × 2C is the transition function, e = (q, σ, q′ , ϕC, rC) ∈ ∆ represents a transition from q to q′ labeled by σ, provided the precondition ϕC on the clocks is met, rC is the set of clocks that are reset to zero.

Remark 1. We focus on timed automata with discrete time, which are also called tick automata in [Gruber et al., 2005].

1 Although other temporal operators such as "Until "(U) may also appear in the full syntax of MITL, they are omitted from the syntax here as they can be hard to interpret and are not often used for the inference of temporal logic formulas [Kong et al., 2017].

A timed automaton A is deterministic if and only if for each location and input symbol there is at most one transition to the next location. We denote by v = (v1, . . . , v|C|) ∈ V ⊂ T|C| the clock valuation of A (we denote by |C| the cardinality of C), where vk ∈ Vk ⊂ T is the value of clock ck ∈ C. For a timed word ν = (σ0, t0), (σ1, t1), . . . , (σm, tm) (where t0 < t1 < · · · < tm, σk ∈ Σ for k ∈ [0,m]) and writing dk := tk+1 - tk, a run of A on ν is defined as

where the flow-step relation is defined by (q, v) d-→ (q, v + d) where d ∈ R>0; the edge-step relation is defined by (q, v) σ (q′ , v′ ) if and only if there is an edge (q, σ, q′ , ϕC, rC) ∈ ∆ such that σ ∈ Σ, v satisfies ϕC, v′k = 0 for all ck ∈ rC and v′k = vk for all ck ̸∈ rC. A finite run is accepting if the last location in the run belongs to F. A timed word ν is accepted by A if there is some accepting run of A on ν.

3 Information-Guided Inference of Temporal Logic Formulas

We now introduce the information gain provided by an MITLf formula, the problem formulation and the algorithm to extract MITLf formulas from labeled trajectories.

3.1 Information Gain of MITLf Formulas

We denote by BL the set of all possible trajectories with length L generated by the MDPM, and use GL : BL → [0, 1] to denote a prior probability distribution (e.g., uniform distribution) over BL. We use PBL,φ to denote the probability of a trajectory s0:L satisfying φ in BL based on GL.

Definition 2. Given a prior probability distribution GL and an MITLf formula φ such that PBL,φ > 0, we define ¯ G φL : BL → [0, 1] as the posterior probability distribution, given that φ evaluates to true, which is expressed as

The expression of ¯ G φL can be derived using Bayes' theorem. We use the fact that the probability of φ evaluating to true given s0:L is 1, if s0:L satisfies φ; and it is 0 otherwise.

Definition 3. When the prior probability distribution GL is updated to the posterior probability distribution ¯ G φL, we define the information gain as

where DKL( ¯ G φL||GL) is the Kullback-Leibler divergence from GL to ¯ G φL.

Proof. Straightforward fromDefinitions 2 and 3.

If φ = ⊤, then PBL,φ = 1 and I(GL, ¯ G φL) = 0, i.e., tautologies provide no information gain. For completeness, we also define that the information gain I(GL, ¯ G φL) = 0 if PBL,φ = 0. So if φ = ⊥, then PBL,φ = 0 and I(GL, ¯ G φL) = 0, i.e., contradictions provide no information gain.

For two MITLf formulas φ1 and φ2, we say φ1 is more informative than φ2 with respect to the prior probability distribution GL if I(GL, ¯ G φ1 L ) > I(GL, ¯ G φ2 L ).

Based on Proposition 1, the computation of the information gain requires the computation of PBL,φ. We point the reader to [Xu et al., 2019] for a recursive method to compute PBL,φ.

3.2 ProblemFormulation

We now provide some related definitions for formulating the inference problem. Let a set P of primitive structures [Bombara et al., 2016] used in the rest of the paper be

where I = [i1, i2] (i1 < i2, i1, i2 ∈ T), I ′ = [0, i2] (i2 > 0, i2 ∈ T), and ρ is an atomic predicate. We call an MITLf formula φ a primitive MITLf formula if φ follows one of the primitive structures in P or the negation of such a structure.

Definition 4. For an MITLf formula φ, we define the starteffect time ts(φ) and end-effect time te(φ) recursively as

Definition 5. An MITLf formula φ is in disjunctive normal form if φ is expressed in the form of (φ11 ∧ · · · ∧ φn1 1 ) ∨ · · · ∨ (φ1m ∧· · ·∧φnm m ), where each φji is a primitiveMITLf formula (also called primitive subformula of φ). If, for any i ∈ [1,m] and for all j, k ∈ [1, ni] such that j < k, it holds that te(φji ) < ts(φki ), then we say φ is in sequential disjunctive normal form (SDNF) and we call each φi := φ1i ∧ · · · ∧ φni i a sequential conjunctive subformula.

In the following, we consider MITLf formulas only in the SDNF for reasons that will become clear in Section 4. We define the size of an MITLf formula φ in the SDNF, denoted as ϱ(φ), as the number of primitive MITLf formulas in φ.

Suppose that we are given a set SL = {(sk0:L, lk)}NSL k=1 of labeled trajectories, where lk = 1 and lk = -1 represent desired and undesired behaviors, respectively. We define the satisfaction signature gφ(sk0:L) of a trajectory sk0:L as follows: gφ(sk0:L) = 1, if sk0:L satisfies φ; and gφ(sk0:L) = -1, if sk0:L does not satisfy φ. Note that here we assume that L is sufficiently large, thus sk0:L either satisfies or violates φ. A labeled trajectory (sk0:L, lk) is misclassified by φ if gφ(sk0:L) ̸= lk. We use CR(SL, φ) = |{(sk0:L, lk) ∈ SL : gφ(sk0:L) = lk}|/|SL| to denote the classification rate of φ in SL.

Problem 1. Given a set SL = {(sk0:L, lk)}NSL k=1 of labeled trajectories, a prior probability distribution GL, real constant ζ ∈ (0, 1] and integer constant ϱth ∈ (0,∞), construct an MITLf formula φ in the SDNF that maximizes I(GL, ¯ G φL) while satisfying

• the classification constraint CR(SL, φ) ≥ ζ and
• the size constraint ϱ(φ) ≤ ϱth.

Intuitively, as there could be many MITLf formulas that satisfy the classification constraint and the size constraint, we intend to obtain the most informative one to be utilized and transferred as features of desired behaviors.

We call an MITLf formula that satisfies both the two constraints of Problem 1 a satisfying formula for SL.

3.3 Solution Based on Decision Tree

We propose an inference technique, which is inspired by [Bombara et al., 2016] and [Xu et al., 2019], in order to solve Problem 1. The technique consists of two steps. In the first step, we construct a decision tree where each non-leaf node is associated with a primitive MITLf formula (see the formulas inside the circles in Figure 2). In the second step, we convert the constructed decision tree to an MITLf formula in the SDNF.

In Algorithm 1, we construct the decision tree by recursively calling the MITLtree procedure from the root node to each leaf node. There are three inputs to the MITLtree procedure: (1) a set S of labeled trajectories assigned to the current node; (2) a formula φpath to reach the current node (also called the path formula, see the formulas inside the rectangles in Figure 2); and (3) the depth h of the current node. The set S assigned to the root node is initialized as SL in Problem 1, φpath and h are initialized as ⊤ and 0, respectively.

For each node, we set a criterion stop(φpath , h, S) to determine whether it is a leaf node (Line 2). Each leaf node is associated with label 1 or -1, depending on whether more than 50% of the labeled trajectories assigned to that node are with label 1 or not.

At each non-leaf node z, we construct a primitive MITLf formula φθ parameterized by θ ∈ Υz, where

For example, for an MITLf formula φθ = □[i1,i2](x > a), we have θ = [i1, i2, a]. If φpath = ♦[1,15]□[0,4](x > 3), then Υz ensures that the start-effect time of φθ is later than the endeffect time of φpath (which is 19). Essentially Υz guarantees that the primitive MITLf formula φθ and primitive subformulas of φpath can be reordered to form a sequential conjunctive subformula (see Definition 5).

Algorithm 1 Information-Guided MITLf Inference.

• 1: procedure MITLtree(S = {(sk0:L, lk)}NS k=1 , φpath , h)
• 2: if stop(φpath , h, S) then
• 3: Create node zLeaf as a leaf node
• 4: if node zLeaf is associated with label 1
• 5: zLeaf .φpath ←φpath
• 6: end if
• 7: return z
• 8: end if
• 9: Create node z as a non-leaf node
• 10: Obtain Υz from (2)
• 11: z.φ ← arg max φ∈P,θ∈Υz CR(S, φθ) +λI(GL, ¯ G φθ L )
• 12: {S⊤, S⊥} ← partition(S, z.φ)
• 13: z.left ←MITLtree(S⊤, φpath ∧ z.φ, h+1)
• 14: z.right ←MITLtree(S⊥, φpath ∧¬z.φ, h+1)
• 15: return z
• 16: end procedure

We use particle swarm optimization (PSO) [Eberhart and Shi, 2001] to optimize θ for each primitive structure from P and compute a primitive MITLf formula z.φ = φ∗θ which maximizes the objective function

in Line 11, where λ is a weighting factor.

With z.φ, we partition the set S into S⊤ and S⊥, where the trajectories in S⊤ and S⊥ satisfy and violate z.φ, respectively (Line 12). Then the procedure is called recursively to construct the left and right sub-trees for S⊤ and S⊥, respectively (Lines 13, 14).

After the decision tree is constructed, for each leaf node associated with label 1, it is also associated with a path formula zLeaf .φpath (Line 4 to Line 6). The path formula zLeaf .φpath is constructed recursively from the associated primitive MITLf formulas along the path from the root node to the parent of the leaf node (see Figure 2). We rearrange the primitive subformulas of each zLeaf .φpath in the order of increasing start-effect time to obtain a sequential conjunctive subformula. We then connect all the obtained sequential conjunctive subformulas with disjunctions. In this way, the obtained decision tree can be converted to an MITLf formula in the SDNF. As in the example shown in Figure 2, if ts(φ1) < ts(φ2) and ts(¬φ1) < ts(φ3), then the decision tree can be converted to (φ1 ∧ φ2) ∨ (¬φ1 ∧ φ3) in the SDNF. If ts(φ2) < ts(φ1) and ts(φ3) < ts(¬φ1), then the decision tree can be converted to (φ2 ∧ φ1) ∨ (φ3 ∧ ¬φ1) in the SDNF.

We set the criterion stop(φpath , h, S) as follows. If at least ζ (e.g., 95%) of the labeled trajectories assigned to the node are with the same label (Condition I) or the depth h of the node reaches a set maximal depth hmax (Condition II) or Υz, as defined in (2), becomes the empty set (Condition III), then the node is a leaf node. If condition I holds for each leaf mode, then the obtainedMITLf formula satisfies the classification constraint of Problem 1. If we set hmax2hmax-1 ≤ ϱth, then the size constraint is guaranteed to be satisfied.

The complexity of Algorithm 1 for the average case can be determined through the Akra-Bazzi method as follows [Bombara et al., 2016]:

where f(NS) is the complexity of the local PSO algorithm for NS labeled trajectories, and Θ(·) denotes the two-sided asymptotic notation for complexity bound.

4 Transfer Learning of Temporal Tasks Based on Logical Transferability

In this section, we first introduce the notion of logical transferability. Then, we present the framework and algorithms for utilizing logical transferability for transfer learning.

4.1 Logical Transferability

To define logical transferability, we first define the structural transferability between two MITLf formulas.

For each primitive MITLf formula φ, we use OT (φ) to denote the temporal operator in φ. For example, OT (♦[5,8](x > 3)) = ♦ (eventually) and OT (□[0,8]♦[0,4](x < 5)) = □♦ (always eventually).

Definition 6. Two MITLf formulas (in the SDNF)

and

are structurally equivalent, if and only if the followings hold: (1) m = ˆm and, for every i ∈ [1,m], ni = ˆni; and (2) For every i ∈ [1,m] and every j ∈ [1, ni], OT (φji ) =

Definition 7. For two MITLf formulas φ1 and φ2 in the SDNF, φ2 is structurally transferable from φ1 if and only if either of the following conditions holds:

1) φ1 and φ2 are structurally equivalent;

2) φ2 is in the form of φ12 ∨ · · · ∨ φp2 (p > 1), where each φk2 (k = 1, . . . , p) is structurally equivalent with φ1.

Suppose that we are given a source task T S in the source environment E S and a target task T T in the target environment E T , with two sets S SL and S TL of labeled trajectories collected during the initial episodes of RL (which we call the data collection phase) in E S and E T respectively. The trajectories are labeled based on a given task-related performance criterion. To ensure the quality of inference, the data collection phase is chosen such that both S SL and S TL contain sufficient labeled trajectories with both label 1 and label -1.We give the following definition for logical transferability.

Definition 8. T T is logically transferable from T S based on S SL, S TL, ζ and ϱth (as defined in Problem 1), if and only if there exist satisfying formulas φS for S SL and φT for S TL such that φT is structurally transferable from φS .

In the following, we explain the proposed transfer learning approach based on logical transferability in two different levels. We provide a workflow diagram as an overview of the proposed transfer learning approach, as shown in Figure 3.

4.2 Transfer of Logical Structures Based on Hypothesis of Logical Transferability

We first introduce the transfer of logical structures between temporal tasks. To this end, we pose the hypothesis that the target task is logically transferable from the source task. If logical transferability can be indeed identified, we perform RL for the target task utilizing the transferred logical structure. Specifically, we take the following three steps:

Step 1: Extracting MITLf Formulas in the Source Task

From S SL, we infer an MITLf formula φS using Algorithm 1. If φS is a satisfying formula for S SL, we proceed to Step 2.

As in the introductory example, we obtain the satisfying formula φS = ♦[1,15]□[0,4] ¯GS ∧ ♦[21,39] ¯ Y S for S SL (see Section 5 for details).

Step 2: Extracting MITLf Formulas in the Target Task

From S TL, we check if it is possible to infer a satisfying MITLf formula φT for S TL such that φT is structurally transferable from the inferred MITLf formula φS from the source task. We start from inferring an MITLf formula that is structurally equivalent with φS . This can be done by fixing the temporal operators (the same with those of φS ), then optimizing the parameters that appear in φT (through PSO) for maximizing the objective function in (3). If a satisfying MITLf formula is not found, we infer a MITLf formula φT in the form of φT = φT1 ∨ φT2 , where φT1 and φT2 are both structurally equivalent with φS . In this way, we keep increasing the number of structurally equivalent formulas connected with disjunctions until a satisfying MITLf formula is found, or the size constraint is violated (i.e., ϱ(φT ) > ϱth). If a satisfying MITLf formula is found, we proceed to Step 3; otherwise, logical transferability is not identified.

As in the introductory example, we obtain the satisfying formula φT = ♦[5,18]□[0,5] ¯GT ∧ ♦[24,39] ¯ Y T for S TL and φT is structurally equivalent with φS , hence logical transferability is identified.

Step 3: Constructing Timed Automata and Performing RL in the Extended State Space for the Target Task

For the satisfying formula φT = φT1 ∨ · · · ∨ φTm in the SDNF, we can construct a deterministic timed automaton (DTA) AφTi = {2AP , QφTi , q0φTi , C φTi , F φTi , ∆φTi } [Alur et al., 1996] that accepts precisely the timed words that satisfy each sequential conjunctive subformula φTi .

We perform RL in the extended state space XT = ⋃i XT i , where each XT i = ST × QφTi × V φTi (ST is the state space for the target task, V φTi is the set of clock valuations for the clocks in C φTi ) is a finite set of extended states. For each episode, the index i is first selected based on some heuristic criterion. For example, if the atomic predicates correspond to the regions to be reached in the state space, we select i such that the centroid of the region corresponding to the atomic predicate in φ1,T i (as in φTi = φ1,T i ∧ · · · ∧ φni,T i ) has the nearest (Euclidean) distance from the initial state sT0 . Then we perform RL in XT i . For Q-learning, after taking action aT at the current extended state χTi = (sT , qT , vT ) ∈ XT i , a new extended state χ′ T i = (s′ T , q′ T , v′ T ) ∈ XT i and a reward RT are obtained. We have the following update rule for the extended Q-function values (denoted as ¯Q):

where α and γ are the learning rate and discount factor, respectively.

As in the introductory example, we construct a DTA [see Figure 4 (b)] that accepts precisely the timed words that satisfy φT as there is only one sequential conjunctive subformula in φT . We then perform RL in the extended state space XT = ST × QφT × V φT , where ST is the state space in the 9×9 gridworld, QφT = {qT 0 , qT 1 , qT 2 , qT 3 } (qT 0 = q0φT ) and V φT = {0, 1, . . . , 40} × {0, 1, . . . , 40} (the set of clock valuations for the clocks cT1 and cT2 ).

4.3 Transfer of Extended Q-functions Based on Identified Logical Transferability

Next, we introduce the transfer of extended Q-functions if logical transferability can be identified from Section 4.2.

We assume that the sets of actions in the source task and the target task are the same, denoted as A. For the satisfying formula φS = φS1 ∨ · · · ∨ φSm in the SDNF, we construct a DTA corresponding to each φSi and perform Q-learning in the extended state space for the source task. We denote the obtained optimal extended Q-functions as ¯QS∗ (sS , qS , vS , a). In the following, we explain the details for transferring ¯QS∗ (sS , qS , vS , a) to the target task based on the identified logical transferability.

From Definitions 6 and 7, if φT = φT1 ∨ · · · ∨ φTmT is structurally transferable from φS = φS1 ∨ · · · ∨ φSmS , then for all index i ∈ [1,mT ], the sequential conjunctive subformulas

φTi and φS ˆi are structurally equivalent, where ˆi = i mod mS (where mod denotes the modulo operation). For the DTA AφTi and AφSˆi constructed from φTi and φS ˆi respectively, it can

be proven that we can establish bijective mappings: ξ i,ˆi Σ : 2AP → 2AP , ξ i,ˆi Q : QφTi → QφSˆi and ξ i,ˆi C : C φTi → C φSˆi such that the structures of AφTi and AφSˆi are preserved under these bijective mappings [Glushkov, 1961]. Specifically, we have ξ i,ˆi Q (q0φTi ) = q0φSˆi , ξ i,ˆi Q [F φTi ] = F φSˆi (where ξ i,ˆi Q [F φTi ] denotes the point-wise application of ξ i,ˆi Q to elements of F φTi ). Besides, for any ρ ∈ 2AP and any q, q′ ∈ QφTi , we have that

holds if and only if

holds, where C1 = C φTi and C2 = ξ i,ˆi C [C φTi ]. See Figure 4 for an illustrative example.

Algorithm 2 is for the transfer of the extended Q-functions. For all indices i, we first identify a unique primitive MITLf formula φj,T i (as in φTi = φ1,T i ∧ · · · ∧ φni,T i ) that is to be satisfied at each extended state χTi = (sT , qT , vT ) (Line 3). Specifically, according to qT and vT , we identify the index j such that φ1,T i , . . . , φ(j-1),T i are already satisfied while φj,T i is still not satisfied.

Next, we identify the state, location and clock valuation in the extended state χS ˆi that are the most similar to sT , qT and vT respectively in the extended state χTi .

Identification of State: We first identify the atomic predicate ρj,T i in the primitiveMITLf formula φj,T i . Then we identify the atomic predicate ρS corresponding to ρj,T i through the Algorithm 2 Transfer of Extended Q-functions Based on Logical Transferability.

• 1: Inputs: φS , φT , XS , XT , A
• 2: for all index i and all χTi = (sT , qT , vT ) ∈ XT i do
• 3: Identify the unique formula φj,T i and its atomic predicate ρj,T i
• 4: ˆi ← mod (i,mS )
• 5: ρS ← ξ i,ˆi Σ (ρj,T i )

• 7: qS ← ξ i,ˆi Q (qT )
• 8: for all cTl ∈ C φTi and all vT l ∈ V φTi l do
• 9: cSk ← ξ i,ˆi C (cTl )

• 11: end for

• 13: end for
• 14: Return ¯QT

mapping ξ i,ˆi Σ (Line 5). As in the introductory example, at the locations qS 0 and qT 0 , we first identify the atomic predicate ¯GT , then the mapping ξ 1,1 Σ maps ¯GT to its corresponding atomic predicate ¯GS . We use Cr(ρ) to denote the centroid of the region corresponding to the atomic predicate ρ and ‖·‖ to denote the 2-norm. We identify the state sS in SS such that the relative position of sS with respect to Cr(ρS ) is the most similar (measured in Euclidean distance) to the relative position of sT with respect to Cr(ρj,T i ) (Line 6).

Identification of Location: We identify the location qS corresponding to qT through the mapping ξ i,ˆi Q (Line 7). As in the introductory example, the mapping ξ 1,1 Q maps the locations qT 0 , qT 1 , qT 2 and qT 3 to the locations qS 0 , qS 1 , qS 2 and qS 3 , respectively (see Figure 4).

Identification of Clock Valuation: For each clock cTl ∈ C φTi , we identify the clock cSk corresponding to cTl through themapping ξ i,ˆi C (Line 9). As in the introductory example, the mapping ξ 1,1 C maps the clocks cT1 and cT2 to the corresponding clocks cS1 and cS2 , respectively (see Figure 4). Then for each clock valuation vT l ∈ V φTi l , we identify the (scalar) clock valuation vS k ∈ V φSˆi k which is the most similar (in scalar value) to vT l (Line 10).

In this way, ¯QS∗ (sS , qS , vS , a) from the source task are transferred to ¯QT (sT , qT , vT , a) in the target task. Finally, we perform Q-learning of T T in the extended state space, starting with the transferred extended Q-functions ¯QT (sT , qT , vT , a).

5 Implementation

In this section, we illustrate the proposed approach on a case study 2 . We consider the introductory example in the 9×9 gridworld as shown in Figure 1. The robot has three possible actions at each time step: go straight, turn left or turn right. After going straight, the robot may slip to adjacent cells with probability of 0.04. After turning left or turning right, the robot may stay in the original direction with probability of 0.03. We first perform Q-learning on the τ-states (i.e., the τ-horizon trajectory involving the current state and the most recent τ - 1 past states, see [Aksaray et al., 2016], we set τ=5) for the source task and the target task. We set α = 0.8 and γ = 0.99. For each episode, the initial state is randomly selected.

We use the first 10000 episodes of Q-learning as the data collection phase. From the source task, all the 46 trajectories with cumulative rewards above 0 are labeled as 1, and 200 trajectories randomly selected out of the remaining 9954 trajectories are labeled as -1. From the target task, all the 19 trajectories with cumulative rewards above 0 are labeled as 1 and 200 trajectories randomly selected out of the remaining 9981 trajectories are labeled as -1.

For the inference problem (Problem 1), we set ϱth = 4 and ζ = 0.95. For Algorithm 1, we set λ = 0.01 and hmax = 2. We use the position of the robot as the state, and the atomic predicates ρ correspond to the rectangular regions in the 9×9 gridworld. For computing the information gain of MITLf formulas, we use the uniform distribution for the prior probability distribution GL. Following the first two steps illustrated in Section 4.2, we obtain the following satisfying formulas:

where

φS reads as "first reach ¯GS during the time interval [1, 15] and stay there for 4 time units, then reach ¯ Y S during the time interval [21, 39]". φT reads as "first reach ¯GT during the time interval [5, 18] and stay there for 5 time units, then reach ¯ Y T during the time interval [24, 39]". The regions ¯GS , ¯ Y S , ¯GT and ¯ Y T are shown in Figure 5 (a) (b). It can be seen that φT is structurally equivalent with φS , hence logical transferability is identified.

For comparison, we also obtain φ′ T without considering the information gain, i.e., by setting λ = 0 in (3):

2 Dur to space limitations, an additional case study can be found in the longer version https://bit.ly/2Zjx7mt.

φ′ T reads as "first reach ¯GT during the time interval [1, 18] and stay there for 4 time units, then reach ¯ Y ′ T during the time interval [24, 40]". ¯GT and ¯ Y ′ T are shown in Figure 5 (c). It can be seen that φT implies φ′ T , hence φ′ T is less informative than φT with respect to the prior probability distribution GL.

We use Method I to refer to the Q-learning on the τ-states. In comparison with Method I, we perform Q-learning in the extended state space with the following three methods:

Method II: Q-learning with φ′ T (i.e., on the extended state that includes the locations and clock valuations of the timed automata constructed from φ′ T ).

Method III: Q-learning with φT .

Method IV: Q-learning with φT and starting from the transferred extended Q-functions.

Figure 6 shows the learning results with the four different methods. Method I takes an average of 834590 episodes to converge to the optimal policy (with the first 50000 episodes shown in Figure 6), while Method III and Method IV take an average of 13850 episodes and 2220 episodes for convergence to the optimal policy, respectively. It should be noted that although Method II performs better than Method I in the first 50000 episodes, it does not achieve optimal performance in 2 million episodes (as φ′ T is not sufficiently informative). In sum, the sampling efficiency for the target task is improved by up to one order of magnitude by performing RL in the extended state space with the inferred formula φT , and further improved by up to another order of magnitude using the transferred extended Q-functions.

6 Discussions

We proposed a transfer learning approach for temporal tasks based on logical transferability. We have shown the improvement of sampling efficiency in the target task using the proposed method.

There are several limitations of the current approach, which leads to possible directions for future work. Firstly, the proposed logical transferability is a qualitative measure of the logical similarities between the source task and the target task. Quantitative measures of logical similarities can be further established using similarity metrics between the inferred temporal logic formulas from the two tasks. Secondly, as some information about the task may not be discovered during the initial episodes of reinforcement learning (especially for more complicated tasks), the inferred temporal logic formulas can be incomplete or biased. We will develop methods for more complicated tasks by either breaking the tasks into simpler subtasks, or iteratively performing inference of temporal logic formulas and reinforcement learning as a closed loop process. Finally, we use Q-learning as the underlying learning algorithm for the transfer learning approach. The same methodology can be also applied to other forms of reinforcement learning, such as actor-critic methods or modelbased reinforcement learning.

Acknowledgements

This research was partially supported by AFOSR FA955019-1-0005, DARPA D19AP00004, NSF 1652113 and ONR N00014-18-1-2829.