pith. sign in

arxiv: 2501.08918 · v2 · submitted 2025-01-15 · 📡 eess.SY · cs.SY

Efficient Planning in Large-scale Systems Using Hierarchical Finite State Machines

Pith reviewed 2026-05-23 05:25 UTC · model grok-4.3

classification 📡 eess.SY cs.SY
keywords hierarchical finite state machinesoptimal planningexit costssubtree pruninglarge-scale systemsreconfigurable planning
0
0 comments X

The pith

A two-step algorithm finds optimal plans between any states in a hierarchical finite state machine by pre-computing exit costs and pruning subtrees.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents an algorithm that separates optimal planning in a large hierarchical finite state machine into a pre-processing phase and a query phase. The pre-processing phase computes optimal exit costs for each machine, with effort that grows only with the number of machines rather than the total number of states. The query phase then uses these costs to remove irrelevant subtrees from consideration while still guaranteeing an optimal plan. The method is designed to handle updates to the hierarchy by recomputing only the affected exit costs and to avoid redundant work when identical machines appear in the structure. Validation on systems with millions of states and a robotic example shows faster performance than standard shortest-path methods.

Core claim

Optimal planning between any two states in an HFSM is achieved by first computing optimal exit costs of the machines in a pre-processing step whose time complexity scales with the number of machines, then using those costs in a query step to prune irrelevant subtrees while preserving optimality; the procedure recomputes only affected costs after changes and computes costs once per group of identical machines.

What carries the argument

The two-step procedure that pre-computes optimal exit costs for each machine and uses them to prune subtrees during the query.

If this is right

  • Changes to the HFSM require only local recomputation of the affected exit costs.
  • Groups of identical machines need only one set of exit-cost computations.
  • The approach applies directly to systems containing millions of states.
  • The same pre-computed costs can be reused for many different start-goal pairs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The pruning rule could be tested on other hierarchical state representations used in model-based reinforcement learning.
  • Reconfigurability suggests the method could support online adaptation when the underlying system model is learned incrementally.
  • The separation of pre-processing and query phases may allow parallel hardware acceleration of the exit-cost calculations.

Load-bearing premise

The hierarchy allows each machine's optimal exit costs to be computed independently so that the query step can prune subtrees without discarding any optimal plan.

What would settle it

An instance of an HFSM where the plan returned after pruning using the pre-computed exit costs has higher total cost than the true shortest path.

Figures

Figures reproduced from arXiv: 2501.08918 by Elis Stefansson, Karl H. Johansson.

