On the Ability of Transformers to Verify Plans

Alexander Koller; Katharina Stein; Michael Hahn; Sylvie Thi\'ebaux; Yash Sarrof; Yupei Du

REVIEW 2 major objections 4 minor 26 references

On the Ability of Transformers to Verify Plans

T0 review · 2 major / 4 minor · reviewed 2026-07-13 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Transformers can learn to verify long plans when domains are delete-free or well-formed, but not for general STRIPS.

desk verdict Solid dichotomy for plan verification plus a real C-RASP extension; the stress-test rank objection is real but does not kill the paper. read the letter →

arxiv 2603.19954 v2 pith:PQE7NG3Z submitted 2026-03-20 cs.AI cs.CLcs.LG

Yash Sarrof , Yupei Du , Katharina Stein , Alexander Koller , Sylvie Thiébaux , Michael Hahn This is my paper · ORCID

classification cs.AIcs.CLcs.LG

keywords transformersplanverificationlengthgeneralizationC-RASPC*-RASPclassicalplanningSTRIPSwell-formeddomains

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Transformers succeed inconsistently on AI planning, and theory has been scarce on when length generalization should occur. This paper studies plan verification: given an instance and a candidate plan, decide whether the plan is valid. The hard case is when the number of objects (hence the input alphabet) can grow at test time. The authors introduce C*-RASP, an extension of C-RASP that gives length-generalization guarantees for transformers under simultaneous growth of sequence length and vocabulary. They prove that for delete-free and well-formed classical planning domains the verification language belongs to C*-RASP and is therefore learnable with perfect length generalization; unrestricted STRIPS and domains with conditional effects fall outside and can encode Flip-Flop or PARITY, which are known not to length-generalize. Experiments on Heavy Grippers, Colors, and Lights Out confirm the predicted split. The result matters because many practical planning benchmarks are well-formed, so the structural form of a domain, not merely size, decides whether transformers can reliably verify long plans.

What carries the argument

C*-RASP: an extension of C-RASP that adds a Match Predicate allowing object identities drawn from a growing alphabet to be compared only via local equality checks, without memorizing absolute identifiers; expressibility in C*-RASP is necessary and sufficient for length generalization of APE transformers under the idealized Inference Procedure that selects the minimal regularizer translation-invariant finite-precision model.

What would settle it

Train an APE transformer on short plans drawn from a well-formed domain (e.g., the well-formed Heavy Grippers or Colors variants) with a limited object set, then measure accuracy on much longer plans with many more objects; if accuracy collapses while the corresponding delete-free or well-formed C*-RASP program exists, the central claim fails.

Watch

Extended reading notes

Core claim

Plan verification for delete-free or well-formed domains lies in C*-RASP (and C-RASP[Pos] when the object set is fixed), so absolute-positional-encoding transformers length-generalize under the Symbolic Limit Transformer learning model; unrestricted STRIPS and conditional-effect domains lie outside C*-RASP and can encode Flip-Flop or PARITY, so length generalization is not expected.

Load-bearing premise

Learning is idealized as selecting, among all translation-invariant finite-precision transformers that match the target on short inputs using only a contiguous alphabet subset, the single model of lowest regularizer; that selection is assumed to converge to the unique Symbolic Limit Transformer that works at every length.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The useful takeaway is a clean structural split: delete-free and well-formed plan verification sit in C*-RASP (hence length-and-alphabet generalizable under their model), while unrestricted STRIPS and conditional effects can encode Flip-Flop or PARITY and sit outside. That organizes a lot of the mixed LLM-planning empirics and is immediately usable for the many IPC domains that already produce well-formed instances.

What is new is C*-RASP itself: the split alphabet, the Match predicate for object-argument equality without memorizing IDs, and the Symbolic Limit Transformer that extends Huang et al. (2025b) to simultaneous growth of length and vocabulary. The positive proofs are explicit counting programs that track proposition truth by net counts of matching actions; the negatives are concrete reductions. Empirics on three minimal-pair domains (Heavy Grippers, Colors, Lights Out) line up with the theory, including the sharp well-formed vs conditional-effects contrast on Lights Out even with fixed objects. Citations and self-citations to the C-RASP line look appropriate.

