Optimal Infinite Temporal Planning: Cyclic Plans for Priced Timed Automata

Venue: icaps-conference_org_ICAPS_2024_Conference
Published: 2023-12-06 14:15:22

Abstract: Many applications require infinite plans ---i.e. an infinite sequence of actions--- in order to carry out some given process indefinitely. In addition, it is desirable to guarantee optimality. In this paper, we address this problem in the setting of doubly-priced timed automata, where we show how to efficiently compute ratio-optimal cycles for optimal infinite plans. For efficient computation, we present symbolic $\lambda$-deduction (S-$\lambda$D), an any-time algorithm that uses a symbolic representation (priced zones) to search the state-space with a compact representation of the time constraints. Our approach guarantees termination while arriving at an optimal solution. Our experimental evaluation shows that S-$\lambda$D outperforms the alternative of searching in the concrete state space, is very robust with respect to fine-grained temporal constraints, and has a very good anytime behaviour.

Main paper: 
 introduction: 
 Temporal planning deals with the problem of finding a (concurrent) plan to achieve a certain goal (Fox and Long 2003; Gigante et al. 2022 ). However, this disregards the resulting state of the system after executing the plan, and how easy it will be to achieve future goals from there. Many planning applications require instead a cyclic schedule, where a system must stay operational while achieving a goal repeatedly (Draper et al. 1999) . Consider for example an assembly line scenario (Asai and Fukunaga 2014) where a large number of units must be produced. A simple approach is to find a plan for producing a single unit and then repeating the plan over and over. However, this may lead to suboptimal plans where no part of the production is parallelised, or even infeasible plans, where after producing some amount the assembly line is left in a state where it cannot produce further units. In such scenarios, we desire infinite plans containing a loop that can be executed arbitrarily many times. Infinite plans have been considered in the context of classical planning with LTL goals (Patrizi et al. 2011) , but here we are interested in finding optimal temporal plans with concurrent and delay-constrained actions.We propose to tackle these applications by finding ratiooptimal cycles in cost-reward timed automata (Bouyer, Brinksma, and Larsen 2004) . Thus, assume that the planning problem under consideration may be modelled as a priced-timed automata (Behrmann et al. 2001; Alur, Torre, and Pappas 2004) , which has been used to model various real-world scenarios (Hune, Larsen, and Pettersson 2001; Fehnker 1999; Niebert and Yovine 2001; Brinksma, Mader, and Fehnker 2002) . The optimal infinite plan has been shown to be a cyclic plan, minimizing the ratio between total cost and reward. This is a very general setting that can, for example, be used to find the schedule that minimizes the monetary cost per produced unit in a factory or that minimizes the amount of time per locations that must be surveyed in a surveillance scenario. Bouyer, Brinksma, and Larsen (2004) showed that finding a plan with optimal cost-reward ratio is possible using the so-called corner-point abstraction, which reduces the problem to a finite doubly weighted graph by discretizing time. However, this approach requires the entire state space to be enumerated in advance and therefore it scales very poorly with respect to the time scale considered. Thus, practical approaches have focused on finding approximate solutions (e.g., population-based methods (Tolonen, French, and Reynolds 2018) ), or analyzing restricted settings, e.g., timed automata with only 1 clock (David et al. 2011) .Our aim is to alleviate the state-space explosion by using priced zones (Larsen et al. 2001 ), a compact representation of sets of states originally introduced in model checking tools for timed automata (Larsen, Pettersson, and Yi 1997) . However, this is not trivial in a cost-reward setting, as symbolic representations make it difficult to determine whether there is a concrete cycle as well as determining the cost and reward the concrete paths they abstract over.We introduce symbolic λ-deduction (S-λD), an anytime algorithm that incrementally finds new cycles with improved ratio. To do so, S-λD reduces the problem to a single priced automaton and explores the state space symbolically using priced zones, avoiding the enumeration of all possible combinations of clock valuations. We show that the approach converges and terminates with a ratio-optimal cyclic plan, proving that no better solution exists.We evaluate S-λD in three scenarios, showing that it is feasible to compute ratio-optimal cycles in different types of practical applications. S-λD has good anytime behaviour, oftentimes finds the optimal cycle faster than the concrete approach, and is far more robust with respect to different time constraints, being almost unaffected by large clock values. 