Figure 2
Figure 2. Figure 2: Change in House 2 in the HiMM given by [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 1
Figure 1. Figure 1: Robot application modelled as an HFSM with three layers. Second, we propose a planning algorithm for computing an optimal plan between any two states in an HiMM. The algorithm consists of two steps. The first step is a preprocess￾ing step, the Optimal Exit Computer, that computes optimal exits costs of each MM in the HiMM, with time complexity O(|X|) where |X| is the number of MMs in the HiMM. This step ne… view at source ↗
Figure 3
Figure 3. Figure 3: Example of an HiMM depicted in a tree-form. that is, the machine does not stop due to unsupported input). Next, we define an HiMM. Definition 3 (Hierarchical Mealy Machine): An HiMM Z = (X, T) consists of a set of MMs X with common input set Σ, and a tree T with nodes being MMs from X (specifying how the machines in X are nested). More precisely, a node M ∈ X of T has |QM| outgoing arcs on the form M q −→ … view at source ↗
Figure 5
Figure 5. Figure 5: The HiMM with identical machines for the robot application from Section I-B. The MM Houses consists of several identical houses, depicted by lines from the MM Houses to the MM House (where the number of lines specify the number of identical houses). The MM House consists in turn of one start state and several identical MMs given by Location, where Location is an MM with states having no further refinement.… view at source ↗
Figure 4
Figure 4. Figure 4: The four modifications of an HiMM depicted. The dashed rectangle specifies the MM M subject to change. respect to M is the HiMM Z ′ with tree T ′ having root M and arcs M qi −→ Ri for i ≤ n and M qi −→ ∅ for i > n, where Ri is the root MM of the tree of Zi . 5 These four modifications form the atomic changes of an HiMM, where a sequence of modifications can change any HiMM Z = (X, T) to any other HiMM Z ′ … view at source ↗
Figure 6
Figure 6. Figure 6: HiMM Z = (X, T ) with optimal exit costs given as tuples (cMa , cMb , cMc ) over each MM M. III. EFFICIENT HIERARCHICAL PLANNING In this section, we present a planning algorithm computing optimal plans for a given HiMM Z = (X, T), 6 summarised by Algorithm 1 (ignore pseudo-code in red for now). The algorithm consists of two steps. In the first step, an Optimal Exit Computer computes optimal exit costs for … view at source ↗
Figure 7
Figure 7. Figure 7: Overview of the procedure of the Optimal Planner. (a) The original HiMM Z. (b) The reduced HiMM Z¯ computed by truncating subtrees of Z not containing sinit or sgoal. (c) Computed optimal trajectory z (marked orange) to the reduced HiMM Z¯. (d) Optimal plan u (with its optimal trajectory marked orange) to the original HiMM Z computed by expanding z. M ∈ M¯ and a ∈ Σ, χ¯(q, a) =    γM(q, a) δM(q, a… view at source ↗
Figure 8
Figure 8. Figure 8: Illustration of a reduced trajectory and optimal expansion. Here, q has replaced the depicted subtree in Z¯. For the trajectory z = ((1, b), (2, b), (3, a)) of Z, the reduced trajectory is therefore zR = ((1, b), (q, a)). Conversely, the optimal expansion of z = ((1, b), (q, a)) is zE = ((1, b), (2, b), (3, a)). For simplicity, we plot just the relevant transitions and assume unit costs. we are down in the… view at source ↗
Figure 9
Figure 9. Figure 9: , with resulting algorithm summarised by Algorithm 1, where parts handling modifications are coloured red. More precisely, a change is given as a sequence of modifications mseq, where each modification m in mseq modifies Z (line 3), and the planning algorithm correspondingly marks each MM that needs to recompute its optimal exit costs due to m (line 4). Here, the marked MMs, due to m, are the MM affected b… view at source ↗
Figure 11
Figure 11. Figure 11: The MM M (left) and resulting HiMM Z (right) from Study 1 using one recursion. given in Section I-B and validate the reconfigurability of the algorithm. In both studies, we also consider how the examples can be modelled more compactly and solved faster using HiMMs with identical machines. We compare our algorithm with Dijkstra’s algorithm [11], [12], Bidirectional Dijkstra [4] and Contraction Hierarchies … view at source ↗
Figure 12
Figure 12. Figure 12: Computing time for varying depth in Study 1. system with depth 20.13 This speed-up comes also at the cost of a more expensive preprocessing step. In particular, for the HiMM Z with depth 20, the preprocessing step of Contraction Hierarchies is 20 times slower than the Optimal Exit Computer (1200 s compared to 42 s). Finally, we show how we can rapidly speed-up the com￾putation time of the Optimal Exit Com… view at source ↗
read the original abstract

We consider optimal planning in a large-scale system formalised as a hierarchical finite state machine (HFSM). A planning algorithm is proposed computing an optimal plan between any two states in the HFSM, consisting of two steps: A pre-processing step that computes optimal exit costs of the machines in the HFSM, with time complexity scaling with the number of machines; and a query step that efficiently computes an optimal plan by removing irrelevant subtrees of the HFSM using the optimal exit costs. The algorithm is reconfigurable in the sense that changes in the HFSM are handled with ease, where the pre-processing step recomputes only the optimal exit costs affected by the change. The algorithm can also exploit compact representations that groups together identical machines in the HFSM, where the algorithm only needs to compute the optimal exit costs for one of the identical machines within each group, thereby avoid unnecessary recomputations. We validate the algorithm on large systems with millions of states and a robotic application. It is shown that our approach outperforms Dijkstra's algorithm, Bidirectional Dijkstra and Contraction Hierarchies.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes an algorithm for computing optimal plans between any pair of states in a hierarchical finite state machine (HFSM). It consists of a pre-processing phase that computes optimal (target-independent) exit costs for each machine, with complexity linear in the number of machines, followed by a query phase that uses these costs to prune irrelevant subtrees of the HFSM while claiming to preserve optimality. The method is presented as reconfigurable under local HFSM changes and able to exploit identical-machine groupings; empirical results on million-state instances and a robotic application show it outperforming Dijkstra, bidirectional Dijkstra, and contraction hierarchies.

Significance. If the optimality claim is rigorously established, the approach would offer a practical, reconfigurable method for optimal planning in very large hierarchical systems, directly addressing scalability limits of standard shortest-path algorithms. The reconfigurability and grouping optimizations are notable strengths for dynamic or repetitive system models.

major comments (2)
  1. [Query step (abstract and §4)] The central optimality claim rests on the query-step pruning rule using pre-computed, target-independent minimum exit costs. Because a machine may have multiple exits with distinct costs, a single min-exit value supplies only a lower bound; the manuscript must demonstrate (via proof or admissible-heuristic argument) that the pruning predicate never discards an optimal path for an arbitrary target exit. No such demonstration appears in the supplied description of the query step.
  2. [Pre-processing step (abstract and §3)] The pre-processing computes exit costs once per machine (or per group of identical machines). For the subsequent pruning to be both sound and complete across all query pairs, the exit-cost values must be shown to be admissible with respect to every possible target state inside or outside the machine. The current presentation leaves this admissibility argument implicit.
minor comments (2)
  1. [§3] Clarify the precise definition of 'optimal exit cost' (is it the minimum cost to any exit, or the cost to a designated exit?) and how it is stored for use in the query phase.
  2. [Experiments] The experimental section should report the exact HFSM sizes, number of machines, and whether the reported speed-ups include the pre-processing time or only query time.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript. The two major comments correctly identify that the optimality argument for the pruning rule and the admissibility of the pre-computed exit costs are presented implicitly rather than with an explicit demonstration. We address each point below and will incorporate the requested clarifications.

read point-by-point responses
  1. Referee: [Query step (abstract and §4)] The central optimality claim rests on the query-step pruning rule using pre-computed, target-independent minimum exit costs. Because a machine may have multiple exits with distinct costs, a single min-exit value supplies only a lower bound; the manuscript must demonstrate (via proof or admissible-heuristic argument) that the pruning predicate never discards an optimal path for an arbitrary target exit. No such demonstration appears in the supplied description of the query step.

    Authors: We agree that an explicit argument is required. The minimum exit cost serves as an admissible lower bound on the cost to reach any exit from a state inside the machine. In the query phase, a subtree is pruned only when this lower bound plus the cost to reach the subtree root already exceeds the cost of the best complete plan found so far. Because any path that would exit through a more expensive exit cannot improve upon a plan that exits through the cheapest exit (when the target lies outside), the pruning rule preserves optimality. We will add a short lemma and proof of this claim to §4 in the revision. revision: yes

  2. Referee: [Pre-processing step (abstract and §3)] The pre-processing computes exit costs once per machine (or per group of identical machines). For the subsequent pruning to be both sound and complete across all query pairs, the exit-cost values must be shown to be admissible with respect to every possible target state inside or outside the machine. The current presentation leaves this admissibility argument implicit.

    Authors: We concur that the admissibility property should be stated explicitly. The pre-processing step solves a shortest-path problem from every state to the set of all exits of its machine; the resulting value is therefore the minimum cost to leave the machine and is admissible for any target (inside or outside) because the true cost to the target is at least the cost to the nearest exit. When identical machines are grouped, the same values remain admissible. We will insert a brief paragraph making this argument explicit in §3 of the revised manuscript. revision: yes

Circularity Check

0 steps flagged

No circularity: algorithm is direct computation without reduction to inputs

full rationale

The provided text (abstract and description) presents a two-step planning algorithm: pre-processing computes optimal exit costs per machine (scaling with number of machines), followed by a query step that prunes subtrees using those costs. No equations, self-definitions, fitted parameters renamed as predictions, or load-bearing self-citations appear. The approach is described as reconfigurable and benchmarked externally against Dijkstra variants, with no derivation chain that reduces by construction to its own inputs. This matches the default expectation of a non-circular algorithmic paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on the domain assumption that HFSMs admit independent exit-cost computation and that standard shortest-path optimality carries over after pruning; no free parameters or new entities are introduced.

axioms (1)
  • domain assumption The hierarchical finite state machine admits a well-defined notion of optimal exit cost for each machine that can be computed independently of specific start and goal states.
    Invoked directly in the description of the pre-processing step.

pith-pipeline@v0.9.0 · 5715 in / 1270 out tokens · 76106 ms · 2026-05-23T05:25:31.233617+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages

  1. [1]

    R. Alur, M. Benedikt, K. Etessami, P. Godefroid, T. Reps, and M. Yan- nakakis. Analysis of recursive state machines. ACM Transactions on Programming Languages and Systems , 27(4):786–818, 2005

  2. [2]

    R. Alur, R. Grosu, and M. McDougall. Efficient reachability analysis of hierarchical reactive machines. In International Conference on Computer Aided Verification, pages 280–295. Springer, 2000

  3. [3]

    Alur and M

    R. Alur and M. Yannakakis. Model checking of hierarchical state machines. ACM SIGSOFT Software Engineering Notes , 23(6):175–188, 1998

  4. [4]

    H. Bast, D. Delling, A. Goldberg, M. M ¨uller-Hannemann, T. Pajor, P. Sanders, D. Wagner, and R. F. Werneck. Route planning in trans- portation networks. In Algorithm Engineering: Selected Results and Surveys, pages 19–80. Springer, 2016. 14 IEEE TRANSACTIONS ON AUTOMATIC CONTROL

  5. [5]

    Biggar, M

    O. Biggar, M. Zamani, and I. Shames. Modular decomposition of hierarchical finite state machines. arXiv preprint arXiv:2111.04902 , 2021

  6. [6]

    G. Booch. The Unified Modeling Language User Guide . Pearson Education India, 2005

  7. [7]

    C. G. Cassandras and S. Lafortune. Introduction to Discrete Event Systems. Springer, 2008

  8. [8]

    A. E. C. da Cunha, J. E. R. Cury, and B. H. Krogh. An assume-guarantee reasoning for hierarchical coordination of discrete event systems. In International Workshop on Discrete Event Systems , pages 75–80. IEEE, 2002

  9. [9]

    R. P. C. de Souza, M. V . Moreira, and J. Lesage. A hierarchical approach for discrete-event model identification incorporating expert knowledge. 15th IFAC Workshop on Discrete Event Systems , 53(4):275–281, 2020

  10. [10]

    Dibbelt, B

    J. Dibbelt, B. Strasser, and D. Wagner. Customizable contraction hierarchies. ACM Journal of Experimental Algorithmics, 21:1–49, 2016

  11. [11]

    E. W. Dijkstra. A note on two problems in connexion with graphs. Numerische Mathematik, 1(1):269–271, 1959

  12. [12]

    M. L. Fredman and R. E. Tarjan. Fibonacci heaps and their uses in improved network optimization algorithms. In 25th Annual Symposium on Foundations of Computer Science , pages 338–346, 1984

  13. [13]

    Geisberger, P

    R. Geisberger, P. Sanders, D. Schultes, and C. Vetter. Exact routing in large road networks using contraction hierarchies. Transportation Science, 46(3):388–404, 2012

  14. [14]

    D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming , 8(3):231–274, 1987

  15. [15]

    Hubbard and P

    P. Hubbard and P. E. Caines. Dynamical consistency in hierarchical supervisory control. IEEE Transactions on Automatic Control, 47(1):37– 52, 2002

  16. [16]

    Laster and O

    K. Laster and O. Grumberg. Modular model checking of software. In Tools and Algorithms for the Construction and Analysis of Systems: 4th International Conference, pages 20–35. Springer, 1998

  17. [17]

    Ma and W

    C. Ma and W. M. Wonham. Nonblocking supervisory control of state tree structures. IEEE Transactions on Automatic Control , 51(5):782– 793, 2006

  18. [18]

    J. Maue, P. Sanders, and D. Matijevic. Goal-directed shortest-path queries using precomputed cluster distances. ACM Journal of Exper- imental Algorithmics, 14, 2010

  19. [19]

    Millington and J

    I. Millington and J. Funge. Artificial Intelligence for Games. CRC Press, 2018

  20. [20]

    R. H. M ¨ohring, et al. Partitioning graphs to speedup dijkstra’s algorithm. ACM Journal of Experimental Algorithmics , 11:2–8, 2007

  21. [21]

    S. Perk, T. Moor, and K. Schmidt. Hierarchical discrete event systems with inputs and outputs. In 8th International Workshop on Discrete Event Systems, pages 427–432. IEEE, 2006

  22. [22]

    Schillinger, S

    P. Schillinger, S. Kohlbrecher, and O. V on Stryk. Human-robot collab- orative high-level control with application to rescue robotics. In IEEE International Conference on Robotics and Automation , pages 2796– 2802, 2016

  23. [23]

    Stefansson and K

    E. Stefansson and K. H. Johansson. Efficient and reconfigurable optimal planning in large-scale systems using hierarchical finite state machines. In IEEE Conference on Decision and Control , pages 7380–7387, 2023

  24. [24]

    Stefansson and K

    E. Stefansson and K. H. Johansson. Hierarchical finite state machines for efficient optimal planning in large-scale systems. In European Control Conference, pages 1–8. IEEE, 2023

  25. [25]

    O. N. Timo, A. Petrenko, A. Dury, and S. Ramesh. Reachability in hierarchical machines. In Proceedings of the IEEE 15th International Conference on Information Reuse and Integration, pages 475–482, 2014

  26. [26]

    X. Wang, Z. Li, and W. M. Wonham. Real-time scheduling based on nonblocking supervisory control of state-tree structures. IEEE Transactions on Automatic Control , 66(9):4230–4237, 2020

  27. [27]

    K. C. Wong and W. M. Wonham. Hierarchical control of discrete-event systems. Discrete Event Dynamic Systems , 6:241–273, 1996

  28. [28]

    Zhong and W

    H. Zhong and W. M. Wonham. On the consistency of hierarchical supervision in discrete-event systems. IEEE Transactions on Automatic Control, 35(10):1125–1134, 1990. Elis Stefansson received a B.Sc. degree in Engineering Physics from KTH Royal Institute of Technology, Sweden in 2015 and a M.Sc. degree in Mathematics jointly from KTH Royal Institute of Tech...

  29. [29]

    The other cases are totally analogous to the FSM proof and we refer to

    with minor modifications to account for costs. The other cases are totally analogous to the FSM proof and we refer to

  30. [30]

    To show (iii) assumeu ∈ S, v /∈ S

    for details. To show (iii) assumeu ∈ S, v /∈ S. Consider an arc u a,o − − →v in M. Then u has no a-arc in M[S] as v ∈ S. Since S a,o − − →v is an arc in Z/S, we have that all states of Z[M] in M/S ·S M[S] without a-arcs now have a-arcs to v with cost o (due to the definition of an expansion), so u a,o − − →v is in M/S ·S M[S]. Conversely, consider an arc ...

  31. [31]

    This algorithm is given by Algorithm 5, where the subroutine Compute paths, given by Algorithm 6, computes the se- quences U1,

    Reduce: Algorithm: We start by providing the algorithm for computing the reduced HiMM ¯Z, mentioned in Remark 2. This algorithm is given by Algorithm 5, where the subroutine Compute paths, given by Algorithm 6, computes the se- quences U1, . . . , Un and D1, . . . , Dm (called Upath and Dpath respectively) and α and β. Here, α is analogous to β but for ¯U...

  32. [32]

    To this end, consider an HiMM Z and its reduced HiMM ¯Z with respect to some initial state sinit and goal state sgoal

    Reduced Trajectory and Optimal Expansion: We continue with the complete definitions of a reduced trajectory zR and an optimal expansion zE outlined in Section III-B.1. To this end, consider an HiMM Z and its reduced HiMM ¯Z with respect to some initial state sinit and goal state sgoal. The reduced trajectory zR of a trajectory z of Z is then given by Algo...

  33. [33]

    Planning Equivalence: In this section, we prove the planning equivalence given by Theorem 1. For a more compact terminology, we say that a trajectory z = ( qi, ai)N i=1 is a feasible trajectory to (Z, sinit, sgoal) if it is a trajectory of Z such that q1 = sinit and ψ(qN , aN) = sgoal. A feasible trajectory to ( ¯Z, sinit, sgoal) is analogously defined. W...

  34. [34]

    Note that sgoal is one of the nested states within the subtree with root ¯Dβ

    Proof of Lemma 1: We now provide the proof of Lemma 1 in Section III-B: Proof: [Proof of Lemma 1] Let z = ( qi, ai)N i=1 be an optimal trajectory to ( ¯Z, sinit, sgoal). Note that sgoal is one of the nested states within the subtree with root ¯Dβ. Thus, the only way to reach sgoal from a state outside this subtree is via a transition going through ¯Dβ end...

  35. [35]

    To this end, we present a more formal and detailed version of Algorithm 3, given by Algorithm 9, calling subroutines given by Algorithm 10 to 13

    Solve: Algorithm and Correctness: We continue by prov- ing Proposition 5, assuring the correctness of Algorithm 3. To this end, we present a more formal and detailed version of Algorithm 3, given by Algorithm 9, calling subroutines given by Algorithm 10 to 13. Before proving Proposition 5, it is beneficial to give an overview of this detailed version, com...

  36. [36]

    Note that also ˜wk 1 corresponds to an arc in G labelled by ˜wk 1 and its corresponding cost ¯C( ˜wk 1)

    ≤ ¯C(wk 1). Note that also ˜wk 1 corresponds to an arc in G labelled by ˜wk 1 and its corresponding cost ¯C( ˜wk 1). Therefore, the trajectory ˜w1 = ˜w1 1 . . . ˜wK 1 corresponds to a directed path of G from sinit to ¯Dβ with cost ¯C( ˜w1) = KX k=1 ¯C( ˜wk

  37. [37]

    Since z1 is by construction an optimal directed path in G from sinit to ¯Dβ, we have ¯C(z1) ≤ ¯C( ˜w1), and thus ¯C(z1) ≤ ¯C(w1)

    = ¯C(w1). Since z1 is by construction an optimal directed path in G from sinit to ¯Dβ, we have ¯C(z1) ≤ ¯C( ˜w1), and thus ¯C(z1) ≤ ¯C(w1). This completes the first part of the proof. Part 2: ¯C(z2) ≤ ¯C(w2). Let c, g and ¯Di be as in lines 14– 16 in Algorithm 9. Note that w2 starts at c and can only reach sgoal by going to g. Hence, w2 must have a sub-tr...

  38. [38]

    The procedure is almost identical to the optimal expansion, given by Algorithm 8

    Expand: Algorithm: We now provide the full algorithm of Expand (line 10 of Algorithm 1), given by Algorithm 14. The procedure is almost identical to the optimal expansion, given by Algorithm 8. Indeed, there are only two differences. The first difference is that line 8 in Algorithm 8 is changed to return only the input a. In this way, Algorithm 14 outputs...

  39. [39]

    Time Complexity: Finally, we prove the time complexity of the Online Planner given by Proposition 6. The proof is rather straightforward: We first compute the time complexities of all called algorithms of the Online Planner, then we combine these time complexities to infer the time complexity of the Online Planner. We start by proving the following lemma....

  40. [40]

    We have V = |Q| ≤ bs and E ≤ | Q||Σ| ≤ bs|Σ|

    Line 18 has time complexity O(E + V log(V )) where E and V are the number of arcs and nodes of ¯Di (seen as a graph). We have V = |Q| ≤ bs and E ≤ | Q||Σ| ≤ bs|Σ|. Thus, line 18 has time complexity O(bs|Σ| + bs log(bs)). Since the while-loop can be called at most depth(Z) times, the total contribution line 18 has to the time complexity is O depth(Z) · bs|...

  41. [41]

    Here, M is the MM targeted by m, specified in Definition 5 to 8 for each type of modification

    Marking Procedure: The details of the marking procedure for a modification m is given by Algorithm 15. Here, M is the MM targeted by m, specified in Definition 5 to 8 for each type of modification. To understand the marking, note that when modifying M, the optimal exit costs of M may change and thus needs to be recomputed (line 2). Moreover, if M is neste...

  42. [42]

    Proof: [Proof of Proposition 7] Let HiMM Z = (X, T) be given

    Proofs: We continue with the proofs. Proof: [Proof of Proposition 7] Let HiMM Z = (X, T) be given. The key observation for showing Proposition 7 is to note that the marked MMs of Z will always either form a subtree of T that includes the root of T , or be empty (where the latter is the case if all MMs in Z have optimal exit costs that are up-to-date). The...

  43. [43]

    Let nadd (nto) be the number of times we add HiMMs to form Zadd (Zto) using either state addition or composition, similar to n

    Assume first that Z1 is formed by state addition, adding an HiMM Zadd to an HiMM Zto. Let nadd (nto) be the number of times we add HiMMs to form Zadd (Zto) using either state addition or composition, similar to n. Then, 24In particular, we mark the root MM of W ′. 25Note that Z1 must indeed exist since we start with the HiMMs in Z but eventually are left ...

  44. [44]

    Assume now that Z1 is formed by composition using an MM M. By induction, analogous to the state addition case, all the HiMMs in the composition fulfils the subtree- property, and since M (the root of Z1) is marked, we conclude that Z1 also fulfils the subtree-property. Combining the two cases, we conclude that Z1 fulfils the subtree-property, hence, Z ful...