The soft spot is the one the stress-test flags. A fixed finite width d cannot realize exact equality indicators over an unbounded object alphabet via Tok-Tok products (Gram rank argument). The paper never spells out how Match is approximated or how the p-bit product functions evade this; the simulation claim for variable-universe C*-RASP is therefore incomplete as written. That is a genuine gap in Appendix C, not a minor omission. It does not erase the fixed-universe results or the empirical pattern, and the idealized inference procedure is the same style of assumption already used in the prior C-RASP literature, but it does mean the strongest variable-universe guarantee needs more work.

This is for people who care about length generalization of transformers or about when LLMs can be expected to verify plans. The math and data are careful enough that a serious referee should see it. I would engage, cite the dichotomy and the C*-RASP idea, and push on the Match simulation in review.

Referee Report

2 major / 4 minor

Summary. The paper analyzes length generalization of decoder-only transformers on plan verification (deciding whether a given plan solves a given classical planning instance). It distinguishes fixed-universe (fixed objects) and variable-universe (growing objects/alphabet) settings, and subclasses of domains (delete-free, well-formed, unrestricted STRIPS, conditional effects). For fixed universe it shows membership of the valid-plan language in C-RASP[Pos] for delete-free/well-formed domains (hence length-generalizable) and non-membership for some STRIPS and conditional-effect instances via reductions to Flip-Flop and PARITY. For variable universe it introduces C*-RASP (C-RASP plus a Match predicate for object-argument equality) and Symbolic Limit Transformers, claims that C*-RASP programs are simulated by the latter, and thereby obtains analogous positive/negative results (Theorems 3.1, 3.2, 3.5, 3.6). Empirics on Heavy Grippers, Colors and Lights Out variants corroborate the predicted generalization pattern.

Significance. If the claims hold, the work supplies the first theoretically grounded account of when transformers can length-generalize on plan verification, identifies a broad and practically relevant class of domains (well-formed, covering many IPC/Learning-Track benchmarks) for which this is possible, and introduces a reusable extension of the C-RASP framework to growing alphabets. The explicit C*-RASP programs, the reductions to known hard languages, the idealized but fully formalized learning model, and the matching empirical results (including code) are concrete strengths that would advance both the planning-with-LLMs literature and the length-generalization theory of transformers.

major comments (2)

The positive variable-universe claim (Thm. 3.6.1 / B.1) rests on every C*-RASP program, including those that use the Match predicate (Def. 3.3) to test object-argument equality, being simulable by a Symbolic Limit Transformer (Def. C.5). The latter object is required to have bounded residual dimension (the paper explicitly states that width d stays bounded while alphabet size diverges) together with bounded-norm embeddings {e_k} and local translation-invariant product functions α. Realizing exact equality indicators 1_{k=m} (needed for the exact counts that decide preconditions and goals) produces a Gram matrix of rank equal to the number of distinct objects M. That matrix is realized as E^ op AE and therefore has rank ≤ d. For every fixed d the construction is impossible once M > d. Consequently no single bounded-d Limit Transformer correctly evaluates Match-based counts on all finite i
The same rank obstruction appears inside the learning model (Sec. 3.2 / App. C). The Inference Procedure is claimed to converge to a unique Symbolic Limit Transformer because translation invariance + locality + the regularizer R leave only finitely many candidate algorithms (Thm. C.9). For any program that uses Match, however, exact agreement with the target on all length-n/2 inputs that employ a contiguous alphabet of size n/2 already requires residual dimension Ω(n). Either the hypothesis class Θ_n must allow d o ∞ (contradicting the bounded-d Limit) or, if R penalizes large d, no hypothesis matches the target for large n. In either case the finiteness argument and the claimed convergence fail for the very programs used in the positive proofs of Thm. 3.6.1.

minor comments (4)

The informal statement of Thm. 3.2 and the surrounding prose (p. 5) repeatedly assert that C*-RASP membership yields a length-generalization guarantee for APE transformers; after the simulation gap is repaired this claim should be restated with the precise hypotheses under which the guarantee holds.
Figure 1 and the overview paragraph of Sec. 1 list “STRIPS otin C-RASP[Pos]” while the body (Thm. 3.1.2) only shows existence of some STRIPS instances outside the class; a one-sentence clarification would avoid over-statement.
Appendix C.1.2 defines product functions over a Hilbert space H that is never declared finite- or infinite-dimensional; an explicit sentence would remove ambiguity about whether the rank argument can be circumvented.
In the experimental section the growth rate of the object set with plan length is not quantified; a short table or plot would make the “variable-universe” claim fully transparent.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: positive results rest on explicit C*-RASP program constructions and reductions to Flip-Flop/PARITY; the learning model is an idealized selection procedure whose convergence is proved, not fitted from data.