background: 
 We adopt the formalism used by Bouyer, Brinksma, and Larsen (2004) . A clock is an object that measures the time since it was last reset. A clock valuation u ∈ R C ≥0 over the set of clocks C is a function u : C → R ≥0 assigning a value to each clock. When time passes, it is called a delay, and the value of all clocks increase uniformly. For a delay δ ∈ R ≥0 we denote the updated valuation by u + δ, where(u + δ)(x) = u(x) + δ. Let R ⊆ C be a set of clocks to be reset, then u ′ = u[R → 0] is the new valuation such that u ′ (x) = 0 if x ∈ R, otherwise, u ′ (x) = u(x).We denote by B(C) the set of clock constraints over C obtained by conjunction over atomic constraints of the type x ▷◁ n for x ∈ C, ▷◁ ∈ { ≤, =, ≥ }, and n ∈ N. Let g ∈ B(C) be such a constraint, then we write u | = g when u satisfies g. For example, for the valuation u(x) = 3, u(y) = 1, we have thatu | = x ≤ 3 and u ̸ | = y ≥ 2 ∧ x ≥ 1.Definition 1. A timed automaton over a set of clocks C is a tuple (L, ℓ 0 , E, I), where L is the set of locations, ℓ 0 ∈ L is the initial location, E ⊆ L×B(C)×2 C ×L is the set of edges between locations, and I : L → B(C) assigns invariants to locations.A state of the timed automaton consists of a location and a clock valuation. An edge e = (ℓ, g, R, ℓ ′ ) ∈ E means that the automaton can move from location ℓ to ℓ ′ if the clocks satisfy the guard g, and after taking this edge the clocks in R will be reset. The invariant of a location I(ℓ) is the clock constraints that must be satisfied to be in location ℓ, thus you cannot move into location ℓ if the clock valuation does not satisfy I(ℓ) and if already in ℓ you cannot delay such that the clock valuation no longer satisfies I(ℓ).The semantics of a timed automaton are given by an underlying labeled transition system T * A = (S, s 0 , A, T ), where S = L×R C ≥0 is the set of concrete states, s 0 = (ℓ 0 , 0) is the initial state, where 0 is the valuation mapping all clocks to 0, A = E∪R ≥0 is the set of actions, being either an edge or a time to delay, and T ⊆ S × A × S is the transition relation. We write s α -→ s ′ whenever (s, α, s ′ ) ∈ T and refer to states in this transition system as concrete. The transition relation then contains delay transitions with δ∈ R ≥0 (ℓ, u) δ -→ (ℓ, u + δ) if ∀0 ≤ δ ′ ≤ δ. u + δ ′ | = I(ℓ),and edge transitions with e = (ℓ, g, R, ℓ′ ) ∈ E (ℓ, u) e -→ (ℓ ′ , u[R → 0]) if u | = g and u[R → 0] | = I(ℓ ′ ).We now extend timed automata by also including costs and rewards for edges and delays.Definition 2. A Cost-Reward Timed Automaton (CRTA) A = (L, ℓ 0 , E, I, c, r) is a timed automaton extended with two functions c, r : L ∪ E → N 0 , which represent cost and reward rates for locations and edges.A CRTA A = (L, ℓ 0 , E, I, c, r) induces a Cost-Reward Weighted Transition System (CR-WTS) T A = (S, s 0 , A, T, cost, reward), a labeled transition system extended with functions cost, reward : T → R, which assignshort x ≤ 3 c ′ = 1 r ′ = 10 long x ≤ 5 c ′ = 1 r ′ = 3 slow x ≤ 3 c ′ = 1 r ′ = 0 fast x ≤ 3 c ′ = 1 r ′ = 0 x := 0 y := 0 x ≥ 3, x := 0 x ≥ 2 x ≥ 1 x := 0 y ≥ 5 x := 0Figure 1: CRTA of a lawnmower example. Resets are denoted by "x := 0", cost increments by "c += n" (or reward by "r += n"), the cost/reward rates of delaying in locations are denoted by "c ′ = n" (and "r ′ = n" for reward). The initial state is marked by a sourceless incoming edge.cost and reward to transitions.cost((ℓ, u) α -→ (ℓ ′ , u ′ )) = c(ℓ) • δ if α = δ ∈ R ≥0 c(e) if α = e ∈ Eand dually for reward.Let π = s 0 α0 -→ s 1 α1 -→ . . . αn-1---→ s n be a finite execution in a CR-WTS (S, s 0 , T, cost, reward) consisting of concrete states. The cost and reward functions extend to finite executions straightforwardly as Cost(π) = n i=1 cost(s i-1 , α i-1 , s i ) and dually for Reward. We define the cost-reward ratio for a finite execution, where Reward(π) ̸ = 0, as Ratio(π) = Cost(π) Reward(π) . We now consider the case of an infinite execution, Π. Let Π n denote the finite prefix execution of Π with length n. The ratio of the infinite execution Π is then defined by Ratio(Π) = lim inf n→+∞ Ratio(Π n ), provided this limit exists. The optimal ratio for a CR-WTS A is indicated byθ * = inf { Ratio(Π) | Π is an infinite execution in A } . An infinite execution Π is ratio-optimal if Ratio(Π) = θ * .We make the restriction that automata must not contain any so-called Zeno-cycles, i.e. all infinite executions must also use an infinite amount of time. Similarly, they must also be reward-diverging, meaning all infinite executions that are time-divergent accumulate infinite reward. Finally, we will assume that the automata are bounded, i.e. there exists a C max ∈ N s.t. no clock ever has a value larger than C max . Behrmann et al. (2001) shows that any unbounded timed automaton can be converted into an equivalent bounded timed automaton, thus no expressiveness is lost.An interesting subclass of CRTA is when reward corresponds to the time elapsed (i.e., there are no transition rewards and the reward rate at each location is the same). Ratio-optimal plans correspond then to operating the system with lowest cost per time unit. In this case, not having Zeno-cycles is the same as reward-divergence. Example 1 Consider the example CRTA shown in Figure 1 , which models a lawnmower, whose job is to tend a lawn by keeping it nicely short. When it decides that the grass is too long (after some 1 to 3 time units) it transitions to the long location. Here it waits for an additional 2 time units, but receives less reward. Next, it has the option of whether to mow fast or slow by going to their respective location. The slow approach takes 3 units of time, and the fast approach takes between 2 and 3 units of time. The reward models the quality of the lawn, and the cost models the time. One example of a cycle is to delay 3 units of time in short, go to long, delay 2, go to fast, delay 3, and complete the cycle by returning to short. This cycle accumulates 8 cost and 36 reward, and thus it has a ratio of 8 36 ≈ 0.22. The optimal plan has a ratio of 11 60 ≈ 0.18 and it involves a longer loop that alternates between slow and fast.For simplicity we describe our techniques as operating on the full timed automata, as they are agnostic of the exact formalism used. In practice more compact representations can be used. Our implementation is based in UPPAAL (Larsen, Pettersson, and Yi 1997) , which uses a representation based on networks of synchronized timed automata. This can be exponentially more compact than the full CRTA, which is only generated in an on-the-fly manner.Corner-Point abstraction Bouyer, Brinksma, and Larsen (2004) introduced cornerpoint abstraction, a method for discretising the clock valuation space by only considering points that are integer-valued. In a bounded timed automata this reduces to a finite state space which can be represented as a doubly weighted finite graph. They showed that this abstraction is sound and complete. There is a slight distinction in our model as, for simplicity, we only allow non-strict clock guards, which simplifies the corner-point abstraction.The intuition for why it suffices to consider integer valuations only, is that all clock guards have integer bounds and the minimum of a linear fractional function with linear constraints is attained in the corner-points of the zone that the constraints define, hence at integer valuations.We call a cycle with integer-valued clock valuations a discrete cycle. Bouyer, Brinksma, and Larsen (2004) show that there are only finitely many discrete simple cycles and there is always such a cycle that is ratio-optimal.Wielding the corner-point abstraction, a simple approach is to construct the entire corner-point abstracted state-space as a doubly weighted graph, then use an existing algorithm for the ratio-optimal cycle problem, such as Howard's policy iteration algorithm (Howard 1960; Dasdan, Irani, and Gupta 1999) . We use this as a base-line for our symbolic approach. 
