Transforming Robotic Plans with Timed Automata to Solve Temporal Platform Constraints

1 Introduction

When using planners to solve robotic tasks, a programmer has to model the domain of interest. However, it is often problematic to specify the behavior of a robot based on highlevel domain features alone, as lower-level components may impose constraints on the executability of high-level actions. As an example, we consider a simple robot that can move around, and pick up as well as put down objects. For highlevel reasoning purposes, it may suffice to only consider the actions put, pick, and goto. When actually operating on the robot, additional details need to be taken care of, e.g., the perception unit needs to be enabled when picking an object. As the camera needs some time to initialize, it needs to be enabled a few seconds before it is used. When moving, the robot should disable its perception unit to save computational resources. In this scenario, the perception control cannot be handled within low-level implementations easily without either wasting time at each pick (turning it on when the robot decides to pick, then wait until it is ready) or wasting resources (turning it on when it is unnecessary). The essential problem here is that the perception handling is dependent on the context determined by the high-level reasoner.

These low-level constraints could be considered directly by the high-level planner. However, this would considerably increase the domain size and thus impair planner performance. Also, it goes against separation of concerns, as the high-level planning domain directly incorporates low-level platform details. Thus, a separation of high-level reasoning and robotspecific actions is desirable [Hofmann et al., 2018].

In this paper, we instead propose a plan transformation based on timed automaton (TA) reachability analysis. We model each robot platform component as a TA and define constraints on the platform model using a subset of Metric Temporal Logic (MTL). The MTL constraints connect the high-level plan with the robot platform, e.g., by requiring that the camera is turned on two seconds before the robot performs the action pick. Given a high-level plan, we first construct a TA that represents the plan. Next, we extend the constructed TA by replacing each state by a copy of the platform model, while removing any edges that violate a constraint. By applying reachability analysis on the constructed TA, we obtain a sequence of high-level and low-level actions along with execution times that satisfy all constraints.

In the remainder of this paper, we first summarize related work, before we address some core design decisions of our proposed transformation. Then, we summarize the formalism of MTL and TAs, before we describe how to encode the problem as a reachability task on TAs. We evaluate our approach on logistics robots as well as on a domestic service robot, before we conclude.

2 RelatedWork