full rationale

The paper's central claims (Theorems 3.1/3.6 and the informal Theorem 3.2) are established by direct constructions: for delete-free and well-formed domains they write finite C-RASP[Pos] or C*-RASP programs that count adds/deletes (or use the Match predicate for object equality) and check preconditions/goals (Appendix A.1, B.1); for negative results they reduce fixed instances to Flip-Flop or PARITY, which are already known outside C-RASP[Pos] (and hence outside C*-RASP by the finite-alphabet reduction of Lemma C.22). The Symbolic Limit Transformer and Inference Procedure (Def. C.5, Theorem C.9) are defined and proved to converge under translation-invariance, locality and finite-precision constraints; no free parameters are fitted to experimental accuracy curves, and the experiments are purely corroborative. Self-citations to Huang et al. (2025b) supply the base C-RASP/Limit-Transformer framework (an independently published, parameter-free formal model used as a black-box tool). This is ordinary scientific reuse, not a load-bearing circular reduction: the planning-specific membership proofs and the C* extension are self-contained against the paper's own definitions and do not reduce by construction to the cited results. No uniqueness theorem is imported to forbid alternatives, no ansatz is smuggled, and no empirical pattern is merely renamed. The skeptic concern about bounded-width realization of exact Match is a potential correctness gap in the simulation claim, not a circularity (it does not make any claimed prediction equivalent to its inputs by definition).

Assumptions & free parameters 0 free parameters · 4 assumptions · 3 invented entities

The paper rests on the C-RASP length-generalization theorem of Huang et al. (2025b), standard STRIPS semantics, and an idealized learning model that forces locality and translation invariance. No numerical free parameters are fitted; the invented formal objects (C*-RASP, Symbolic Limit Transformer, Match Predicate) are definitional tools whose independent utility is demonstrated by the planning results.

assumptions (4)

domain assumption C-RASP[Pos] membership implies length generalization for APE transformers under the Limit Transformer learning model of Huang et al. (2025b).
Invoked throughout Section 3 and Appendix C as the base case that C*-RASP extends.
ad hoc to paper The Inference Procedure that selects the minimal-R translation-invariant finite-precision transformer matching the target on all length-n/2 inputs (restricted alphabet) converges to a unique Symbolic Limit Transformer.
Stated as Theorem C.9; the entire length-generalization guarantee for growing alphabets rests on this idealized selection model.
domain assumption Well-formedness: for every reachable state S and every effect literal l of an applicable action a, S satisfies the negation of l (i.e., every effect strictly changes the state).
Definition in Section 2.2; used to obtain the clean toggle-counting C*-RASP programs.
standard math Standard closed-world STRIPS semantics and the closed-world assumption for states.
Background from Fikes & Nilsson (1971) and Haslum et al. (2019); used for all formal definitions.

invented entities (3)

C*-RASP
purpose: Extension of C-RASP that admits a countably infinite object alphabet via a local Match Predicate while preserving length-generalization guarantees.
Definition 3.4; the sole new syntactic construct is the Match Predicate (Definition 3.3).
Symbolic Limit Transformer
purpose: Limiting object that unifies a sequence of finite transformers trained on increasing lengths and alphabets under locality and translation-invariance constraints.
Definition C.5; used to state the necessary-and-sufficient condition for generalization (Theorem 3.2 / C.9).
Match Predicate
purpose: Local equality checks between object tokens in fixed relative neighborhoods, allowing object identity matching without memorizing absolute identifiers.
Definition 3.3; the only addition to the C-RASP syntax.

how reviews work

0 comments

Cite this review

Pith. "Pith review of On the Ability of Transformers to Verify Plans." pith.science (2026). https://pith.science/paper/PQE7NG3Z

@misc{pith2026260319954,
  author       = {Pith},
  title        = {Pith review of: On the Ability of Transformers to Verify Plans},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PQE7NG3Z}},
  note         = {Machine review of arXiv:2603.19954}
}