anytime λ-deduction algorithm: 
 The main issue with using the corner-point abstraction is that often the size of the graph grows exponentially with the number of clocks. Therefore, constructing the entire graph before starting the search is a huge bottleneck. Instead, we aim to perform an on-the-fly exploration of the state space in order to find the optimal-ratio cycle. However, when dealing with both cost and reward, a problem arises because the costs and rewards of reaching a state can be incomparable. For example, a cost/reward of 1/1 is not necessarily better or worse than 2/3 because, depending on the rest of the path to close the cycle, both could be the minimum ratio. If the rest of the cycle has cost/reward 1/0, then the better ratio is 3/3, and if it has 0/2, then the better ratio is 1/3. While this could be dealt with multi-objective search (Fränzle et al. 2022; Larsen and Rasmussen 2008) , maintaining the entire Pareto front for each clock valuation is unnecessary because we are interested on a single objective: the minimum ratio. Gondran and Minoux (1995) show how to overcome this problem by combining the cost and reward into a single weight, and then incrementally finding better solutions (according to the current weight) until the optimal is found. This style of algorithm works by maintaining the ratio of the best solution found so far, λ. The weight at each iteration isw λ = Cost -λ • Reward. Proposition 3. A cycle x has negative λ-deducted weight if and only if Ratio(x) < λ. Proof. Cost(x)-λ•Reward(x) < 0 ⇐⇒ Cost(x)Reward(x) < λ. This suggests the method used in Algorithm 1: First, pick any cycle x from the CRTA, and let λ := Ratio(x) = Cost(x) Reward(x) . Then, find a cycle x ′ s.t. w λ (x ′ ) < 0, and update λ := Ratio(x ′ ). This is repeated until no such x ′ exists, at which point an optimal solution has been found.To use this approach in our setting, we need a method for finding cycles with negative λ-deducted weight. We therefore introduce a transformation of the original cost-reward automaton into a λ-deducted single priced timed automaton.Definition 4. Let A = (L, ℓ 0 , E, I, c, r) be a CRTA. The λ-deducted single priced timed automata of A is A λ = (L, ℓ 0 , E, I, w λ ), where w λ (a) = c(a) -λ • r(a) for a ∈ L ∪ E.Note that the weight of any path in A λ corresponds to the λ-deducted weight of the path in A. This follows from the semantics of A and the additive nature of the λ-deducted weight. We say a cycle in A λ is a negative-weight concrete cycle if the summed weight of the cycle is negative.Algorithm 1 shows an abstract algorithm for finding ratiooptimal cycles using the λ-deducted automaton. Theorem 5. Algorithm 1 terminates, and returns a ratiooptimal concrete cycle, if one exists, otherwise NO CYCLE.Proof. There are finitely many simple discrete cycles. At each step λ decreases. Thus at some point there will be no simple discrete cycle with ratio lower than λ.It is worth noting that, at each iteration, it suffices to find any negative cycle, not necessarily one with minimum (negative) cost. In fact, finding cycles with lower weight does not guarantee faster convergence. For example, with λ = 3, a cycle with cost/reward 3/2 has weight w λ = 3-3•2 = -3, while a cycle with a better cost/reward ratio 1/1 has weightw λ = 1 -1 • 2 = -1. 