Task and motion planning (TAMP) combines high-level task planning with low-level motion planning, e.g., with an interface between task and motion planner to effectively combine off-the-shelf planners [Srivastava et al., 2014], by extending the FF heuristics for geometric reasoning [Garrett et al., 2015], or by using constraint programming to guide the high-level search with geometric [Gravot et al., 2005; Dantam et al., 2016] and temporal constraints [Erdem et al., 2011]. In contrast to our proposed approach, TAMP never extends but instead constrains the high-level plan. Additionally, the lower level in our approach differs from TAMP; while TAMP focuses on motion planning, our low-level components are symbolic representations of arbitrary platform components not restricted to manipulation. In a similar fashion, Erdem et al. [2016] integrate general feasibility checks into an ASP-based planner, either by checking constraints directly during search, or by constraining the planner afterwards if a feasibility check is violated. Alternatively, external predicates can be directly embedded into PDDL-based planners [Hertle et al., 2012; Dornhege et al., 2012], ASP-based planners [Erdem et al., 2012], and other reasoners such as CCALC [Aker et al., 2011]. There, a low-level component sets the value of a symbolic atom used by the task planner, which allows to integrate platform components, but does not allow for temporal constraints. RMPL [Kim et al., 2001] extends simple temporal networks into temporal plan networks to use a temporal planner to resolve temporal constraints. In contrast to the proposed approach, constraints in RMPL express relations between actions of the plan and do not provide an abstraction of the underlying platform. Konecn`y et al. [2014] use temporal constraints for execution monitoring, but do not use the constraints to augment the original plan. Hofmann and Lakemeyer [2018] formulate metric temporal constraints on GOLOG programs and describe a transformation procedure based on MTL synthesis [Hofmann and Lakemeyer, 2020], but do not provide an implementation.

Concerning planning via model checking [Cimatti et al., 1997; Giunchiglia and Traverso, 2000], Li et al. [2012] compare the performance of different model checking tools against planning tools, showing that some model checkers can compete with planners. Panek et al. [2006a] obtain an order schedule for a lacquer production plant from reachability analysis on TAs extended by weights and communication across different TAs with the tool TaOpt [Panek et al., 2006b]. Largou¨et et al. [2016] combine two TA extensions to perform planning in an extension of the transport domain from the International Planning Competition (IPC). They also apply reachability analysis to compute plans. Ziegert and Wehrheim [2013] decouple time-critical software component management from a top-level graph transformation framework to guarantee exclusive access to resources.

3 Plan Transformation: Assumptions

Our goal is to decouple the platform specifics from the abstract reasoning. To narrow down this broad objective, we postulate core assumptions that form the base of the procedure this paper presents. Constraints required by the operating platform should be modeled separately from the abstract reasoning domain. Those constraints are satisfied only after a high-level course of action is determined. This is done by means of a plan transformation that adds platform actions to the existing abstract plan. It specifically does not remove or re-order existing plan actions to avoid tampering with the feasibility of the initial plan. For the same reason, controlling platform specifics must not alter the high-level reasoning states, hence the platform domain and planning domain are disjoint. This enables us to treat the operation of platforms as a process that runs in parallel to the execution of domain actions. It also allows us to treat the plan actions as atomic propositions in MTL. In particular, we do not need to know about the preconditions and effects of the plan actions, because plan actions do not affect platform actions (and vice versa). Instead, the dependencies that the transformation ensures may be fully captured in terms of temporal relations between the domain actions and the platform states. The responsibility of the proposed transformation is therefore to determine an executable plan together with execution start times for each action, based on the temporal restrictions propagated by the reasoner, the control restrictions induced by the models, and the temporal constraints expressing relations between high-level and low-level actions. For simplicity, we assume that the robot platform is modeled with a single TA. If multiple TAs are modeled, they can be combined by a product construction [Alur and Dill, 1994].

4 Foundations

We briefly summarize suitable formalisms, namely MTL and timed automata, to model temporal dependencies.

4.1 Metric Temporal Logic (MTL)

MTL [Koymans, 1990] extends Linear Time Logic (LTL) with timing constraints on the Until modality. One commonly used semantics for MTL is a pointwise semantics [Henzinger, 1998], in which formulas are interpreted over timed words.

Definition 1 (Timed Words). A timed word ρ over a finite set of atomic propositions Σ is a finite or infinite sequence (σ0, τ0) (σ1, τ1) . . ., where σi ⊆ Σ and τi ∈ R≥0 such that the sequence (τi) is monotonically non-decreasing and nonZeno. The set of timed words over Σ is denoted as TΣ∗ .

Definition 2 (Formulas of MTL). Given a set Σ of atomic propositions, the formulas of MTL are built as follows:

We use the abbreviations XIφ := (⊥UI φ) (next), FIφ := (⊤UI φ) (future) and GIφ := ¬FI¬φ (globally). We may omit the interval I if I = [0,∞).

Definition 3 (Pointwise semantics of MTL). Given a timed word ρ = (σ0, τ0) (σ1, τ1) . . . over alphabet Σ and an MTL formula φ, ρ, i |= φ is defined as follows:

1. ρ, i |= p iff p ∈ σi 2. ρ, i |= ¬φ iff ρ, i ̸|= φ
2. ρ, i |= φ1 ∧ φ2 iff ρ, i |= φ1 and ρ, i |= φ2
3. ρ, i |= φ1UI φ2 iff there exists j such that (1) i < j < |ρ|, (2) ρ, j |= φ2, (3) τj - τi ∈ I, (4) and ρ, k |= φ1 for all k with i < k < j.

Following [Henzinger, 1998], we use the strict semantics for the Until modality, which can be translated into the nonstrict semantics [Ouaknine and Worrell, 2005].

4.2 Timed Automata

Timed automata [Alur and Dill, 1994] extend finite automata by a notion of continuous time. We adopt the definition of Bengtsson and Yi [2004].

Definition 4. A timed automaton (TA) is a tuple A = (L, l0, E, I) over a finite set of clocks C and a finite alphabet ΣE, where L is a finite set of locations (also called states); l0 ∈ L is a starting location; I : L → Φ(C) is the invariant of each location; and E ⊆ L×Φ(C)×ΣE ×2C ×L is the set of transitions. Φ(C) denotes the set of clock constraints δ (also called guards), defined by δ ::= x op c | c op x | δ∧δ, where x ∈ C is a clock, op ∈ {<, ≤, =, ≥, >} and c ∈ Q is a constant. Instead of (li, g, a, r, lj) ∈ E, we write li g,a,r ---→ lj ∈ E and call r the set of resets or updates.

TAs model behavior depending on continuous time with the help of clocks. The current value of clocks is expressed via Clock assignments ν : C → R≥0, initially all clocks start at value 0, then they advance continuously and at the same rate. At any given time, a TA A is in a configuration 〈li, νi〉, which is valid only if the clock values given through νi satisfy the constraint I(li). A configuration can be changed by either letting d time elapse while not changing li, or by taking a transition e = li g,a,r ---→ lj ∈ E. Transition e may only be taken if νi satisfies g and taking e changes all values of clocks in r to 0. This induces an infinite transition system T(A) where the set of states are all possible configurations and the transitions are formed by either delaying for d seconds or taking transitions e ∈ E. A path in T(A) is called a timed trace and defines a run on A through the labels on the used transitions. Each run induces a timed word (σ0, τ0) (σ1, τ1) . . . ∈ TΣ∗E , establishing a connection between MTL and TAs.

The reachability problem on a TA can be stated as follows: Given a starting configuration 〈l, ν〉 and a destination state l′ along with a target clock constraint ϕ, find a path from 〈l, ν〉 to a configuration 〈l′ , ν ′ 〉 where ν ′ satisfies ϕ. The problem is PSPACE-complete and thus decidable [Alur and Dill, 1994].

5 PlatformConstraints

As motivated above, we are given a plan P = 〈a1, . . . , an〉 and a TA AM with labeled states, as shown in Figure 1. The plan P describes some agent behavior, while the TA AM models the specific robot platform. The edge labels of the platform components describe low-level actions that the robot can take, e.g., shut-off. The set of plan actions ΣP , the low-level actions ΣE and the state labels ΣL are assumed to be pairwise disjoint. For a timed word σ we consider it to describe a transformed plan, if for each σi ∈ σ: |σi ∩ ΣP | ≤ 1, |σi ∩ΣE| ≤ |σi ∩ΣL| = 1 and δ0 ∩ΣP = ∅. Hence, in σ, the platform is always in exactly one state, at most one action is executed, and the first entry contains no action. We connect the plan P and the platform TA AM by three kinds of temporal constraints formulated in MTL over Σ = ΣP ∪ ΣE ∪ ΣL.

5.1 Requiring Certain PlatformActions

Let us start with constraints postulating how M has to be controlled during P . Let βi denote a disjunction over a subset of ΣP ⊆ Σ and αi a disjunction over a subset of ΣL ⊆ Σ.

where B := 〈〈β1, I1〉, . . . , 〈βn, In〉〉. A so-called until-chain constraint uc states that whenever an action a1 matching α1 is followed by a2 matching α2, without further occurrences of α1 or α2 in between, then between such a matching pair of domain actions a1 and a2 the platform has to sequentially remain in the states specified through the βi in B for a time span given through the intervals Ii.

Satisfying uc(B, α1, α2), given a plan P = 〈a1, . . . , an〉, equates to grounding a timed word ({a1}, τ1) . . . ({an}, τn) while also extending it by additional platform actions. Consider the TA from Figure 1, γe := uc(〈running, [0,∞)〉, s pick, e pick) and a plan 〈s pick, e pick〉 consisting of a durative pick action represented by a start and end action. Let ρ := ({s pick}, τ1)({e pick}, τ2) for some τ1, τ2 ∈ Q+. It holds that ρ |= (s pick ∧ X(e pick ∨ (¬s pickUe pick))). Hence, the constraint γe requires (running ∧ ¬e pick)Ue pick. Assuming Acam is in state off prior to P , we could adapt ρ to satisfy γe:

5.2 Temporal Constraints on Plan Actions

Furthermore, we may also impose temporal constraints on the actions in the abstract plan, e.g., the duration between two plan actions. For this, we define two macros IsDomAct and PlanOrder(i), where IsDomAct := ∨a∈P a holds iff the current action is a plan action, and PlanOrder(i) holds iff the current action is the i-th action in the plan. Given the total number of plan actions n, it can be defined as follows:

Formulas to constrain the time interval I in which the i-th plan action starts can be simply given as follows:

We may also require a certain amount of time passing between plan actions by specifying the time interval I in between the i-th and j-th plan action, with j > i:

Continuing with the example from above, we can adapt ρ′ to satisfy a constraint rel(1, 2, [15, 20]) (requiring a time interval [15, 20] between action 1 and action 2) by adapting the grounded times in ρ′ :

Listing 1: Transformation Procedure

1 AP:=encode_plan(P,Cabs ∪Crel) 2 Abase:=add_platform_ta(AP ,AM) 3 Aenc:=encode_platform_control(Abase,Cuc): 4 For γ ∈ Cuc: 5 For (aj, aj′ ) in get_activations(γ, P) 6 Abase:=enforce_uc(Abase, aj , aj′ , γ) 7 return Abase 8 enforce_uc(Acurr, aj, aj′ , uc(〈β1, I1〉 . . . 〈βn, In, α1, α2)): 9 Acontext:=get_sub_ta(Acurr, aj, aj′) 10 For i in {1, . . . , n}: 11 Si:=copy(Acontext) 12 Si:=restrict(Acurr,αi,Ii) 13 Atemp:=combine(S1, . . . , Sn, I1, . . . , In-1) 14 return replace(Acontext,Atemp, S1, Sn, In)

6 Transformation

Our proposed plan transformation can be summarized as follows: (1) Construct a single TA encoding the satisfaction of constraints during the plan as a reachability problem to a designated goal state (2) Find a symbolic representation of traces reaching that state using a model checker (3) Decode an actual trace from a symbolic one with grounded execution times. An overview of the procedure is shown in Figure 2. Here we focus on the encoding step, which is the core of our approach. The goal of the encoding step is to construct one TA Aenc with a state fin, such that every run reaching fin corresponds to a timed word satisfying the given constraints (of the form uc, abs and rel) whithin the plan P = 〈a1, . . . , ak〉. Listing 1 gives an overview over the necessary steps encode plan, add platform ta and encode platform control to construct Aenc.

Consider P e = 〈s goto, e goto, s pick, e pick〉, a plan consisting of start and end actions for the durative actions goto and pick, together with constraints:

The constraints γ1, γ2 and γ3 provide the duration of goto and pick and enforce that pick follows without any pause after goto finishes; γ4 states that during a goto action the camera should be turned off until the last 4 seconds of its execution, where it may become necessary to boot the camera for a subsequent pick action, which per γ5 requires a running camera for the whole duration. We denote the sets of constraints of the respective types by Cuc, Cabs and Crel.

6.1 Plan Constraint Encoding

The procedure encode plan constructs a TA AP with designated states a0 := start and an+1 := fin such that traces from start to fin induce execution time groundings of P respecting Cabs ∪ Crel. The construction is depicted in Figure 3 for our running example. Initially, the plan actions are translated into states as follows:

A fresh clock xabs is introduced to encode Cabs as follows: Let lb(x, I) := x ≥ a, if I = [a, b) or I = [a, b] and lb(x, I) := x > a otherwise. Let ub(x, I) be defined analogously for upper bounds. For each abs(k, Ik) ∈ Cabs, we add ub(xabs, Ik) as invariant to lk-1. Similarly, the lower bound of Ik is added as guard lb(xabs, Ik) on the transition reaching lk. Trivial bounds xabs ≥ 0 and xabs < ∞ are omitted.

Lastly, for each rel(k, k′ , I) ∈ Crel a new clock xk,k′ is added that is reset on the incoming transition of lak . Then, a clock constraint encoding the lower bound of I is added to the guard on the incoming transition of lak′ and the upper bound is added as invariant on all states li, k ≤ i < k′ . This step may be optimized by re-using a clock for different constraints when possible, e.g., a single clock xrel can encode all constraints of the form rel(k, k + 1, I).

The induced directed graph of the resulting TA AP is a simple line and time elapsing in state lak corresponds to the time elapsing since starting ak (and before starting ak+1). The constructed TA indeed encodes the possible action groundings to the plan that satisfy Cabs ∪ Crel:

Theorem 1. ρ = (∅, 0)({a1}, τ1)({a2}, τ2), . . . , ({an}, τn) is a timed word satisfying Cabs ∪ Crel iff there exists a valid timed trace ξ on AP from start to fin that induces ρ.

6.2 PlatformEncoding

We proceed by incorporating the platform TA into the construction. Listing 1 Line 2 creates a TA Abase based on AP such that runs to fin in Abase also include arbitrary control according to AM. Abase consists of k + 1 fresh copies Aak of AM (with a0 := start). For each state l ∈ LP \fin, we add its invariant I(l) to each state in the corresponding copy Al. For each transition e = l g,a,r ---→ l′ ∈ EP , we add transitions from each state s in Al to the corresponding copy s′ in Al′ (or to fin, if l′ = fin): s g,a,r ---→ s′ . Figure 4 shows such a constructed TA Abase schematically for our P e and Acam, leaving out all annotations on states and transitions.

Theorem 2. Every valid timed trace ξ on Abase from its initial state to fin induces a timed word ρ that satisfies Cabs ∪ Crel and the sequence of platform actions within ρ induce a valid run in AM.

6.3 PlatformConstraint Encoding

Finally, we encode the until-chain constraints Cuc (Listing 1 Line 3). By iteratively considering for each γ ∈ Cuc all corresponding scopes aj, aj ′ within the plan, the procedure encodes the platform controlling constraints. Hence the routine enforce uc restricts the traces reaching fin between the start of aj an aj ′ to remain in states of AM as specified in γ. Consider γ4 = uc(B4, s goto, e goto) with B4 := 〈〈off, [0,∞]〉, 〈⊤, [0, 4]〉〉. It states that whenever s goto is followed by e goto without occurrences of s goto or e goto in between, then starting at this s goto action, the platform has to be off for some time, followed by arbitrary actions for at most four seconds until the matching e goto starts. In other words, while driving, the camera has to be off unless the destination is reached within the next four seconds.

We need to modify each copy Aai in Abase that covers the relevant time frame to satisfy the constraint γ4. Each Aai models platform actions in the time frame between two subsequent plan actions. In Line 9, we construct a sub-automaton Acontext that contains all states that might be visited between aj and a′j , which is shown in Figure 4. An until-chain γi defines n sets of states specified by βi that have to be subsequently visited, which we can enforce by creating n copies Si of Acontext (Line 11). Each Si is subsequently restricted further (Line 12) to reflect the specification of βi: First, all states not matching βi are deleted. Then all those states within Si are removed that can never be visited while satisfying βi due to time conflicts imposed by the other constraints.

Since γ4 describes platform control only between the first and second plan action in P e , we end up with two copies S1, S2 of the initial copy As goto. After restricting the possible states, we consider the temporal constraints of γ, which are given by the intervals Ii. With a fresh clock xγ and by adding state invariants ub(xγ, Ii) to each state of Si, the upper bound of Ii can be enforced if xγ is set to 0 when entering Si. This is done in the next subroutine combine (Line 13), where a single TA is formed out of S1, . . . , Sn by connecting states s ∈ LSi with s′ ∈ LSi+1 as follows: Either s and s′ are copies of the same state in Acontext, then a transi-

tion s gi,copy,{xγ} --------→ s′ is added, where gi = lb(xγ, Ii+1) (copy transitions), or there exists a transition sc g,a,r ---→ s′c in AM and s is a copy of sc, s′ is a copy of s′c , then s g∧gi,a,r∪{xγ} ---------→ s′ is added (successor transitions).

Lastly, the resulting TAAtemp replaces the sub-automaton Acontext within Acurr (Line 14). This can be achieved by iterating over all transitions s g,a,r ---→ s′ of Acurr with either s in Acontext and s′ not in Acontext (incoming transitions) or vice versa (outgoing transitions). Any incoming transition with s′ matching β1 gets the respective copy within S1 as new destination and xγ is added to r. Any outgoing transition with s matching βn gets the respective copy within Sn as new source and lb(xγ, In) is added to g. All other incoming and outgoing transitions are deleted.

Applying this construction to our example yields a TA as shown in Figure 5. When all activations of each γ ∈ Cuc are encoded, our encoding stops with a TA Aenc. The correctness of our encoding is covered by Theorem 3.

Theorem 3. There exists a timed word ρ based on P augmented by control of AM that satisfies Cabs ∪ Crel ∪ Cuc iff there exists a run on Aenc from start to fin.

7 Evaluation

Using our implementation taptenc 1 (timed automatabased plan transformation encoding procedure), together with the CLI verifyta of the UPPAAL model checking suite [Bengtsson et al., 1996], we conducted two experiments on an Intel i7-8565U 1.8 GHz processor with 16 GB memory. UPPAAL does not return concrete timed traces when answering reachability queries, but yields a symbolic trace which represents possibly infinitely many concrete traces. Considering difference bound matrices as symbolic representation formalism (such as used by UPPAAL), Bøgsted Poulsen and van Vliet [2010] describe how to retrieve the fastest concrete trace out of a given symbolic one. We adopt that approach in our tool to cover the full transformation procedure.

First, we consider a scenario from the RoboCup Logistics League (RCLL) [Niemueller et al., 2013]. In the RCLL, robots have to move workpieces between machines and instruct those machines to assemble a product. We apply the transformation to possible production sequences of varying length in a simplified RCLL setting. The domain consists of the actions goto(m,m'), pick(o,m), get-from-shelf(o,m), put(o,m), and pay(o,m). The robot platform is modeled via three different timed automata. Aperc offers control over the perception to activate a camera when necessary, trigger object detection to validate grasping attempts as well as providing images to human supervisors during those attempts. Acalib manages the occasional need to calibrate an axis-driven gripper. Depending on the situation, a calibration may be undesirable, e.g., to avoid axis movement when holding something. Lastly, Acomm(m) allows to send instructions to a machine m to modify a product.

1 https://github.com/TarikViehmann/taptenc

As a first experiment, we consider plans of length 50 with a varying number of platform TAs (including multiple instances of Acom for different machines), as shown in Table 1. We can see that our approach is suitable to be used in typical robotics applications, given a limited number of platform components. The size of the encoded TAs is a major factor considering both the time spent by verifyta to load the TA and by taptenc to produce the encoding. Interestingly, the model checking task is not the limiting factor in the conducted tests, which we assume is due to the guidance that the explicit encoding gives to the underlying task. As a second experiment, we examined how the transformation scales as the plan length increases, as shown in Table 2. The results show that the presented approach is able to transform plans with 150 domain actions in reasonable time.

Lastly, we evaluated our approach in a domestic service robot scenario based on [Hofmann et al., 2016]. The robot is tasked to clean up a table full of cups. Clean cups have to be placed on a shelf, dirty ones belong in a dishwasher. In the domain, the robot must (a) align to the furniture properly before picking up a cup, (b) scan surfaces before picking up or putting down a cup, (c) back off an object before moving away from it. We modified the domain to be suitable for temporal planning and considered scenarios with a varying number of cups on the table. We built a simplified domain without the special requirements (a)-(c) and decoupled them in a separate platform TA. Our plan transformation procedure then inserts platform actions to compute a feasible solution. We used TFD [Eyerich et al., 2009] for planning both on the full and the simplified domain and configured it to stop when the first plan was found. The plans obtained from the simple domain were then used as input for taptenc. The results are summarized in Figure 6. From those we conclude that decoupling of platform constraints helped to reduce the overall runtime on complex problem instances significantly, while causing minor computational overhead on small tasks.

8 Conclusion

We developed a procedure to transform an abstract plan into an executable action sequence that considers all platform specifics that were ignored in the abstract domain. Such an abstract plan may be determined by a planner or by any other reasoning system that produces action sequences. Having platform components decoupled from the high-level domain allows to adapt low-level specifics without changing the highlevel reasoner, as different concerns are clearly separated. It also simplifies the high-level domain, which may improve the reasoner's performance. We represent platform components as timed automata (TAs) and express the connection between such automata models and the abstract domain with constraints from a subset of Metric Temporal Logic (MTL). The proposed transformation first combines the abstract plan and the platform components into a single TA and then applies reachability analysis to determine an execution trace. We evaluated the approach on real-world scenarios from the RoboCup Logistics League and from a domestic service robot setting. Both scenarios showed that our approach is able to transform an abstract plan in reasonable time, even when dealing with large problems. The proposed approach also outperforms an alternative approach, where the platform details are directly encoded into the planning problem.

Acknowledgements

This work is funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under grants GL-747/23-1, GRK 2236/1, and under Germany's Excellence Strategy - EXC-2023 Internet of Production - 390621612.

This work is partially supported by the EU ICT-48 2020 project TAILOR (No. 952215).

We thank Stefan Schupp for an insightful initial discussion on timed automata modelling.