read the original abstract

Transformers have shown inconsistent success in AI planning tasks, and theoretical understanding of when generalization should be expected has been limited. We take important steps towards addressing this gap by analyzing the ability of decoder-only models to verify whether a given plan correctly solves a given planning instance. To analyse the general setting where the number of objects -- and thus the effective input alphabet -- grows at test time, we introduce C*-RASP, an extension of C-RASP designed to establish length generalization guarantees for transformers under the simultaneous growth in sequence length and vocabulary size. Our results identify a large class of classical planning domains for which transformers can provably learn to verify long plans, and structural properties that significantly affects the learnability of length generalizable solutions. Empirical experiments corroborate our theory.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

26 extracted references · 1 linked inside Pith

[1]

Jiang, H., Hahn, M., Zetzsche, G., and Lin, A

URL �� . Jiang, H., Hahn, M., Zetzsche, G., and Lin, A. W. Soft- max transformers are turing-complete.arXiv preprint arXiv:2511.20038, 2025. 10 On the Ability of Transformers to Verify Plans Jobanputra, M., Veitsman, Y ., Sarrof, Y ., Bakalova, A., Dem- berg, V ., Pavlick, E., and Hahn, M. Born a transformer– always...

doi:10.1609/aaai 2025
[2]

Stein, K., Fiˇser, D., Hoffmann, J., and Koller, A

URL �� . Stein, K., Fiˇser, D., Hoffmann, J., and Koller, A. Automat- ing the generation of prompts for llm-based action choice in pddl planning. InProceedings of the 35th Interna- tional Conference on Automated Planning and Schedul- ing (ICAPS), pp. 250–259, 2025. Strobl, L. Average-hard attention transformers are ...

arXiv doi:10.1002/aaai.12169 2025
[3]

Weiss, G., Goldberg, Y ., and Yahav, E

URL �� . Weiss, G., Goldberg, Y ., and Yahav, E. Thinking like trans- formers. InInternational Conference on Machine Learn- ing, pp. 11080–11090. PMLR, 2021. Xiao, C. and Liu, B. Generalizing reasoning problems to longer lengths. InThe Thirteenth International Confer- ence on Learning Representations, 2025. Yang, A....

2021
[4]

Zhou, H., Bradley, A., Littwin, E., Razin, N., Saremi, O., Susskind, J

URL �� . Zhou, H., Bradley, A., Littwin, E., Razin, N., Saremi, O., Susskind, J. M., Bengio, S., and Nakkiran, P. What algorithms can transformers learn? A study in length generalization. InThe Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net, ...

2024
[5]

Proof of Statement 1

�� There exist domains with conditional effects such that L�� is neither star-free nor in ��[Pos]. Proof of Statement 1. In this setting, the domain D and the set of objects O are fixed and finite. However, the initial state I and the goal state G are provided as part of the input sequence, and can vary per sample. Given this settin...
[6]

We must identify which part of the input a token belongs to, using cumulative counts of separator tokens. CountSep(i) :=#[j≤i]Q � (j) Using this, we define the section selectors: • InInit(i) := (CountSep(i) == 0) • InPlan(i) := (CountSep(i) == 1) • InGoal(i) := (CountSep(i) == 2) • End(i) := (CountSep(i) == 3) The==syntax is equivalent to checking(CountSe...
[7]

Let a∈A be a specific ground action, defined by schema α and argument objects u�,

We first identify, at any indexi, whether an action has just completed and what that action is. Let a∈A be a specific ground action, defined by schema α and argument objects u�, . . . , u� . The action a ends at index i if the sequence of tokens ending atimatches the signature ofa: token ati=u � ,token ati−1 =u �� , . . . ,token ati−k=α 13 On the Ability...
[8]

These sets will be fixed and known a priori, given our fixed objects and domain