symbolic λ-deduction: 
 All that remains to instantiate the λ-deduction algorithm is an effective and efficient way for finding negative-weight concrete cycles in A λ . This could be done with an explicit search of the corner-point abstracted state space. However, Algorithm 1: λ-deduction algorithm.input : A bounded and strongly reward-divergent CRTA A = (L, ℓ0, E, I, c, r) over the clocks C. output: A ratio-optimal concrete cycle, if one exists, otherwise NO CYCLE. as the number of states grows exponentially with the number of clocks, we utilise a symbolic representation of the clockspace.1 if A has no cycle then 2 return NO CYCLE 3 C λ := any cycle in A 4 λ := Ratio(C λ ) 5 while A λ has negative-weight simple discrete cycle C do 6 λ := Ratio(C) 7 C λ := C 8 return C λ y x 0 1 2 3 4 0 1 2 3 4 x -y ≥ 0 y ≤ 2 x ≥ 1 x ≤ 3 y x 0 1 2 3 4 0 1 2 3 4In model checking, zones are commonly used as a symbolic representation of a subset of the clock space (Daws et al. 1995; Larsen, Pettersson, and Yi 1997) . A zone over a set of clocks C is defined by a conjunction of constraints, which can be upper or lower bounds on either the value of clocks or the difference between two clocks. Thus, the zone represents a convex subset of |C|-dimensional Euclidean space.As we are also dealing with a price, namely the λdeducted weight, we use priced zones (Larsen et al. 2001) . Priced zones extend zones with a price function, an affine function from the clock values to the price of reaching that particular state. Figure 2 (left) shows an example of a zone. Assuming that the price function isw green (u) = -1 • u(x) + 2 • u(y) + 1, the price of reaching the valuation (x = 2, y = 1) is w green (2, 1) = -1 • 2 + 2 • 1 + 1 = 1.A symbolic state S = (ℓ, Z, w) consists of a location, a zone and a price function. We say that a concrete state s = (ℓ, u) is in S, denoted by s ∈ S, iff u ∈ Z.Zones themselves are represented using difference bound matrices (Dill 1989; Bengtsson and Yi 2003) , a data structure for efficient storing and performing necessary operations on zones. We define the functions Post e and Post ϵ that return, for a given symbolic state S = (ℓ, Z, w), the symbolic successors after using the discrete edge and delay actions, respectively. The delay successors of a symbolic state, Post ϵ (S) reflect the lowest price of reaching a specific point the successors from some point in S. Each delay action has an associated delay rate r. The slope of the delay trajectory of a priced zone is the price of increasing all clocks by 1 according to w, let us call this q. There are only two ways to reach a valuation to consider: (i) delaying as much as possible in this delay action; (ii) delaying the least possible. We should choose (i) when r ≤ q and choose (ii) when r ≥ q.The result of delaying can be represented as one or more symbolic states. The example of Figure 2 (right) shows the successors after a symbolic delay action on the zone depicted in the left, assuming the location ℓ has an invariant x ≤ 4, and that we delay in a location with weight-rate r = 3. In this case, the slope of the delay trajectory of the green zone is q = 1 (i.e. the sum of the coefficients for u(x) and u(y)); thus we should delay the least possible. Therefore, only the valuations not already reachable from green are represented in separate symbolic states with new zones. The two new zones, red and blue (respectively, vertical lines and dots), have price functions w red (u) = -1•u(x)+1•u(y)+2 and w blue (u) = 1 • u(x) + 2 • u(y) -5. There are similar considerations for the discrete edge successor; we refer the reader to Larsen et al. (2001) for full details.We write S α -→ S ′ whenever S ′ ∈ Post α (S) for some α ∈ E ∪ {ϵ}. When the particular action does not matter, we simply write S → S′ . A symbolic path Π = S 0 α0 -→ S 1 → • • • αn-1---→ S n is sequence of symbolic transitions. We use the notation S 0 ⇝ S n whenever there exists a symbolic path from S 0 to S n . We say that a concrete path π is in a symbolic path Π, denoted π ∈ Π, when π and Π agree on the discrete transitions and all concrete states in π are contained in the corresponding symbolic state in Π. Definition 6. A symbolic path Π is a symbolic cycle iff there exists a concrete cycle π ∈ Π. A symbolic cycle Π is a negative-weight symbolic cycle iff there exists a negativeweight concrete cycle π ∈ Π.We first consider the problem of, given a symbolic path, how to determine whether it is a (negative-weight) symbolic cycle. This is an important question, as we want to symbolically search for negative-weight concrete cycles. However, this is not readily apparent as there may be an overlap in the start and end zones but no concrete cycle from one point back to itself. Furthermore, despite priced zones keeping the price of reaching any point in the end zone, we cannot determine the price of a particular path from start to end. For a given end valuation, we only know the cheapest price of reaching this valuation, but not from which valuation a path with this price is realisable from. Next, we will show how to extract the best concrete cycle from a symbolic path, both w.r.t. to ratio and λ-deducted weight.Extracting the best concrete cycle from a symbolic cycle consists of finding optimal concrete delays for the symbolic delays. However, since symbolic states abstract over many concrete states, there are also concrete cycles that do multiple revolutions inside the symbolic cycle. Specifically, given a symbolic cycle Π, we want to find the best concrete cycle π s.t. there exists a k for which π ∈ Π k , where Π k is Π concatenated onto itself k times. Theorem 7. Let Π = (ℓ, Z 1 ) ⇝ (ℓ, Z n ) be a symbolic cycle. Then for all k > 1, the optimal concrete cycle in Π 1 has the same ratio as the optimal concrete cycle in Π k . Proof sketch. Let π k be a cycle in Π k . We will then show how to construct a cycle π 1 ∈ Π 1 that has the same ratio. Letπ 1 π 2 • • • π k = π k be the partitioning of π k s.t. π i ∈ Π for 0 < i ≤ k.We then construct π 1 as a convex combination of all π i . For a scalar η ∈ R ≥0 and a valuation u ∈ R C ≥0 , we define(η • u)(x) = η • u(x) for x ∈ C. Also, we define (u + u ′ )(x) = u(x) + u ′ (x) for x ∈ C.Let η = 1 k , we then construct π 1 as the convex combination, such that each state (ℓ j , v j ) ∈ π 1 has v j = k i=1 u i j where (ℓ j , u i j ) ∈ π i . The delays are then also the convex combination of the delays of all π i . It can be shown that π 1 is a valid cycle and has the same ratio as π k . Since the zones are convex, π 1 ∈ Π. The reset operation also works in the convex combination because they all agree that the reset clock is 0. The ratio is the convex combination of all of the ratios, since η = 1 k it is the same as the ratio of π k .Corollary 8. Let Π = (ℓ, Z 1 ) ⇝ (ℓ, Z n ) be a symbolic cycle in a single weight timed automata. Then for all k > 1, there exists a concrete cycle with weight w in Π 1 if and only if there exists a concrete cycle with weight w • k in Π k .Proof. This follows easily from Theorem 7. We can simply pretend that Reward(Π) = 1, then there is a cycle π ∈ Π with Ratio(π) = w 1 iff there is a cycleπ k ∈ Π k with Ratio(π k ) = k•w k .With this, we know that we can limit ourselves to finding cycles of a single revolution in the symbolic cycle; thus, we will now describe how to extract a concrete cycle. We will first focus on extracting the best concrete cycle w.r.t. costreward ratio. Tolonen, French, and Reynolds (2018) show how this is achieved by optimisation the delays of the symbolic cycle using linear-fractional programming (Charnes and Cooper 1962) ; here, we give only an overview of the procedure. We optimise the delays to minimise over the fractional objective that is the cost-reward ratio of the cycle. For a symbolic cycle Π, the core idea is to construct timestamps t i for each α i in Π, representing the time elapsed since the action α 0 . Additionally, a timestamp t n+1 is added as the end of the cycle, where n = |Π|, i.e. the duration of the cycle. Recall that zones are constructed from difference constraints on clock values. Therefore, zones can be transformed into constraints on timestamps by translating a clock value at index i into a difference constraint on the current timestamp and the timestamp at which it was last reset. For a constraint x ≤ n at index i, we find the index j that is the latest index (w.r.t. i) where x was reset. Then, if j ≤ i the constraint is equivalent to t i -t j ≤ n, and if j > i, i.e. if x was only reset in the previous iteration of Π, then the constraint is equivalent to t i + t n+1 -t j ≤ n.We can therefore determine whether a symbolic cycle is negative by optimising for the lowest weight concrete cycle and seeing if it is negative, or alternatively, optimize for the best cost-reward ratio concrete cycle and checking if it is less than the current λ (i.e., the best ratio found so far). The latter is preferred, as we might as well extract the best cost-reward ratio cycle, as this will maximise the improvement of λ.We are now ready to present our algorithm for finding negative-weight cycles. Algorithm 2 performs best-first search, where each search node corresponds with a symbolic state. We maintain a parent pointer, Parent, that maps each discovered symbolic state to its predecessor. Specifically, the Parent pointer returns for S either a pair (S ′ , α), where S ′ is the predecessor and e ∈ E is the action, s.t. S ′ e -→ S, or the special symbol NIL when S is the initial state.On line 5, the algorithm extracts and expands a minimum element from Waiting, according to some ordering. The order chosen has no consequence on termination and correctness of the algorithm, but it may affect the efficiency. We suggest to choose a state containing the minimum weight valuationfrom the intuition that cheap valuations are more likely to produce negative cycles.Every time a new successor is generated, we check whether it belongs to a negative-weight cycle (line 10) by calling the subroutine FI N D-NE G A T I V E-CY C L E. This recursive subroutine follows the Parent pointer backwards, checking whether the suffix is a cycle. This is done with the linear-fractional program for all symbolic paths that satisfy some necessary conditions (e.g. there is some concrete state s such that s ∈ S 1 and s ∈ S n ). Thus, FI N D-NE G A T I V E-CY C L E returns a negative-weight symbolic cycle if one is found, otherwise it will eventually reach NIL and return NO CYCLE.The key problem is when to stop searching. It may seem that duplicate detection is safe, i.e., if we return to a state (ℓ, Z, w) with the same location and zone, there is no point in continuing the search. However, that is not the case. Duplicate pruning ignoring w, may incorrectly prune the optimal cycle, which may pass multiple times by the same symbolic state. Proposition 9. There exist CRTAs such that the optimal concrete cycle is contained in a non-simple symbolic cycle. Proof sketch. Consider the automaton:a x ≤ 1 r ′ = 5 b x ≤ 2 c ′ = 100 c x ≤ 2 r ′ = 1 c ′ = 1 e 1 x = 1 e 2 x := 0 e 3 x ≥ 1 e 4 x ≥ 2, x := 0The optimal concrete cycle is (a, 0)1 -→ (a, 1) e1 -→ (b, 1) e2 -→ (c, 0) 2 -→ (c, 2) e3 -→ (b, 2) e4-→ (a, 0), with a ratio of 2 7 . However, this is in the non-simple symbolic cycle S 0 → S 1 → S 2 → S 3 → S 4 → S 5 → S 3 → S 0 , with both S 0 and S 3 appearing twice. There are two simple symbolic cycles S 0 → S 1 → S 2 → S 3 → S 0 and S 3 → S 4 → S 5 → S 3 , however, the optimal concrete cycles in these only achieve a cost-reward ratio of 100 5 and 1 1 , respectively. Note that this does not contradict Theorem 7, as both parts of the cycle are using different edges. 9 insert S ′ into Waiting 10 if NE G-CY C L E(S α -→ S ′ ) returns cycle C then 11 return C 12 return NO CYCLE 13 Function NE G-CY C L E(S1 α 2 --→ • • • αn --→ Sn) 14 if S1 α 2 --→ • • • αn --→ Sn is a negative-weight cycle then 15 return best concrete cycle in S1 α 2 --→ • • • αn --→ Sn 16 if Parent(S1) ̸ = NIL then 17 (S, α) := Parent(S1) 18 return NE G-CY C L E(S α -→ S1 α 2 --→ • • • αn --→ Sn) 19 else 20 return NO CYCLETo ensure termination, we define a domination criteria to prune symbolic states if they have a higher price everywhere. Definition 10. A priced symbolic state S = (ℓ, Z, w) dominates another S ′ = (ℓ ′ , Z ′ , w ′ ), denoted by S ⊑ S ′ , iff (i) ℓ = ℓ ′ , (ii) Z ⊇ Z ′ , and (iii) w(u) ≤ w ′ (u) for all u ∈ Z ′ .When searching, we do not expand a state S if we have already seen a state S ′ where S ′ ⊑ S. On line 7, only successors where no dominating state has already been discovered are added to Waiting. This ensures that an optimal cycle will not be pruned, and it is sufficient to ensure that the algorithm terminates. If prices keep becoming lower and lower, then a negative cycle will be found. If there is no negative cycle, eventually no non-dominated state will be left, and the algorithm will return NO CYCLE. Lemma 11. The subroutineFI N D-NE G A T I V E-CY C L E in Algorithm 2 terminates.Proof. We first argue that there exists a constant w min for A λ s.t. any symbolic path that contains a concrete path with weight less than w min must contain a negative-weight concrete cycle. Let T cp = (S cp , s 0 , A, T cp , cost, reward) be the CR-WTS induced by the corner point abstraction of the automaton A, i.e. containing only discrete states and transitions, then w min = { w λ (t) | t ∈ T cp , w λ (t) < 0 }, where w λ (t) = cost(t) -λ • reward(t), i.e. the sum of the weight of all negative λ-deducted transitions. Any concrete path with weight less than w min must use at least one negative edge more than once, and therefore, it contains at least one concrete cycle. At least one of these cycles must be negative.Now, let S be the set of all priced symbolic states and S ≥wmin = { (ℓ, Z, w) ∈ S | ∀u ∈ Z. w(u) ≥ w min }. We now argue that (S ≥wmin , ⊑) is a well-quasi order, i.e. there exists no infinite descending sequence where the states are not dominated by a previous state. For a bounded priced timed automaton, there is only a finite number of (unpriced) zones, thus a zone must eventually repeat in an infinite sequence. The minimum of a priced zone is attained in an integer point, therefore, we can limit ourselves to study the cost plane only in the finite number of integer points. Let u ∈ Z be an integer point of zone Z, π be a minimum λ-deducted weight path to u, and λ = a b for a ∈ Z and b∈ N + . Let Q • b = { q ∈ Q | ∃c ∈ Z. q = cb } be the set of rationals that can be written with b as denominator. The λdeducted weight of reaching the integer point isw λ (π) = Cost(π) -a b • Reward(π) = Cost(π)•b-a•Reward(π) b, and since Cost(π) and Reward(π) are integer-valued (known from corner-point abstraction),w λ (π) ∈ Q • b . For all b ∈ Z + , Q •b is nowhere dense in R and thus any infinite descending sequence must tend towards negative infinity. Thus, the weight of the integer points cannot keep improving ad infinitum, as it will become less than w min , and since there are only finitely many integer points eventually no point can improve further. This, in conjunction with the finiteness of zones, shows that (S ≥wmin , ⊑) is a well-quasi order. The argument is similar to Dickson's Lemma (Kruskal 1972) .These properties guarantee that our algorithm terminates. Firstly, the subroutine FI N D-NE G A T I V E-CY C L E terminates either when Waiting = ∅ or when NE G-CY C L E returns a cycle. The if-statement on line 7 ensures that we never added a state to Waiting that is dominated by a previously expanded state. Thus only a finite amount of dominated states will be expanded. If no state is ever expanded that contains a point cheaper than w min , then there exists no infinite descending sequence for ⊑, and thus the algorithm must terminate. Otherwise, whenever any state containing a point cheaper than w min is expanded, then there must be a negative cycle present in the parent pointer, so therefore it terminates. The subroutine NE G-CY C L E is called whenever a state is added to Waiting, thus when the parent pointer contains a cycle, it is detected. We will assume that the linear programming solver finds a discrete cycle. However, if it does not, this does not affect convergence of the algorithm, as we know from corner-point abstraction (Bouyer, Brinksma, and Larsen 2004 ) that there exists an equivalent discrete cycle with the same cost-reward ratio. Symbolic λ-deduction, i.e., Algorithm 1 using Algorithm 2 as a sub-routine in line 5 is complete, sound, and optimal.Theorem 12. The symbolic λ-deduction algorithm terminates, and it returns a ratio-optimal concrete cycle, if one exists, otherwise NO CYCLE.Proof sketch. We know that Algorithm 1 is correct and terminates (Theorem 5), therefore, it suffices to show that FI N D-NE G A T I V E-CY C L E is correct and terminates. We handled termination already in Lemma 11. Here we prove the correctness as soundness and completeness.Soundness: if FI N D-NE G A T I V E-CY C L E returns a cycle then it is a negative-weight concrete cycle in A λ . The algorithm only expands reachable states and only returns a cycle if it is negative. The concrete cycles are extracted by linear program optimisation, and by Corollary 8, we need only consider one revolution in each symbolic cycle. Thus, the cycle is reachable and has negative-weight.Completeness: if there exists a negative cycle in A λ then FI N D-NE G A T I V E-CY C L E returns a cycle. Recall from the proof of Lemma 11, that if there exists a negative cycle, then there is a weight w min s.t. reaching a weight below this can only be done with a negative cycle. Also, a negative cycle always makes the weight arbitrarily cheap. From the priced zones, we know that there is always a symbolic path to reach any reachable state that is descending w.r.t. ⊑; i.e. no symbolic state is dominated by a preceding state in the path. Thus, the descending symbolic path to reach the state with weight less than w min , must eventually be found by the algorithm, and this must contain a concrete cycle. Thus the symbolic cycle will be discovered because we check of a negative cycle every time a state is added to Waiting. 
experimental evaluation: 
 We conduct experiments comparing symbolic λ-deduction (S-λD) against the baseline CP-MCR. CP-MCR constructs the entire corner-point abstracted concrete state space and then uses existing techniques to find a ratio optimal cycle in the doubly weighted graph. We implemented both algorithms on top of UPPAAL 4.1 (Larsen, Pettersson, and Yi 1997) . CP-MCR uses the Boost library's solver for minimum cycle ratio problems, which is based on Howard's algorithm (Dasdan, Irani, and Gupta 1999) . All experiments were run on a cluster with AMD EPYC 7551 32-core processors, with a 10-minute time limit and 10GB memory limit. The data from the experiments and the scripts for generating the figures and tables will be made publicly available.We conduct experiments in three different domains: surveillance, job scheduling and volunteer. The problems are modelled in UPPAAL as networks of timed automata. Larsen, Pettersson, and Yi (1997) gives a thorough description of how modelling in UPPAAL works. We extended UP-PAAL's parsing module to allow for both costs and rewards.Surveillance In this domain one or more agents must surveil different places. If a place has not been surveilled for 10 units of time, the cost of the place is increased. The agents can either be waiting or surveilling, with the former giving more reward. At some point the agent can choose to surveil a place, this takes between 5 to 10 units of time and resets the cost of the place to its initial value. We denote instances of this problem as S a,p , where a is the number of agents and p is the number of places.Job Scheduling This is a small extension to the scheduling problem by Behrmann, Larsen, and Rasmussen (2005) . 1 : Results of comparison between S-λD and CP-MCR in terms of time in seconds until finding the first (nonoptimal) solution (t f ), the optimal solution without proving optimality (t s ), and until termination (t opt ). OOT means that the time limit was exceeded (the memory limit was never exceeded). The States column indicates the number of concrete (for CP-MCR) and symbolic states (for S-λD).We made it cyclic, adding a reward for completing jobs. The model concerns with scheduling a set of jobs on specific machines. Each job needs to serially perform two tasks on two specific machines for an amount of time, and it has a frequency at which it needs to be repeated (e.g., job A needs to use 10s on machine 1 and then 5s on machine 3, and the job must be completed every 60 seconds). Completing the task provides reward and running the machines has a cost. We denote instances of this problem as J m,j , where m is the number of machines and j is the number of jobs.Volunteer This is a scheduling problem which concerns volunteers balancing their university work while maintaining a supply of cold drinks in the refrigerators. The refrigerator can store up to 4 items, which can be withdrawn by the consumers and volunteers, yielding reward. A volunteer can decide to walk to the refrigerators to refill them, this adds to the cost and spends time. The consumers start as active members,but become inactive if they do not withdraw an Figure 3 : 3a shows the sub-optimality ratio over time for S-λD (black, solid) and CP-MCR (red, dashed). Figures 3b and 3c show the time of CP-MCR and S-λD on J 2,2 , V 1,1,2 and S 1,2 when scaling all clock constants.item within a given time interval. An inactive consumer no longer withdraws items and does not generate any reward. The volunteers earn reward by working in their group room, as well as when they withdraw items. We denote instances as V f,v,c , where f is the number of refrigerators, v is the number of volunteers, and c is the number of consumers.We first analyze scalability with respect to the number of objects, i.e., the number of concurrent timed automata and thus the number of locations and clocks in the full CRTA. All clock constants in invariants and guards are small (≤ 15), and are kept constant across all instances of the domain. Table 1 shows the results. Overall, we see that S-λD clearly outperforms CP-MCR in the job and surveil domains, solving more problems and being significantly faster and with lower memory usage. We also note that on S 1,7 , symbolic λdeduction finds that there is no cycle, as a single agent cannot surveil seven places within the time constraints. However, CP-MCR outperforms S-λD on volunteer. This is partially due to a larger number of iterations (up to 22 in V 2,1,2 ) finding improving cycles, and due to the large length of the optimal cycle (up to 416/7118 steps in V 1,1,2 /V 1,1,3 , where as in other domains are only up to 25 steps). Contrary to CP-MCR, S-λD uses different states in each iteration, leading to nearly an order of magnitude more states, even though S-λD's states are using priced zones and thus correspond to multiple explicit states. The number of states gives a clear indication of why S-λD performs poorly on the volunteer domain. S-λD searches nearly an order of magnitude more states, even though S-λD's states are using priced zones and thus correspond to multiple explicit states.An important advantage of S-λD is its good anytime behaviour. As it immediately starts searching for cycles, it can always return the best found cycle so far, before converging on the optimal. Notably, S-λD always found a (possibly non-optimal) solution in few seconds, and oftentimes found the optimal solution a lot sooner than its termination proving that no better solution exists. Even in the volunteer domain, where S-λD performs poorly, it finds a decent solution before CP-MCR finds any. CP-MCR also incrementally improves on the best found ratio, however before being able to do so, it needs to spend a lot of effort to expand the entire state-space. Figure 3a shows the best ratio found along the search for the most difficult instance of each domain where both algorithms finished. S-λD excels in this regard, finding a solution in less than one tenth of a second in most cases, whereas CP-MCR sometimes fail to find any solution.Finally, we analyze the performance of the algorithms when scaling the size of the clock constants. To that end, we fixed a single instance per domain and scaled all constants in the model by a factor. Additionally, we add 1 to the constants to remove large common divisors, which means that the problem can no longer be reduced to the original by simply dividing by the scaling factor. Figure 3 shows that CP-MCR suffers a large increase in run-time when scaling the clock constants. In contrast, scaling the clock constants does correlate with the run time of symbolic λ-deduction. This is not surprising as scaling can result in a polynomial increase in the number of discrete states in the underlying transition system, which has a direct proportional increase in the number of vertices in the doubly weighted graph of CP-MCR. Contrarily, scaling the size of the constants does not have a direct impact on the number of symbolic states to explore, and in most cases it only increases the size of the zones. However, adding 1 to the constants after scaling sometimes changes the solution space, thus we also see some fluctuations, especially in the volunteer domain. 