For every ground proposition p∈P , we identify the set of ground actions that add it, T P�, where T P� ={a∈A|p∈ eff(a)� }. These sets will be fixed and known a priori, given our fixed objects and domain. We define the cumulative count of additions forpat stepi: MadeTrue�(i) := ( � �� #[j≤i]OccursAction �(j)) We do the same for the set of actions that...

Show all 26 references

[9]

• Well-Formed: Because of well-formedness, the truth value of a proposition toggles (False → True → False)

Now, we define the truth value of a propositionpat stepi. • Well-Formed: Because of well-formedness, the truth value of a proposition toggles (False → True → False). We compute the net flow (adds minus deletes) for each proposition at every step. If the proposition was in the ...
[10]

We need to check that all the preconditions are satisfiedbeforethe action effect takes place

For every ground action a, let pre(a)� , pre(a)� define the list of positive and negative ground propositions for a given action. We need to check that all the preconditions are satisfiedbeforethe action effect takes place. We check the state of preconditions at i−1 (the state...
[11]

We iterate over our ground propositions

Finally, we need check if every goal condition is satisfied. We iterate over our ground propositions. For every proposition, either it does not appear in the goal or it is valid. GoalSat(i) := � �� ¬OccursGoal�(i)∨Valid �(i) At the end token, we need to check, that all goals ...

2022
[12]

In particular, generalization from both limited number of objects and plan lengths during training to a increased number of objects and plan lengths is expected

�� IfD is delete-free or well-formed, then L� ∈�� . In particular, generalization from both limited number of objects and plan lengths during training to a increased number of objects and plan lengths is expected
[13]

Generalization to instances with longer plans or increased number of objects is thus not expected

�� There exists STRIPS domains as well as domains with conditional effects for which L� /∈�� . Generalization to instances with longer plans or increased number of objects is thus not expected. In particular, there are domains whereL� subsumes F...
[14]

Section Identification:we must identify which part of the input a token belongs to, using cumulative counts of separator tokens. CountSep(i) :=#[j≤i]Q � (j) • InInit(i) := (CountSep(i) == 0) • InPlan(i) := (CountSep(i) == 1) • InGoal(i) := (CountSep(i) == 2) • End(i) := (Count...
[15]

•F P �: The set of action names along with placeholder object arguments α∈� that have p in their delete-effects (eff(α)� )

Precalculated Sets based on D:Since our D is fixed, we can precalculate the following sets for every predicate p∈ P and thus have them be plugged into our program whenever we want: •T P �: The subset of action names along with placeholder object arguments α in � that have p in...
[16]

Check presence of Action/Predicate:To check the presence of a specific action/ predicate, we can use our local function fromj. Curr� (i) =#[j≤i, i=j+arity(α)]Q � � (j)≥1 Curr�(i) =#[j≤i, i=j+arity(p)]Q � � (j)≥1 We can still useQhere as the number of predicates and action name...
[17]

Thus, we compare them exclusively through their positions relative to the object names

Match predicate:We have to determine if two different subsequences refer to the same ground proposition, and since our object universe is variable, object names cannot be directly compared against a fixed list. Thus, we compare them exclusively through their positions relative...
[18]

Precondition Check at every action:For a specific action instance α at i and a specific precondition p of α, we compute three values: (a)Provided by Init:Does the initial state contain the required ground proposition? V��(i) :=#[j < i] (InInit(j)∧χ ��Init��(i, j)) The ch...
[19]

We iterate over all predicates p∈ P

Finally, we check if all goal conditions are met. We iterate over all predicates p∈ P . For each predicate p, we perform validity checks at every position in the block where the goal proposition is of the type p (each such proposition may have different objects). We can constr...

2022
[20]

Locality & Translation Invariance for Related Types:When inputs share a type (Pos-Pos or Tok-Tok), then their interactions vanish if the distance exceeds a bandwidth∆∈� 11: |k−m|>∆ =⇒α �� = 0(10) Translation Invariance implies that for all shiftsδ, the behaviour remain...
[21]

Thus, the interaction collapses to aConstant

Translation Invariance for Unrelated Types:When inputs differ in type (Pos-Tok) or act singly (MLP-Pos), the interaction cannot pick out specific absolute indices from a structure it is unrelated to. Thus, the interaction collapses to aConstant. For any� � , if the other term ...
[22]

There existsC emb >0such that: sup �� ∥� �∥ ≤C emb andsup �� ∥�� ∥ ≤C emb (13)

Positional encodings {� �}�� and extended alphabet embeddings {�� }�� have globally bounded norms in H. There existsC emb >0such that: sup �� ∥� �∥ ≤C emb andsup �� ∥�� ∥ ≤C emb (13)
[23]

All weight matrices �∈ {� ��,� ��,� ��,� �,� �,�} are bounded linear operators on H, where their spectral norms are bounded
[24]

There exists dff ∈� such that � � :H →� � ff and � � :� � ff → H

For every layer l, the MLP projects to a finite-dimensional subspace. There exists dff ∈� such that � � :H →� � ff and � � :� � ff → H
[25]

Each product function must evaluate to a number in p-bit precision, for some fixed p∈�

The behavior of this transformer is governed by the set of scalar product functions defined earlier (Definition C.1). Each product function must evaluate to a number in p-bit precision, for some fixed p∈� . Crucially, these functions must satisfy theLocality and Translation In...
[26]

implies that the rest of the parameters are the same on both sides 24

Pith tools

Reviewed July 13, 2026 · model on record in the stance chip above.

[1] [1]

Jiang, H., Hahn, M., Zetzsche, G., and Lin, A

URL �� . Jiang, H., Hahn, M., Zetzsche, G., and Lin, A. W. Soft- max transformers are turing-complete.arXiv preprint arXiv:2511.20038, 2025. 10 On the Ability of Transformers to Verify Plans Jobanputra, M., Veitsman, Y ., Sarrof, Y ., Bakalova, A., Dem- berg, V ., Pavlick, E., and Hahn, M. Born a transformer– always...

doi:10.1609/aaai 2025

[2] [2]

Stein, K., Fiˇser, D., Hoffmann, J., and Koller, A

URL �� . Stein, K., Fiˇser, D., Hoffmann, J., and Koller, A. Automat- ing the generation of prompts for llm-based action choice in pddl planning. InProceedings of the 35th Interna- tional Conference on Automated Planning and Schedul- ing (ICAPS), pp. 250–259, 2025. Strobl, L. Average-hard attention transformers are ...

arXiv doi:10.1002/aaai.12169 2025

[3] [3]

Weiss, G., Goldberg, Y ., and Yahav, E

URL �� . Weiss, G., Goldberg, Y ., and Yahav, E. Thinking like trans- formers. InInternational Conference on Machine Learn- ing, pp. 11080–11090. PMLR, 2021. Xiao, C. and Liu, B. Generalizing reasoning problems to longer lengths. InThe Thirteenth International Confer- ence on Learning Representations, 2025. Yang, A....

2021

[4] [4]

Zhou, H., Bradley, A., Littwin, E., Razin, N., Saremi, O., Susskind, J

URL �� . Zhou, H., Bradley, A., Littwin, E., Razin, N., Saremi, O., Susskind, J. M., Bengio, S., and Nakkiran, P. What algorithms can transformers learn? A study in length generalization. InThe Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net, ...

2024

[5] [5]

Proof of Statement 1

�� There exist domains with conditional effects such that L�� is neither star-free nor in ��[Pos]. Proof of Statement 1. In this setting, the domain D and the set of objects O are fixed and finite. However, the initial state I and the goal state G are provided as part of the input sequence, and can vary per sample. Given this settin...

[6] [6]

We must identify which part of the input a token belongs to, using cumulative counts of separator tokens. CountSep(i) :=#[j≤i]Q � (j) Using this, we define the section selectors: • InInit(i) := (CountSep(i) == 0) • InPlan(i) := (CountSep(i) == 1) • InGoal(i) := (CountSep(i) == 2) • End(i) := (CountSep(i) == 3) The==syntax is equivalent to checking(CountSe...

[7] [7]

Let a∈A be a specific ground action, defined by schema α and argument objects u�,

We first identify, at any indexi, whether an action has just completed and what that action is. Let a∈A be a specific ground action, defined by schema α and argument objects u�, . . . , u� . The action a ends at index i if the sequence of tokens ending atimatches the signature ofa: token ati=u � ,token ati−1 =u �� , . . . ,token ati−k=α 13 On the Ability...

[8] [8]

These sets will be fixed and known a priori, given our fixed objects and domain

For every ground proposition p∈P , we identify the set of ground actions that add it, T P�, where T P� ={a∈A|p∈ eff(a)� }. These sets will be fixed and known a priori, given our fixed objects and domain. We define the cumulative count of additions forpat stepi: MadeTrue�(i) := ( � �� #[j≤i]OccursAction �(j)) We do the same for the set of actions that...