conclusion: 
 We introduced symbolic λ-deduction, a novel approach for finding ratio-optimal cycles in cost-reward timed automata. Our approach combines the cost and reward functions into a single weight, circumventing some significant barriers that arise in the doubly priced setting. S-λD incrementally improves the best found cycle, searching with priced zones. We proved that it converges on an optimal solution.Our experiments show that S-λD outperforms the baseline, CP-MCR, in many cases, except when the symbolic representation is inefficient and leads to a larger number of explored states. However, even in those cases, S-λD is far more robust with respect to large values in the temporal constraints. 
 
 Appendix:  


Decision: There is an overall positive consensus about this work, which appears rather novel, interesting, well written and solid. The reviewers raised some issues, which the author response seems to have addressed in a satisfactory way. In case of acceptance, I recommend the authors to suitably incorporate their responses in the paper.

Reviews: review: strength_weakness: strength_weakness: It would be helpful to have a discussion of the differences between priced TAs and cost-reward TAs, e.g., why a cost-reward TA cannot be reduced to a priced TA by setting the cost to the ratio. This would be important in particular because there are symbolic methods for priced TAs and it remains unclear why these are not applicable to cost-reward TAs.

Minor comments:
* In the proof of Theorem 7, there seems to be a missing eta in the definition of v_j.
* Below Corollary 8: 'times-tamps'
* also p 5, right: 'valuationfrom' (missing space)
* p7, right: 'members,but' (missing space)

--------
Post Rebuttal:
The rebuttal has clarified my concerns. It would be important that the authors include a brief discussion comparing priced TAs and cost-reward TAs.
questions: questions: 1. Are cost-reward TAs more expressive than priced TAs with a single price?
2. Similarly, can the evaluated domains also be modeled as priced TAs? If so, have you compared your approach to symbolic approaches for priced TAs, in particular (Larsen et al., 2001)?
strength_weakness: strength_weakness: The experimental evaluation is convincing, as I said, but on the reproducibility side there are no details on the implementation itself, nor on whether it will be made available for further study.
questions: questions: N/A
strength_weakness: strength_weakness: 1.	The paper does not discuss in detail the reasons for the poor performance of S-λD in certain domains (e.g., the Volunteer) and possible ways to improve it.
2.	In analyzing the performance of the algorithm when scaling the size of the clock constant, it is not clear exactly why adding 1 to the constant after CP-CRM scaling changes the solution space.
3.	The relevant literature mentioned in the paper, such as Patrizi et al. 2011, David et al. 2011, etc., has relevant methods and domains that can be used in the experiments of this paper. The experimental evaluation of this paper needs to add domains and comparative methods.
questions: questions: 1.	Why does S-λD perform poorly in the volunteer domain compared to the Surveillance and Job Scheduling domains?
2.	Is it possible to add more domains for experimental comparisons to be more convincing?
3.	Is it possible to add more comparisons with existing methods to the experimental evaluation, such as the methods mentioned in the paper Tolonen, French, and Reynolds 2018, David et al. 2011, etc.?