从自然语言意图到可执行控制：面向多组件信息物理系统的层次化反馈引导大模型规划

# From Natural Language Intent to Executable Control: Hierarchical Feedback-Guided LLM Planning for Multi-component Cyber-Physical Systems
Source: [https://arxiv.org/html/2610.22441](https://arxiv.org/html/2610.22441)
CCS:Software and its engineering Formal methodsCCS:Computer systems organization Embedded and cyber\-physical systems,Jiawan Wangemail:[wjwnju@nju\.edu\.cn](mailto:[email protected])Affiliation:Nanjing University,Nanjing,China,Ruiqi Hongemail:[rqhong@smail\.nju\.edu\.cn](mailto:[email protected])Affiliation:Nanjing University,Nanjing,ChinaandLei Buemail:[bulei@nju\.edu\.cn](mailto:[email protected])Affiliation:Nanjing University,Nanjing,China

© none

###### Abstract\.

Large language models \(LLMs\) provide a convenient interface for translating natural language commands into task plans for cyber\-physical systems \(CPSs\)\. However, two gaps hinder their use for real execution: generated plans may misinterpret or omit the user’s intent, and even a logically plausible plan may be infeasible under component dynamics, interactions, or safety constraints\. Existing LLM\-based planning approaches often lack informative feedback on why a generated plan fails, providing little guidance for revising the plan accordingly\.

To address these challenges, we present a hierarchical feedback framework that uses different types of feedback information to guide LLMs in generating executable plans for CPSs\. We prompt LLMs to generate both a structured task plan and corresponding signal temporal logic \(STL\) constraints, and design a sound algorithm that identifies definite contradictions between them and provides feedback for revising inconsistencies\. At the execution level, when control synthesis fails, we extract different types of diagnostic information, such as violated constraints and conflicting component assignments, and feed them back to guide task replanning\. Experiments on seven heterogeneous multi\-component CPS scenarios have shown that our framework can generate executable plans and feasible control executions that satisfy the original natural language missions with a success rate of 87\.9% with GPT\-5\.

###### Keywords:

Large Language Model \(LLM\), Cyber\-physical systems \(CPSs\), planning

## 1\.Introduction

Cyber\-physical systems \(CPSs\), which consist of multiple components with different capabilities, are increasingly expected to carry out complex missions in open physical environments\. Preparing task plans and inputs for control synthesis for these missions requires knowledge of the component models and the ability to express requirements formally\. This creates a need for interfaces that allow users without such expertise to describe missions in natural language and translate those descriptions into plans from which the underlying tools can synthesize feasible executions\.

Recent work\([Li et al\., 2026](https://arxiv.org/html/2610.22441#bib.bib1);[Kannan et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib2);[Xu et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib3);[Wu et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib4);[Chen et al\., 2024a](https://arxiv.org/html/2610.22441#bib.bib5)\)has explored large language models \(LLMs\) as natural language interfaces for multi\-agent task allocation and planning\. Given a natural language command, LLMs can be prompted to decompose the mission into subtasks and assign them to different agents for downstream execution\. Some work\([Kannan et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib2)\)then turns the resulting plan into executable code that runs the subtasks sequentially or in parallel in a simulator\. Other work\([Chen et al\., 2024a](https://arxiv.org/html/2610.22441#bib.bib5)\)uses LLMs to translate intent into intermediate representations, such as signal temporal logic \(STL\) formulas, which specify task goals and constraints for downstream planners\. However, some approaches\([Kannan et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib2);[Xu et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib3)\)do not include a repair loop after failure, while others\([Chen et al\., 2024a](https://arxiv.org/html/2610.22441#bib.bib5)\)primarily use feedback to correct syntactic and semantic errors in STL translation\. Effective repair must address both errors in the generated task structure and failures revealed when that structure is used for the underlying systems\. Two challenges remain in generating executable plans for CPSs:

Challenge 1:A semantic gap exists between a mission expressed in natural language and the task plan LLMs generate from it\. Requirements on task ordering and coordination may be omitted or misinterpreted during task decomposition\. A key challenge, therefore, is to expose errors in the translation of mission requirements into a task structure before attempting control synthesis\.

Challenge 2:A feasibility gap may arise between a task plan and a feasible execution in the target CPS\. Even when the plan captures the mission requirements, its execution depends on component dynamics, interactions among components, and physical and temporal constraints\. Some conflicts become apparent only during simulations or control synthesis\. Recovering from such failures may require changes to task decomposition or component allocation\. However, knowing that synthesis failed does not indicate which planning decisions should be reconsidered\.

For challenge 1, we prompt LLMs to produce two complementary representations of the same mission: a structured task plan that organizes how subtasks are carried out, and task\-level STL specifications that express temporal requirements on their execution\. This makes it possible to expose conflicts between the proposed task structure and the requirements expressed in the specifications\. We design a novel consistency checking algorithm to detect contradictions between the task plan and the STL specifications\. Detected contradictions provide feedback for revising the plan or specifications before control synthesis\.

For challenge 2, we extract diagnostic information from the underlying tool to guide replanning\. When synthesis fails, we analyze the failure logs to identify the probable cause\. We distinguish among several types of failures and extract corresponding diagnostic information, such as violations of physical constraints and conflicts caused by assigning the same component to parallel subtasks\. We return this information to the task plan generation stage so that the LLM can revise the task decomposition and component allocation while taking the system’s physical behavior into account\.

The main contributions of this work are as follows:

- –We design an algorithm to check the consistency between the task plans and STL specifications generated by LLMs\. It detects contradictions without constructing an execution, enabling repair before control synthesis\. \(See Sect\.[4\.2](https://arxiv.org/html/2610.22441#S4.SS2)\)
- –We extract control synthesis diagnostics to guide task replanning\. It links control synthesis failures to violated constraints, component behaviors, and affected tasks, providing diagnostic information for revising task decomposition and allocation\. \(See Sect\.[4\.3](https://arxiv.org/html/2610.22441#S4.SS3)\)
- –We implement the framework and evaluate it across seven heterogeneous multi\-component CPS scenes\. The framework achieves an overall success rate of 87\.9% with GPT\-5\. \(See Sect\.[5](https://arxiv.org/html/2610.22441#S5)\)

## 2\.Background

### 2\.1\.Preliminaries

This section introduces the concepts used throughout the paper\. Section[2\.2](https://arxiv.org/html/2610.22441#S2.SS2)presents a detailed example that illustrates each of them\. We begin with hybrid automata \(HAs\), which we use to model each component of a CPS\. HAs capture both discrete mode transitions and continuous dynamics\.

###### Definition 0\.

\(Hybrid Automaton\([Henzinger, 1996](https://arxiv.org/html/2610.22441#bib.bib6)\)\)\. A hybrid automaton is a tuple

H=\(X,Q,F,I​n​v,E,G,R\),H=\(X,Q,F,Inv,E,G,R\),whereXXis a set of real\-valued variables,QQis a set of discrete modes,FqF\_\{q\}defines the continuous flow in modeqq,I​n​vqInv\_\{q\}is the invariant of modeqq,E⊆Q×QE\\subseteq Q\\times Qis a set of discrete transitions,GeG\_\{e\}andReR\_\{e\}are the guard and reset of transitionee, respectively\.

The state ofHHis a pair\(q,x\)∈Q×ℝ\|X\|\(q,x\)\\in Q\\times\\mathbb\{R\}^\{\|X\|\}\. It can evolve continuously inside the current modeqqaccording toFqF\_\{q\}as long asI​n​vqInv\_\{q\}holds, or jump discretely through a transitioneewhen its guardGeG\_\{e\}is satisfied, after which variables are updated by the resetReR\_\{e\}\.

We further partition the transition setEEinto activated transitionsEa​c​tE\_\{act\}and automatic transitionsEa​u​t​oE\_\{auto\}, withE=Ea​c​t∪Ea​u​t​oE=E\_\{act\}\\cup E\_\{auto\}andEa​c​t∩Ea​u​t​o=∅E\_\{act\}\\cap E\_\{auto\}=\\emptyset\. Transitions inEa​c​tE\_\{act\}require explicit activation through an atomic task configuration, whereas transitions inEa​u​t​oE\_\{auto\}do not require such activation\. Fig\.[1](https://arxiv.org/html/2610.22441#acmlabel1)illustrates the hybrid automaton used by the truck component in the motivating example in Section[2\.2](https://arxiv.org/html/2610.22441#S2.SS2)\. The controllablenotifytransition belongs toEa​c​tE\_\{act\}and sets the target parameters, while thearrivetransition belongs toEa​u​t​oE\_\{auto\}and triggers when the truck reaches the target region\.

Figure 1\.Hybrid automaton model of a truck component and an example atomic task\.Truck hybrid automaton and an example atomic task configuration\.The overall mission may be complex and can be decomposed into various subtasks\. Subtasks may be executed either concurrently or sequentially\. We use a specified structure calledScenario Task\([Wang et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib7)\)to describe the whole task plan\.

###### Definition 0\.

\(Scenario Task\)\. A scenario task is recursively definedST=AT\|\(ST;ST\)\|\(ST∥ST\)ST=AT\\;\|\\;\(ST\\mathbin\{;\}ST\)\\;\|\\;\\allowbreak\(ST\\parallel ST\), whereA​TATis an atomic task,\(S​T;S​T\)\(ST\\mathbin\{;\}ST\)denotes the sequential execution of two scenario tasks, and\(ST∥ST\)\(ST\\parallel ST\)denotes the parallel composition of two scenario tasks\. Therefore, it can either be a single atomic task or a sequential/parallel compositional task\.

###### Definition 0\.

\(Atomic Task\)\. An atomic task is the smallest task unit, and it specifies which components participate and which action they should choose\. Formally, an atomic task is a tuple

A​T=\(Aa,Ua,qa0,qaf\),AT=\(A\_\{a\},U\_\{a\},q\_\{a\}^\{0\},q\_\{a\}^\{f\}\),whereAaA\_\{a\}is the set of involved component instances,UaU\_\{a\}is the set of activated transitions with parameter bindings, andqa0,qafq\_\{a\}^\{0\},q\_\{a\}^\{f\}specify the expected initial and final modes of the participating components\. Among them,UaU\_\{a\}specifies which transitions should be activated, along with their reset parameters\. Figure[1](https://arxiv.org/html/2610.22441#acmlabel1)\(b\) illustrates an example atomic task configuration\.

Signal Temporal Logic \(STL\) is commonly used to specify requirements for control synthesis in CPSs\. It can specify not only logical relationships but also dense\-time constraints\. We use it to capture temporal behaviors and requirements in multi\-component CPSs\.

###### Definition 0\.

\(Signal Temporal Logic\([Maler and Nickovic, 2004](https://arxiv.org/html/2610.22441#bib.bib8)\)\)\. The syntax of an STL formulaφ\\varphiinterpreted over a set of atomic predicatesΠ\\Piis defined as:

φ:=𝑡𝑟𝑢𝑒​∣p∣​¬φ1​∣φ1∨φ2∣​φ1​𝒰𝐈​φ2\.\\varphi:=\\mathit\{true\}\\mid p\\mid\\neg\\varphi\_\{1\}\\mid\\varphi\_\{1\}\\vee\\varphi\_\{2\}\\mid\\varphi\_\{1\}\\mathcal\{U\}\_\{\\mathbf\{I\}\}\\;\\varphi\_\{2\}\.
wherep∈Πp\\in\\Pi,𝒰\\mathcal\{U\}denotes the until operator, and𝐈⊆ℝ≥0\\mathbf\{I\}\\subseteq\\mathbb\{R\}\_\{\\geq 0\}denotes a timing interval, which can be omitted when it is\[0,∞\)\[0,\\infty\)\. Other standard operators can be derived as follows:𝑓𝑎𝑙𝑠𝑒≡¬𝑡𝑟𝑢𝑒\\mathit\{false\}\\equiv\\neg\\mathit\{true\},φ1∧φ2≡¬\(¬φ1∨¬φ2\)\\varphi\_\{1\}\\wedge\\varphi\_\{2\}\\equiv\\neg\(\\neg\\varphi\_\{1\}\\vee\\neg\\varphi\_\{2\}\),φ1→φ2≡¬φ1∨φ2\\varphi\_\{1\}\\rightarrow\\varphi\_\{2\}\\equiv\\neg\\varphi\_\{1\}\\vee\\varphi\_\{2\},◇I​φ≡𝑡𝑟𝑢𝑒​𝒰𝐈​φ\\Diamond\_\{I\}\\varphi\\equiv\\mathit\{true\}\\;\\mathcal\{U\}\_\{\\mathbf\{I\}\}\\;\\varphi, and□I​φ≡¬◇I​\(¬φ\)\\Box\_\{I\}\\varphi\\equiv\\neg\\Diamond\_\{I\}\(\\neg\\varphi\)\.

Semantics:An STL formulaφ\\varphihas Boolean semantics that define its satisfaction relation over a signalssat a timett\. This satisfaction relation is defined inductively as follows:

\(1\)\(s,t\)⊧p↔πp​\(s\)​\[t\]=True\(s,t\)⊧¬φ↔\(s,t\)⊧̸φ\(s,t\)⊧φ1∨φ2↔\(s,t\)⊧φ1​or​\(s,t\)⊧φ2\(s,t\)⊧φ1​𝒰\[a,b\]​φ2↔∃t′∈\[t\+a,t\+b\]​s\.t\.​\(s,t′\)⊧φ2and​∀t′′∈\[t,t′\),\(s,t′′\)⊧φ1\\begin\{split\}\(s,t\)\\models p&\\leftrightarrow\\pi\_\{p\}\(s\)\[t\]=\\text\{True\}\\\\ \(s,t\)\\models\\neg\\varphi&\\leftrightarrow\(s,t\)\\not\\models\\varphi\\\\ \(s,t\)\\models\\varphi\_\{1\}\\vee\\varphi\_\{2\}&\\leftrightarrow\(s,t\)\\models\\varphi\_\{1\}\\text\{ or \}\(s,t\)\\models\\varphi\_\{2\}\\\\ \(s,t\)\\models\\varphi\_\{1\}\\mathcal\{U\}\_\{\[a,b\]\}\\varphi\_\{2\}&\\leftrightarrow\\exists t^\{\\prime\}\\in\[t\+a,t\+b\]\\text\{ s\.t\. \}\(s,t^\{\\prime\}\)\\models\\varphi\_\{2\}\\\\ &\\quad\\text\{ and \}\\forall t^\{\\prime\\prime\}\\in\[t,t^\{\\prime\}\),\(s,t^\{\\prime\\prime\}\)\\models\\varphi\_\{1\}\\end\{split\}
STL conventionally uses atomic predicates over continuous states, such as numerical conditions on the variables of CPS components\. In this work, we additionally definetask predicatesto express whether a scenario task has begun or finished\. Thus, our STL formulas may refer to both component states and task status\.

###### Definition 0\.

\(Task Predicates\)\. For a scenario taskS​TST, the predicate\_​T​a​s​k​B​e​g​i​n​\(S​T\)\\\_TaskBegin\(ST\)indicates thatS​TSThas begun, and\_​T​a​s​k​F​i​n​i​s​h​\(S​T\)\\\_TaskFinish\(ST\)indicates thatS​TSThas finished\.

Semantics:These predicates have cumulative semantics\. Once the taskS​TSThas begun,\_​T​a​s​k​B​e​g​i​n​\(S​T\)\\\_TaskBegin\(ST\)remains true at all later times; otherwise, it is false\. Similarly, once taskS​TSThas finished,\_​T​a​s​k​F​i​n​i​s​h​\(S​T\)\\\_TaskFinish\(ST\)remains true at all later times; otherwise, it is false\.

###### Definition 0\.

\(State Predicates\)\. The state predicate is a numeric condition over the continuous variables of CPS components, such asθ⁡\(𝐱\)≥d\\theta\(\\mathbf\{x\}\)\\geq d\.

Overall, STL formulas over task status predicates specify requirements on task progression, while formulas over state predicates specify requirements on physical trajectories\.

### 2\.2\.Motivating Example

![Motivating Example.](https://arxiv.org/html/2610.22441v1/Example.png)Figure 2\.Motivating Example\.Motivating Example\.Consider a multi\-component CPS scenario with two trucks \(t1t\_\{1\},t2t\_\{2\}\) and one robotic arm \(a​r​marm\)\. The system undertakes the following mission: both trucks move to their respective destinations in parallel, arrive within 20 seconds, and maintain a distance of at least 1 metre throughout the mission\. After both trucks arrive, use the arm to unload the object from truck 1 into the place zone, then unload the object from truck 2\. As shown in Fig\.[2](https://arxiv.org/html/2610.22441#S2.F2)\(a\),t1t\_\{1\}starts at\(0,0,0\)\(0,0,0\)and targetsg1=\(10,10,0\)g\_\{1\}=\(10,10,0\), whilet2t\_\{2\}starts at\(0,10,0\)\(0,10,0\)and targetsg2=\(10,0,0\)g\_\{2\}=\(10,0,0\)\. Both trucks travel at1​m/s1\\,\\mathrm\{m/s\}\. The arm is based at\(10,5,3\)\(10,5,3\)and places the objects inZ=\[12,13\]×\[0,10\]×\{0\}Z=\[12,13\]\\times\[0,10\]\\times\\\{0\\\}\.

We use this mission to illustrate both the concepts introduced in Section[2\.1](https://arxiv.org/html/2610.22441#S2.SS1)and the two challenges identified in Section[1](https://arxiv.org/html/2610.22441#S1)\. We show an LLM\-generated initial task plan in Fig\.[2](https://arxiv.org/html/2610.22441#S2.F2)\(b\), which can be represented as a scenario task:

\(2\)𝑚𝑖𝑠𝑠𝑖𝑜𝑛0\\displaystyle\\mathit\{mission\}\_\{0\}=𝑡𝑟𝑎𝑛𝑠𝑝𝑜𝑟𝑡\|𝑢𝑛𝑙𝑜𝑎𝑑,\\displaystyle=\\mathit\{transport\}\\parallel\\mathit\{unload\},𝑡𝑟𝑎𝑛𝑠𝑝𝑜𝑟𝑡\\displaystyle\\mathit\{transport\}=𝑚𝑜𝑣𝑒t1\|𝑚𝑜𝑣𝑒t2,\\displaystyle=\\mathit\{move\_\{t\_\{1\}\}\}\\parallel\\mathit\{move\_\{t\_\{2\}\}\},𝑢𝑛𝑙𝑜𝑎𝑑\\displaystyle\\mathit\{unload\}=𝑝𝑖𝑐𝑘t1;𝑑𝑟𝑜𝑝t1;𝑝𝑖𝑐𝑘t2;𝑑𝑟𝑜𝑝t2\.\\displaystyle=\\mathit\{pick\_\{t\_\{1\}\}\}\\mathbin\{;\}\\mathit\{drop\_\{t\_\{1\}\}\}\\mathbin\{;\}\\mathit\{pick\_\{t\_\{2\}\}\}\\mathbin\{;\}\\mathit\{drop\_\{t\_\{2\}\}\}\.
Its root runs the transportation tasktransportin parallel with the unloading taskunload\. Transportation consists of two parallel routes, while unloading consists of four sequential actions\. The subtasksm​o​v​et1move\_\{t\_\{1\}\}andm​o​v​et2move\_\{t\_\{2\}\}move the respective trucks directly tog1g\_\{1\}andg2g\_\{2\}\. The arm executesp​i​c​kt1pick\_\{t\_\{1\}\}to retrieve the object fromt1t\_\{1\}atg1g\_\{1\}, followed byd​r​o​pt1drop\_\{t\_\{1\}\}to deposit it inZZ, and repeats the same action fort2t\_\{2\}\. Thus, the leaf assignments are\{t1\}\\\{t\_\{1\}\\\}form​o​v​et1move\_\{t\_\{1\}\},\{t2\}\\\{t\_\{2\}\\\}form​o​v​et2move\_\{t\_\{2\}\}, and\{𝑎𝑟𝑚\}\\\{\\mathit\{arm\}\\\}for each manipulation task\.

Figure[1](https://arxiv.org/html/2610.22441#acmlabel1)\(b\) expands one atomic task,A​Tm​o​v​et1=\(Aa,Ua,qa0,qaf\)AT\_\{move\_\{t\_\{1\}\}\}=\(A\_\{a\},U\_\{a\},q\_\{a\}^\{0\},q\_\{a\}^\{f\}\)\. Its component set isAa=\{t1\}A\_\{a\}=\\\{t\_\{1\}\\\};UaU\_\{a\}activatest1\.n​o​t​i​f​yt\_\{1\}\.\{notify\}with target parameters\(10,10,0\)\(10,10,0\); andqa0=qaf=I​d​l​eq\_\{a\}^\{0\}=q\_\{a\}^\{f\}=Idle\. These fields connect the atomic task to the truck HA in Fig\.[1](https://arxiv.org/html/2610.22441#acmlabel1): the controllablenotifytransition entersMoving, the continuous flow advances the truck toward its target, and the automaticarrivetransition returns it toIdlewhen the arrival guard holds\. The configuration therefore specifies both the participating component and the behavior it must execute\.

For task predicates, two representative LLM\-generated constraints are

\(3\)φorder\\displaystyle\\varphi\_\{\\mathrm\{order\}\}=□⁡\(\_​T​a​s​k​B​e​g​i​n​\(𝑝𝑖𝑐𝑘t1\)→\_​T​a​s​k​F​i​n​i​s​h​\(𝑚𝑜𝑣𝑒t1\)\),\\displaystyle=\\Box\\bigl\(\\\_TaskBegin\(\\mathit\{pick\_\{t\_\{1\}\}\}\)\\rightarrow\\\_TaskFinish\(\\mathit\{move\_\{t\_\{1\}\}\}\)\\bigr\),\(4\)φtime\\displaystyle\\varphi\_\{\\mathrm\{time\}\}=◇\[0,20\]​\_​T​a​s​k​F​i​n​i​s​h​\(𝑡𝑟𝑎𝑛𝑠𝑝𝑜𝑟𝑡\)\.\\displaystyle=\\Diamond\_\{\[0,20\]\}\\\_TaskFinish\(\\mathit\{transport\}\)\.The first requires truckt1t\_\{1\}to have arrived by the time the arm begins unloading the object fromt1t\_\{1\}\. The second requires the transportation task to finish within 20 seconds\.

For state predicates, let𝐩i\\mathbf\{p\}\_\{i\}be the position of trucktit\_\{i\}\. Two representative constraints are

\(5\)ψsafe\\displaystyle\\psi\_\{\\mathrm\{safe\}\}=□⁡\(‖𝐩1−𝐩2‖2≥1\),\\displaystyle=\\Box\\bigl\(\\\|\\mathbf\{p\}\_\{1\}\-\\mathbf\{p\}\_\{2\}\\\|\_\{2\}\\geq 1\\bigr\),\(6\)ψarrive\\displaystyle\\psi\_\{\\mathrm\{arrive\}\}=◇\[0,20\]​\(‖𝐩1−g1‖∞<ϵ∧‖𝐩2−g2‖∞<ϵ\),\\displaystyle=\\Diamond\_\{\[0,20\]\}\\Bigl\(\\\|\\mathbf\{p\}\_\{1\}\-g\_\{1\}\\\|\_\{\\infty\}<\\epsilon\\ \\wedge\\\|\\mathbf\{p\}\_\{2\}\-g\_\{2\}\\\|\_\{\\infty\}<\\epsilon\\Bigr\),
whereϵ\\epsilonis a small positive tolerance, and the infinity norm requires the absolute error in each coordinate to be less thanϵ\\epsilon\. The first constraint requires the trucks to maintain a separation of at least 1 metre throughout the mission\. The second requires both trucks to be within their destinations within 20 seconds\.

In this example, the LLM initially generates an incorrect plan that executes𝑡𝑟𝑎𝑛𝑠𝑝𝑜𝑟𝑡\\mathit\{transport\}and𝑢𝑛𝑙𝑜𝑎𝑑\\mathit\{unload\}in parallel\. As a result,𝑝𝑖𝑐𝑘t1\\mathit\{pick\}\_\{t\_\{1\}\}begins when transportation begins, violating constraint[3](https://arxiv.org/html/2610.22441#S2.E3)\. This inconsistency follows from the task structure and can be detected without analyzing continuous motion\. We show later how this inconsistency is detected to guide revision in Section[4\.2](https://arxiv.org/html/2610.22441#S4.SS2)\.

Moreover, changing the root composition to𝑡𝑟𝑎𝑛𝑠𝑝𝑜𝑟𝑡;𝑢𝑛𝑙𝑜𝑎𝑑\\mathit\{transport\}\\mathbin\{;\}\\mathit\{unload\}resolves this ordering conflict, but does not by itself ensure physical feasibility\. Under the motion settings stated by LLMs, the trucks start their direct movements together and reach the intersection of their routes at the same time, violating constraint[5](https://arxiv.org/html/2610.22441#S2.E5)\. We revisit this example in Section[4\.3](https://arxiv.org/html/2610.22441#S4.SS3)to illustrate how this diagnostic information guides revision\.

## 3\.Problem Formulation

The preceding example illustrates a mission involving multiple CPS components and constraints on their execution\. We now formalize the problem of generating a feasible execution for such a mission\.

Inputs\.An input scene instance is represented as

\(7\)𝒮=\(ℳ,𝒲,ℋ\),\\mathcal\{S\}=\(\\mathcal\{M\},\\mathcal\{W\},\\mathcal\{H\}\),whereℳ\\mathcal\{M\}is the mission expressed in natural language,𝒲\\mathcal\{W\}is a structured description of the task environment, andℋ\\mathcal\{H\}contains the functional descriptions and hybrid automaton models of the CPS components\. Among them, the task environment is represented as

\(8\)𝒲=\(𝒵,𝒪,𝒞′\),\\mathcal\{W\}=\(\\mathcal\{Z\},\\mathcal\{O\},\\mathcal\{C^\{\\prime\}\}\),
where𝒵\\mathcal\{Z\}is the set of relevant zones,𝒪\\mathcal\{O\}describes the objects and obstacles in the scene, and𝒞′\\mathcal\{C^\{\\prime\}\}is the set of available component instances\. These elements are provided as structured entries specifying the relevant names and types, together with spatial coordinates or ranges\.

Output\.The desired output is a feasible execution traceρ\\rhoover the composed components\. We represent the trace as

ρ=\(𝐪0,𝐱0,t0\)→𝐞0\(𝐪1,𝐱1,t1\)→𝐞1⋯,\\rho=\(\\mathbf\{q\}\_\{0\},\\mathbf\{x\}\_\{0\},t\_\{0\}\)\\xrightarrow\{\\mathbf\{e\}\_\{0\}\}\(\\mathbf\{q\}\_\{1\},\\mathbf\{x\}\_\{1\},t\_\{1\}\)\\xrightarrow\{\\mathbf\{e\}\_\{1\}\}\\cdots,where𝐪i=\(qic\)c∈𝒞i\\mathbf\{q\}\_\{i\}=\(q\_\{i\}^\{c\}\)\_\{c\\in\\mathcal\{C\}\_\{i\}\}denotes the joint discrete state of the active components at timetit\_\{i\}, and𝐱i=\(xic\)c∈𝒞i\\mathbf\{x\}\_\{i\}=\(x\_\{i\}^\{c\}\)\_\{c\\in\\mathcal\{C\}\_\{i\}\}collects their continuous states \(variables\)\. Here,𝒞i\\mathcal\{C\}\_\{i\}is the set of active components, and𝐞i\\mathbf\{e\}\_\{i\}denotes the component transitions taken in the corresponding discrete step\. The trace also includes the continuous evolution between successive recorded states\.

The trace must be consistent with the component models inℋ\\mathcal\{H\}and the task environment𝒲\\mathcal\{W\}, and fulfill the original natural language missionℳ\\mathcal\{M\}\.

## 4\.Methodology

Figure 3\.Overview of the two\-stage framework with hierarchical feedback\.framework### 4\.1\.Framework Overview

To solve this problem, our framework generates a formal mission description:

\(9\)ℐ=\(T,Φ\)\.\\mathcal\{I\}=\(T,\\Phi\)\.Here,TTis a scenario task that organizes the mission into subtasks through sequential and parallel composition, andΦ\\Phicontains STL formulas specifying the objectives and constraints for control synthesis\. A feasible trace synthesized fromℐ\\mathcal\{I\}must followTTand satisfyΦ\\Phi\.

The two challenges discussed in Section[1](https://arxiv.org/html/2610.22441#S1)arise in constructing this description: the semantic gap concerns whetherℐ\\mathcal\{I\}capturesℳ\\mathcal\{M\}, whereas the feasibility gap concerns whether a feasible execution can be synthesized fromℐ\\mathcal\{I\}\. We address these challenges through a framework with two stages and hierarchical feedback, as shown in Fig\.[3](https://arxiv.org/html/2610.22441#S4.F3)\.

Algorithm 1Two\-Stage Synthesis with Hierarchical FeedbackInput :Scene instance

𝒮\\mathcal\{S\}, iteration budgets

K1,K2,K3K\_\{1\},K\_\{2\},K\_\{3\}
Output :Generated instance

ℐ\\mathcal\{I\}and feasible execution trace

ρ\\rho, or failure report

1for*i←1i\\leftarrow 1toK1K\_\{1\}*do

2for*j←1j\\leftarrow 1toK2K\_\{2\}*do

3Prompt the LLM to generate scenario task

TTand task\-level STLs

ΦT\\Phi\_\{T\}from

𝒮\\mathcal\{S\}
4

RT←CheckSyntax​\(ΦT\)R\_\{T\}\\leftarrow\\textnormal\{\{CheckSyntax\}\}\(\\Phi\_\{T\}\)
5if*RTR\_\{T\}reports no syntax error*then

6

RT←CheckConsistency​\(T,ΦT\)R\_\{T\}\\leftarrow\\textnormal\{\{CheckConsistency\}\}\(T,\\Phi\_\{T\}\)⊳\\trianglerightsee Algorithm[2](https://arxiv.org/html/2610.22441#algorithm2)

7if*RTR\_\{T\}reports no task\-level error*then

8break

9Update the stage\-I prompt with

RTR\_\{T\}⊳\\trianglerightconsistency\-guided revision

10for*ℓ←1\\ell\\leftarrow 1toK3K\_\{3\}*do

11Prompt the LLM to generate atomic task configurations for each

A​TATand control\-level STLs

ΦC\\Phi\_\{C\}
12

RC←CheckSyntax​\(T,ΦC\)R\_\{C\}\\leftarrow\\textnormal\{\{CheckSyntax\}\}\(T,\\Phi\_\{C\}\)
13if*RCR\_\{C\}reports a control\-level parsing error*then

14Update the stage\-II prompt with

RCR\_\{C\}continue

15

Φ←ΦT∪ΦC\\Phi\\leftarrow\\Phi\_\{T\}\\cup\\Phi\_\{C\}
16

ρ←InvokeControlSynthesizer​\(T,Φ\)\\rho\\leftarrow\\textnormal\{\{InvokeControlSynthesizer\}\}\(T,\\Phi\)
17if*ρ\\rhois feasible*then

18

ℐ←\(T,Φ\)\\mathcal\{I\}\\leftarrow\(T,\\Phi\)
19return

ℐ,ρ\\mathcal\{I\},\\rho
20

R←ToolFailureReport​\(\)R\\leftarrow\\textnormal\{\{ToolFailureReport\}\}\(\)⊳\\trianglerightlocalized execution diagnostics

21Update the stage\-I prompt with

RR⊳\\trianglerightdiagnostic\-guided replanning

22break

23returnfailure report

Given a scene instance𝒮\\mathcal\{S\}, we prompt an LLM to decompose the whole objective and construct the hierarchical structure ofTTthrough sequential and parallel composition\. In this stage, each atomic task initially contains a natural language description, stating its subgoal, participating components, and relevant objects or regions\. For example, the task𝑚𝑜𝑣𝑒t1\\mathit\{move\}\_\{t\_\{1\}\}in the motivating example can be described as “move truckt1t\_\{1\}tog1=\(10,10,0\)g\_\{1\}=\(10,10,0\)\.” This stage also generates*task\-level STL specifications*ΦT\\Phi\_\{T\}, which are formulas over the task predicates introduced in Definition[2\.5](https://arxiv.org/html/2610.22441#S2.Thmtheorem5)\. Before proceeding, the framework checks the syntax inΦT\\Phi\_\{T\}and uses a novel algorithm to check the inconsistencies between the plan and these specifications\. Detected errors are returned to Stage I to guide revision of the task plan or the specifications\.

Once the first stage reports no error, we prompt an LLM to convert the natural language description of each atomic task into the structured representation defined in Definition[2\.3](https://arxiv.org/html/2610.22441#S2.Thmtheorem3)\. Using the environment description𝒲\\mathcal\{W\}and component modelsℋ\\mathcal\{H\}, this stage specifies the participating components, activated transitions, and expected initial and final states\. This stage also generates*control\-level STL specifications*ΦC\\Phi\_\{C\}over the state predicates introduced in Definition[2\.6](https://arxiv.org/html/2610.22441#S2.Thmtheorem6)\. Representative constraints can be found in Section[2\.2](https://arxiv.org/html/2610.22441#S2.SS2)\. Once all atomic task configurations have been generated, the completedTTand the combined specificationsΦ=ΦT∪ΦC\\Phi=\\Phi\_\{T\}\\cup\\Phi\_\{C\}form the tool inputℐ\\mathcal\{I\}\. The framework checks the syntax ofΦC\\Phi\_\{C\}and task configurations\. Errors detected are directly returned to Stage II for correction without revising the accepted task\. Once the outputs pass these checks, the tool attempts to synthesize a feasible execution traceρ\\rhofromℐ\\mathcal\{I\}and the scene information\.

If control synthesis fails, the diagnostic reports are returned to Stage I as replanning feedback\. They guide revisions to the hierarchical structure of the task\. This feedback structure distinguishes local syntax corrections from replanning informed by control synthesis failures\. The framework returns the first feasible trace satisfying the generated specifications, or reports failure when the iteration budgets are exhausted\. Algorithm[1](https://arxiv.org/html/2610.22441#algorithm1)summarizes the process\.

### 4\.2\.Stage I: Intent\-Oriented Task Generation and Consistency Checking

In this stage, the LLMs are instructed to generate a task plan and a set of task\-level specifications, as mentioned before\. Generating both representations makes these requirements explicit and allows checking conflicts between them before control synthesis\.

The main difficulty is thatTTdetermines only a partial order over task events, rather than a complete timed execution\. The checker must therefore reason about concurrent tasks without fixing their execution times or imposing an arbitrary order\. We develop an algorithm that evaluatesΦT\\Phi\_\{T\}over this partial order using three\-valued logic\.

#### 4\.2\.1\.Consistency Checking Algorithm

Algorithm 2Task Plan and STL Consistency CheckingInput :Task treeTT; STL formulaφ\\varphi

Output :Value of

φ\\varphiat the entry event

1Construct

GDG\_\{D\}and

HHfrom

TT; let

ze0z\_\{e\_\{0\}\}be the entry node

2foreach*subformulaψ\\psiofφ\\varphiwith operands processed before their parent*do

3if*ψ\\psiis a Boolean constant*then

4Set

Vz​\(ψ\)V\_\{z\}\(\\psi\)to that constant for every

zz
5else if*ψ\\psiis a task predicate*then

6Compute

Vz​\(ψ\)V\_\{z\}\(\\psi\)using Eq\. \([12](https://arxiv.org/html/2610.22441#S4.E12)\)

7else if*ψ\\psiis a Boolean combination*then

8Combine its operand values at each node using Kleene logic

9else if*ψ\\psiis an unbounded temporal formula*then

10foreach*zzin reverse topological order ofHH*do

11if*SuccH⁡\(z\)=∅\\operatorname\{Succ\}\_\{H\}\(z\)=\\emptyset*then

12Use

Vz​\(α\)V\_\{z\}\(\\alpha\)for

◇​α\\Diamond\\alphaor

□​α\\Box\\alpha, and

Vz​\(β\)V\_\{z\}\(\\beta\)for

α​𝒰​β\\alpha\\mathcal\{U\}\\beta
13else

14Compute

Sz​\(ψ\)S\_\{z\}\(\\psi\)by Eq\. \([13](https://arxiv.org/html/2610.22441#S4.E13)\)

15Compute

Vz​\(ψ\)V\_\{z\}\(\\psi\)by Eq\. \([14](https://arxiv.org/html/2610.22441#S4.E14)\)

16else

17Set

Vz​\(ψ\)←𝖴𝗇𝗄𝗇𝗈𝗐𝗇V\_\{z\}\(\\psi\)\\leftarrow\\mathsf\{Unknown\}for every

zz
18return

Vze0​\(φ\)V\_\{z\_\{e\_\{0\}\}\}\(\\varphi\)

For each task \(node\)S​TSTinTT, we introduce its start eventS​T\.bST\.band finish eventS​T\.fST\.f\. These events determine when\_​T​a​s​k​B​e​g​i​n​\(S​T\)\\\_TaskBegin\(ST\)and\_​T​a​s​k​F​i​n​i​s​h​\(S​T\)\\\_TaskFinish\(ST\)become true\. We assume that every task has positive duration, sequential subtasks start when their predecessors finish, and parallel subtasks share a common start event\. Based on these relations, the algorithm first constructs an event relation graphG=\(V,E=,E<\)G=\(V,E\_\{=\},E\_\{<\}\)whereVVcontains these events,E=E\_\{=\}records simultaneous events, andE<E\_\{<\}records strict precedence \(one event must occur strictly before another\)\. The graphGGcaptures the logical dependencies among events and is constructed directly from the task plan, as follows\.

Every task contributesS​T\.b<S​T\.fST\.b<ST\.f\. A sequential taskST=\(st1;st2;⋯;stk\)ST=\(st\_\{1\}\\mathbin\{;\}st\_\{2\}\\mathbin\{;\}\\cdots\\mathbin\{;\}st\_\{k\}\)contributes

\(10\)S​T\.b=s​t1\.b,s​ti\.f=s​ti\+1\.b⁡\(1≤i<k\),s​tk\.f=S​T\.f\.ST\.b=st\_\{1\}\.b,\\qquad st\_\{i\}\.f=st\_\{i\+1\}\.b\\ \(1\\leq i<k\),\\qquad st\_\{k\}\.f=ST\.f\.A parallel taskST=\(st1∥st2∥⋯∥stk\)ST=\(st\_\{1\}\\parallel st\_\{2\}\\parallel\\cdots\\parallel st\_\{k\}\)contributes

\(11\)S​T\.b=s​ti\.b\(1≤i≤k\)\.ST\.b=st\_\{i\}\.b\\quad\(1\\leq i\\leq k\)\.
The algorithm does not impose ordering betweens​ti\.fst\_\{i\}\.f\. Although parallel subtasks share a common start event, they may finish at different times\. However, if the parallel task has a subsequent serial successorss, the algorithm addsy\.f<s\.fy\.f<s\.ffor every taskyyin the parallel subtree\. This follows from the sequential ordering between the parallel task andss\.

After constructingGG, the algorithm merges simultaneous events inE=E\_\{=\}using union\-find and projects the strict edges inE<E\_\{<\}onto their representatives, obtaining the directed acyclic graph \(DAG\)GD=\(VD,ED\)G\_\{D\}=\(V\_\{D\},E\_\{D\}\)\. We writerep⁡\(e\)∈VD\\operatorname\{rep\}\(e\)\\in V\_\{D\}for the representative of each evente∈Ve\\in V, and writeu⪯vu\\preceq vwhenu=vu=voru≺vu\\prec v\. To account for the time between ordered events, the algorithm constructs a new evaluation graphHHfromGDG\_\{D\}\. Each representativeeebecomes an event nodezez\_\{e\}, and each edgeu→v∈EDu\\to v\\in E\_\{D\}is replaced byzu→zu​v→zvz\_\{u\}\\to z\_\{uv\}\\to z\_\{v\}\. The interval nodezu​vz\_\{uv\}represents the open interval betweenuuandvv, during which other task events may occur\.

Finally, the algorithm assigns each subformula a value in\{𝖳𝗋𝗎𝖾,𝖥𝖺𝗅𝗌𝖾,𝖴𝗇𝗄𝗇𝗈𝗐𝗇\}\\\{\\mathsf\{True\},\\mathsf\{False\},\\mathsf\{Unknown\}\\\}at every node ofHH\. Here,𝖴𝗇𝗄𝗇𝗈𝗐𝗇\\mathsf\{Unknown\}means that the event ordering alone is insufficient to decide the value\.

Evaluating predicates\.For a task predicatepp, letevt⁡\(p\)\\operatorname\{evt\}\(p\)be the representative of its associated start or finish event\. Its value is

\(12\)Vze​\(p\)\\displaystyle V\_\{z\_\{e\}\}\(p\)=\{𝖳𝗋𝗎𝖾,evt⁡\(p\)⪯e,𝖥𝖺𝗅𝗌𝖾,e≺evt⁡\(p\),𝖴𝗇𝗄𝗇𝗈𝗐𝗇,otherwise,\\displaystyle=\\begin\{cases\}\\mathsf\{True\},&\\operatorname\{evt\}\(p\)\\preceq e,\\\\ \\mathsf\{False\},&e\\prec\\operatorname\{evt\}\(p\),\\\\ \\mathsf\{Unknown\},&\\text\{otherwise\},\\end\{cases\}Vzu​v​\(p\)\\displaystyle V\_\{z\_\{uv\}\}\(p\)=\{𝖳𝗋𝗎𝖾,evt⁡\(p\)⪯u,𝖥𝖺𝗅𝗌𝖾,v⪯evt⁡\(p\),𝖴𝗇𝗄𝗇𝗈𝗐𝗇,otherwise\.\\displaystyle=\\begin\{cases\}\\mathsf\{True\},&\\operatorname\{evt\}\(p\)\\preceq u,\\\\ \\mathsf\{False\},&v\\preceq\\operatorname\{evt\}\(p\),\\\\ \\mathsf\{Unknown\},&\\text\{otherwise\}\.\\end\{cases\}These rules determine whether the event has already occurred or must occur later\. For an interval node, a definite value holds throughout the represented interval\. State predicates are assigned𝖴𝗇𝗄𝗇𝗈𝗐𝗇\\mathsf\{Unknown\}because their values require continuous states\.

Evaluating Boolean connectives\.Subformulas are evaluated from the leaves of the formula syntax tree upward\. We evaluate Boolean connectives using Kleene three\-valued logic\. For example,𝖥𝖺𝗅𝗌𝖾∧𝖴𝗇𝗄𝗇𝗈𝗐𝗇=𝖥𝖺𝗅𝗌𝖾\\mathsf\{False\}\\land\\mathsf\{Unknown\}=\\mathsf\{False\}, whereas𝖳𝗋𝗎𝖾∨𝖴𝗇𝗄𝗇𝗈𝗐𝗇=𝖳𝗋𝗎𝖾\\mathsf\{True\}\\lor\\mathsf\{Unknown\}=\\mathsf\{True\}\.

Evaluating temporal formulas\.For an unbounded temporal formula, the algorithm traversesHHin reverse topological order\. For a nodezzwith successors, let

\(13\)Sz​\(ψ\)=⋀z′∈SuccH⁡\(z\)Vz′​\(ψ\)\.S\_\{z\}\(\\psi\)=\\bigwedge\_\{z^\{\\prime\}\\in\\operatorname\{Succ\}\_\{H\}\(z\)\}V\_\{z^\{\\prime\}\}\(\\psi\)\.The conjunction returns𝖥𝖺𝗅𝗌𝖾\\mathsf\{False\}if any successor is false,𝖳𝗋𝗎𝖾\\mathsf\{True\}if all are true, and𝖴𝗇𝗄𝗇𝗈𝗐𝗇\\mathsf\{Unknown\}otherwise\. The temporal recurrences are

\(14\)Vz​\(◇​α\)\\displaystyle V\_\{z\}\(\\Diamond\\alpha\)=Vz​\(α\)∨Sz​\(◇​α\),\\displaystyle=V\_\{z\}\(\\alpha\)\\lor S\_\{z\}\(\\Diamond\\alpha\),Vz​\(□​α\)\\displaystyle V\_\{z\}\(\\Box\\alpha\)=Vz​\(α\)∧Sz​\(□​α\),\\displaystyle=V\_\{z\}\(\\alpha\)\\land S\_\{z\}\(\\Box\\alpha\),Vz​\(α​𝒰​β\)\\displaystyle V\_\{z\}\(\\alpha\\mathcal\{U\}\\beta\)=Vz​\(β\)∨\(Vz​\(α\)∧Sz​\(α​𝒰​β\)\)\.\\displaystyle=V\_\{z\}\(\\beta\)\\lor\\bigl\(V\_\{z\}\(\\alpha\)\\land S\_\{z\}\(\\alpha\\mathcal\{U\}\\beta\)\\bigr\)\.At a node with no successors, the respective base values areVz​\(α\)V\_\{z\}\(\\alpha\),Vz​\(α\)V\_\{z\}\(\\alpha\), andVz​\(β\)V\_\{z\}\(\\beta\)\. Operators with interval\[0,0\]\[0,0\]reduce to their current\-time operands:◇\[0,0\]​α\\Diamond\_\{\[0,0\]\}\\alphaand□\[0,0\]​α\\Box\_\{\[0,0\]\}\\alphatoα\\alpha, andα​𝒰\[0,0\]​β\\alpha\\mathcal\{U\}\_\{\[0,0\]\}\\betatoβ\\beta\. Other bounded temporal operators are assigned𝖴𝗇𝗄𝗇𝗈𝗐𝗇\\mathsf\{Unknown\}, since the graph does not determine elapsed time\.

Algorithm[2](https://arxiv.org/html/2610.22441#algorithm2)summarizes the check process\. It returns the value atze0z\_\{e\_\{0\}\}, wheree0=rep\(T\.b\)e\_\{0\}=\\operatorname\{rep\}\(T\.b\)\. After constructing the event graphs, the evaluation described above takesO​\(\|φ\|​\(n\+m\)\)O\(\|\\varphi\|\(n\+m\)\)time, where\|φ\|\|\\varphi\|is the number of subformulas, andnnandmmare the numbers of nodes and edges inHH, respectively\.

Figure 4\.Task plan and STL consistency checking for the motivating example\.Consistency Checking for Motivating Example\.Proposition 1 \(Soundness of the consistency checking algorithm\)\.Letℛ⁡\(GD\)\\mathcal\{R\}\(G\_\{D\}\)denote the set of all event\-time assignmentsτ:VD→ℝ≥0\\tau:V\_\{D\}\\rightarrow\\mathbb\{R\}\_\{\\geq 0\}satisfyingτ⁡\(u\)<τ⁡\(v\)\\tau\(u\)<\\tau\(v\)for every strict edge\(u,v\)∈ED\(u,v\)\\in E\_\{D\}\. Eachτ\\tauinduces a cumulative Boolean signalsτs\_\{\\tau\}over the task predicates,where, for a task predicatepep\_\{e\}associated with eventee,

\(15\)\(sτ,t\)⊧pe⟺τ\(e\)≤t\.\(s\_\{\\tau\},t\)\\models p\_\{e\}\\quad\\Longleftrightarrow\\quad\\tau\(e\)\\leq t\.The algorithm satisfies

\(16\)Vze0​\(φ\)=𝖥𝖺𝗅𝗌𝖾⟹∀τ∈ℛ⁡\(GD\),\(sτ,τ⁡\(e0\)\)⊧̸φ,V\_\{z\_\{e\_\{0\}\}\}\(\\varphi\)=\\mathsf\{False\}\\;\\Longrightarrow\\;\\forall\\tau\\in\\mathcal\{R\}\(G\_\{D\}\),\\;\(s\_\{\\tau\},\\tau\(e\_\{0\}\)\)\\not\\models\\varphi,wheree0=rep\(T\.b\)e\_\{0\}=\\operatorname\{rep\}\(T\.b\)is the entry event andze0z\_\{e\_\{0\}\}is its corresponding event node inHH\. Therefore, every formula rejected by the algorithm is genuinely inconsistent with every timing realization permitted by the event\-order abstraction\.

The result follows by mutual structural induction on definite truth and falsity, with a nested induction over the reverse topological order ofHHfor temporal formulas\. Equation \([12](https://arxiv.org/html/2610.22441#S4.E12)\) assigns a definite value to a task predicate only when the partial order guarantees that its associated event has already occurred, or has not yet occurred, throughout the time region represented by the current node\. Kleene three\-valued Boolean operations preserve the induction invariant\.

For temporal formulas, the successor aggregation in Eq\. \([13](https://arxiv.org/html/2610.22441#S4.E13)\) and the recurrences in Eq\. \([14](https://arxiv.org/html/2610.22441#S4.E14)\) preserve the same invariant\. In particular, every direct edgeu→vu\\to vinGDG\_\{D\}is represented inHHby an interval node corresponding to the entire open interval\(τ⁡\(u\),τ⁡\(v\)\)\(\\tau\(u\),\\tau\(v\)\)\. Ifuuhas multiple direct successors, their outgoing intervals share a nonempty time interval immediately afterτ⁡\(u\)\\tau\(u\), because all outgoing edges are strict and the graph is finite\. Consequently, a false successor certifies a violation over an actual time interval rather than merely along one graph path\. This prevents an intermediate event from being skipped and producing a spurious inconsistency report\.

#### 4\.2\.2\.Feedback and Revision

Syntax errors and formulas evaluated as𝖥𝖺𝗅𝗌𝖾\\mathsf\{False\}are returned to the same LLM session in Stage I to reviseTT,ΦT\\Phi\_\{T\}, or both\. In the motivating example,𝑝𝑖𝑐𝑘t1\.b\\mathit\{pick\}\_\{t\_\{1\}\}\.bmaps to the entry evente0e\_\{0\}, whilee0≺rep\(𝑚𝑜𝑣𝑒t1\.f\)e\_\{0\}\\prec\\operatorname\{rep\}\(\\mathit\{move\}\_\{t\_\{1\}\}\.f\)\. In Eq\. \([3](https://arxiv.org/html/2610.22441#S2.E3)\), the algorithm returns𝖥𝖺𝗅𝗌𝖾\\mathsf\{False\}forφorder\\varphi\_\{\\mathrm\{order\}\}, prompting a revision such as replacing the root composition with𝑡𝑟𝑎𝑛𝑠𝑝𝑜𝑟𝑡;𝑢𝑛𝑙𝑜𝑎𝑑\\mathit\{transport\}\\mathbin\{;\}\\mathit\{unload\}\. Therefore, the antecedent of the implication is true and its consequent is false at the entry event\. Figure[4](https://arxiv.org/html/2610.22441#S4.F4)shows the concrete process of evaluating the motivating example in Section[2\.2](https://arxiv.org/html/2610.22441#S2.SS2)\.

### 4\.3\.Stage II: Executability\-Oriented Control Synthesis and Diagnostic Feedback

After task\-level checking, feasibility still depends on how the atomic tasks are realized by the CPS components\. Stage II therefore connects each task description to concrete component behaviors and submits the resulting mission description to control synthesis\. Using the environment description𝒲\\mathcal\{W\}and component modelsℋ\\mathcal\{H\}, we prompt an LLM to convert each task description into the configurationA​TATdefined in Definition[2\.3](https://arxiv.org/html/2610.22441#S2.Thmtheorem3)\. A key step is selecting the transitions to activate\. A component HA model may provide several functions, but only a subset is needed for a given task\. For example, a robotic arm may expose transitions for grasping, and placing\. To ground a placing task, the LLM should select the placing transition and binds the target position through reset variables\. The LLM also generates control\-level STL specificationsΦC\\Phi\_\{C\}as mentioned before\.

The framework therefore submit the completed mission descriptionℐ=\(T,Φ\)\\mathcal\{I\}=\(T,\\Phi\)to the underlying control synthesis tool\([Wang et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib7)\)\. We extend the tool’s diagnostic reports to connect failures in the generated behavior to the tasks and components involved, providing feedback for revisingℐ\\mathcal\{I\}\.

Input validation\.Before synthesis, an STL parser checks the syntax ofΦC\\Phi\_\{C\}, while the tool’s input parser validates the task configurations inTT\. Errors detected by these checks are directly returned to Stage II for correction\. Once the input passes validation, the tool attempts to synthesize a feasible execution under the component models and the specifications\.

Control Synthesis diagnostics\.For failures reported during control synthesis, we extract diagnostic information about the failed requirement or component behavior and associate it with the relevant tasks and components\. The following diagnostic categories support this connection between synthesis failures and task revision\.

*STL violations\.*The report identifies the violated specification and the tasks active when the violation is detected\.

*Conflicting component assignments\.*When parallel tasks demand incompatible simultaneous use of the same component, the report identifies that component and the conflicting tasks\. This exposes an allocation conflict that may require changing the participating components or the task composition\.

*Invariant violations\.*When a component’s continuous evolution violates the invariantI​n​vqInv\_\{q\}of its current mode, the report identifies the invariant, the affected component, and the associated active tasks\. This reveals a conflict between the planned behavior and the conditions under which the component may remain in that mode\.

*Guard failures\.*When a required transition cannot be taken because its guardGeG\_\{e\}is unsatisfied, the report identifies the transition, the unsatisfied guard, and the associated tasks\. The failure concerns a transition needed for task progress\.

Feedback routing and revision\.Synthesis failures are returned to Stage I because resolving them may require changes to task decomposition or component allocation\. The diagnostic reports connect the observed failure to the relevant tasks and requirements, guiding the LLM in reconsidering the plan rather than merely requesting another attempt\. The revised task plan and task\-level specifications undergo the Stage I checks again before Stage II regenerates the corresponding configurations and control\-level specifications\. This process continues until a feasible trace is obtained or the iteration budgets are exhausted\.

![Execution Feedback-Guided Repair.](https://arxiv.org/html/2610.22441v1/Example2.png)Figure 5\.Task plan repair guided by control synthesis feedback: resolving collision and deadline violations\.Execution Feedback\-Guided Repair\.Example\.We continue the motivating example after the ordering conflict has been corrected: transportation remains parallel, and unloading starts after transportation finishes, which shows in Fig\.[5](https://arxiv.org/html/2610.22441#S4.F5)\(a\)\. With the initial direct routes, the trucks reach\(5,5\)\(5,5\)simultaneously, violating the separation requirement in Eq\. \([5](https://arxiv.org/html/2610.22441#S2.E5)\)\. The synthesis tool reports the violated formula together with the two movement tasks, and this feedback is returned to Stage I\.

The first revision replaces each direct movement with a sequence of waypoint movements while retaining parallel transportation, producing Fig\.[5](https://arxiv.org/html/2610.22441#S4.F5)\(b\)\. Truck 1 follows\(0,0\)→\(10,5\)→\(10,10\)\(0,0\)\\rightarrow\(10,5\)\\rightarrow\(10,10\), and truck 2 follows\(0,10\)→\(5,15\)→\(15,15\)→\(15,0\)→\(10,0\)\(0,10\)\\rightarrow\(5,15\)\\rightarrow\(15,15\)\\rightarrow\(15,0\)\\rightarrow\(10,0\)\. Although the detour avoids the original collision, truck 2 must travel approximately37​m37\\,\\mathrm\{m\}\. At1​m/s1\\,\\mathrm\{m/s\}, it cannot meet the 20\-second deadline, so a further revision is required\.

After the second feedback, truck 1 follows\(0,0\)→\(10,0\)→\(10,10\)\(0,0\)\\rightarrow\(10,0\)\\rightarrow\(10,10\), while truck 2 follows\(0,10\)→\(0,0\)→\(10,0\)\(0,10\)\\rightarrow\(0,0\)\\rightarrow\(10,0\)\. Each route is20​m20\\,\\mathrm\{m\}long, corresponding to 20 seconds of ideal travel \(Fig\.[5](https://arxiv.org/html/2610.22441#S4.F5)\(c\)\.\)\. The trucks traverse their shared road segment at different times and maintain a minimum separation of approximately7​m7\\,\\mathrm\{m\}\. In this example, the feedback changes how the mission is carried out while retaining its safety, timing, and parallelism requirements\. It therefore illustrates how control synthesis diagnostics guide revisions to task decisions\.

## 5\.Experiment Evaluation

This section evaluates whether our proposed framework can turn scene instances into feasible executions for multi\-component CPSs\. We focus on the following three key questions:

RQ1:Can the full framework generate feasible controls that satisfy the original natural language missions across heterogeneous multi\-component CPS scenes and increasingly complex objectives?

RQ2:How much does our hierarchical feedback mechanism contribute to the success rate of the control generation?

RQ3:Can our work be extended to other scenarios, such as multi\-robot tasks? How does it perform compared with existing LLM\-to\-planning works?

### 5\.1\.Experimental Setup

Implementation\.We implement the prototype of our framework in Python for convenient access to LLM interfaces\. The underlying control synthesis tool SNIFF\([Wang et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib7)\)is implemented in C\+\+ for efficient low\-level solving\. We use it as the underlying search engine for feasible executions and extend its diagnostic interface to support LLM\-guided revision\. Three models, including DeepSeek\-V4\-Flash\([DeepSeek\-AI, 2026](https://arxiv.org/html/2610.22441#bib.bib9)\), GPT\-5 \(version gpt\-5\-2025\-08\-07\), and Qwen3\.7\-Plus, are involved in the experiments\. DeepSeek and Qwen are used with thinking mode enabled, and GPT\-5 is configured with a medium reasoning effort\. We use 3, 3, and 4 as the iteration budgets forK1K\_\{1\},K2K\_\{2\}, andK3K\_\{3\}, respectively, throughout the experiments\. These settings allow repeated repair attempts while limiting the overall running time\.

Benchmark\.The benchmark suite contains seven heterogeneous scenes that we built manually, two of which are adapted from AI2\-THOR\([Kolve et al\., 2022](https://arxiv.org/html/2610.22441#bib.bib10)\)simulation environments\. As summarized in Table[1](https://arxiv.org/html/2610.22441#S5.T1), the scenes cover diverse application domains, including object manipulation, spatial reasoning, household tasks, disaster response, and more\. Each scene contains four natural language objectives\. From objectives 1 to objectives 4 \(O1–O4\), the number of tasks or constraints is progressively increased during construction\. The LLMs may generate different task decompositions and STL formulas for the same objective\. Table[1](https://arxiv.org/html/2610.22441#S5.T1)therefore reports the average numbers of generated tasks \(including both atomic and composite tasks\) and STL formulas to describe the sizes of the resulting plans and specifications\.

Table 1\.Benchmark scenes and average numbers of generated task nodes and STL formulas\.Ablation study\.To evaluate the effectiveness of the proposed hierarchical feedback mechanism, we compare four strategies on the same set of scene instances:

- •Full:our complete method with all feedback channels enabled\.
- •No\-TSTL\-Check:disables the syntactic and semantic consistency check for task\-level STLs in stage 1 while keeping the rest of the pipeline unchanged\.
- •No\-Replan:stops a run when the synthesis tool reports a failure, rather than routing back to stage 1 for replanning\.
- •Simple\-Feedback:preserves the same feedback routing asFull, but replaces the detailed reports with a simple retry prompt\. Just inform the LLMs that an error has occurred\.

To ensure a fair comparison: \(1\) the run scripts randomize the execution order across strategies, and \(2\) each scene\-objective case is repeated five times to account for the stochasticity of LLMs\. In total, this ablation study evaluates 3 different LLMs across 7 scenes, 4 objectives per scene, 5 repetitions, and 4 strategies, resulting in1680runs\.

Comparison with multi\-robot planning methods\.We further compare our framework with two representative LLM\-based task planning approaches, SMART\-LLM\([Kannan et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib2)\)and NL2HLTL2PLAN\([Xu et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib3)\), on two AI2\-THOR household scenes \(scene 6 and scene 7\)\. Each scene contains four objectives, and similarly, each case is repeated five times for every method\.

The three frameworks differ in their outputs\. Our framework generates control trajectories, which are subsequently converted into executable AI2\-THOR Python code within an automated script\. SMART\-LLM generates Python code directly\. NL2HLTL2PLAN generates low\-level trajectories defined on its own grid abstraction, which must also be converted into code\.

Table 2\.Generation and verified success rates ofFullwith GPT\-5\.
### 5\.2\.Success Rates Across Heterogeneous Scenes

To answer RQ1, we examine not only whether the framework can generate feasible controls, but also whether these controls satisfy the intent of the original natural language missions\. Table[2](https://arxiv.org/html/2610.22441#S5.T2)reports the results ofFullwith GPT\-5, which achieves the highest overall success rate among the three evaluated models\.

We distinguish two success criteria\.*Generation success*means that the control synthesis tool successfully generates a feasible control from the LLM\-generated task plan and specifications\.*Verified success*further requires the generated control to satisfy the original natural language mission, as determined by automated checking scripts together with manual inspection\. The latter therefore provides a stricter end\-to\-end measure of whether the framework translates user intent into a feasible and semantically correct control\. Unless otherwise stated, all success rates reported for our framework from RQ2 onward use this theVerified successcriterion\.

Table[2](https://arxiv.org/html/2610.22441#S5.T2)shows thatFullachieves an overall generation success rate of 91\.4% and a verified success rate of 87\.9%, a gap of only 3\.5%\. This small gap indicates that, in most cases where control synthesis succeeds, the resulting control also satisfies the requirements expressed in the original natural language mission\.

The results remain strong as the objectives become more challenging\. From O1 to O4, the objectives introduce additional tasks or constraints, leading to larger task decompositions and more complex specifications, as summarized in Table[1](https://arxiv.org/html/2610.22441#S5.T1)\. As expected, O3 and O4 generally yield lower success rates than O1 and O2\. Nevertheless,Fullcontinues to achieve high verified success rates on these more complex objectives\. Together with the small gap between generation and verified success, these results show that the framework remains effective as mission complexity increases while largely preserving the original mission requirements\.

Answer to RQ1\.Our framework achieves high success rates across heterogeneous CPS scenes, including on more complex objectives\. Moreover, the small gap between generation and verified success shows that successfully generated controls generally satisfy the original natural language mission requirements\.

Table 3\.Ablation of hierarchical feedback: success rates and average runtime\.
### 5\.3\.Ablation Study of Hierarchical Feedback

To answer RQ2, we examine how the individual feedback mechanisms contribute to the success of our framework\. Table[3](https://arxiv.org/html/2610.22441#S5.T3)compares the four strategies on DeepSeek\-V4\-Flash, GPT\-5, and Qwen3\.7\-Plus\. Each row reports the average results across four task objectives\. Thesuccess ratedenotes the average task completion rate, andTime\(s\)reports the mean runtime over successful runs\.

Regarding overall performance, our framework \(strategyfull\) achieves the best aggregate success rate for all three LLM models: 76\.4% on DeepSeek\-V4\-Flash, 87\.9% on GPT\-5, and 81\.4% on Qwen3\.7\-Plus, outperforming all ablated variants\.

Among all strategies,No\-Replanconsumes the least time, which is expected because it performs at most one outer\-level planning attempt\. However, it exhibits the lowest success rate on all three models\. Its performance gap relative toFullshows the value of reconsidering planning decisions in response to synthesis failures, beyond correcting errors within the initial plan\.Simple\-Feedbackachieves the second lowest success rate, despite retaining the same feedback routing asFull\. These results show that simply notifying the LLMs that an error has occurred is not enough\. Localizing the fault and telling the model exactly what went wrong is also critically important\.No\-TSTL\-Checkyields comparatively better results\. Nevertheless, it lowers aggregate success on all three models\. The largest improvement from these checks occurs with GPT\-5:Fullgains 14\.3 percentage points over the setting without these checks\. These results support early task\-level validation as a complement to feedback from control synthesis\.

Answer to RQ2\.The results support early task validation and replanning guided by the control synthesis tool as complementary parts of the framework\. Replanning provides opportunities to recover from synthesis failures, while informative feedback makes those opportunities more effective\.

### 5\.4\.Comparison with Baselines on AI2\-THOR

Table 4\.Comparison with LLM\-based planning methods on AI2\-THOR\.This subsection answers RQ3 by comparing our framework with two representative LLM\-based task planning works, SMART\-LLM\([Kannan et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib2)\)and NL2HLTL2PLAN\([Xu et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib3)\)\. We report four evaluation metrics\.*Time \(s\)*measures the time from method invocation to completion of the final output\.*Generation success*follows each method’s own criterion: successful output reported by the underlying tool for our framework and NL2HLTL2PLAN, and production of Python code for SMART\-LLM\.*AI2\-THOR success*indicates whether the generated outputs can be executed successfully in the AI2\-THOR simulator\.*Travel cost*is the total movement distance across all agents, averaged over successful executions for each objective\.

Table[4](https://arxiv.org/html/2610.22441#S5.T4)shows that our framework not only achieves a high generation success rate but also attains a higher execution success in real simulations within AI2\-THOR\. Moreover, the travel cost further demonstrates the efficiency of our planning approach\. Although our method consumes a relatively large amount of time, mainly due to the multiple rounds of LLM calls, this additional cost is justified by the high success rate achieved during actual execution\. Figure[6](https://arxiv.org/html/2610.22441#S5.F6)illustrates a successful execution in Scene 6\.

SMART\-LLM exhibits substantial variation in success rate across the evaluated models\. With DeepSeek\-V4\-Flash and Qwen3\.7\-Plus, some generated responses contain explanatory text or Markdown formatting that prevents direct Python execution in its evaluated pipeline\. Most runs with Qwen3\.7\-Plus also exceed the default 600\-second request timeout\. With GPT\-5, SMART\-LLM achieves its highest execution success rates among the evaluated models, but remains below our framework in both scenes\. Its travel costs, averaged over successful executions, are also higher for most objectives\.

NL2HLTL2PLAN achieves generation success under its internal grid abstraction, but none of the resulting plans lead to a successful AI2\-THOR execution in our experiments\. In our integration, we observe failures when translating the generated grid trajectories into executable simulator actions\. This discrepancy highlights the distinction between success within the planning abstraction and successful execution in the target environment\.

Answer to RQ3\.On the two evaluated household scenes, our framework achieves higher end\-to\-end simulator execution success than the tested baselines\. The comparison supports its applicability to these multi\-robot tasks, while maintaining accuracy and reliability\.

![Successful Scene 6 execution generated by our method.](https://arxiv.org/html/2610.22441v1/ai2thor.png)Figure 6\.Successful execution of a Scene 6 mission in AI2\-THOR\.Successful Scene 6 execution generated by our method\.
### 5\.5\.Threats to Validity

LLM hallucination is an inherent threat to validity, as it may introduce syntactic errors in generated outputs or inconsistencies between task plans and STLs\. Nevertheless, we observe that the majority of such errors are successfully repaired under our iterative feedback loop\. The main source of failure is that the final plan still violates some complex control\-level temporal constraints after all repair attempts are exhausted\.

We also identify another category of failures\. Consider the motivating example, which requires two trucks to move in parallel toward their respective targets\. The LLMs initially decompose the objective into two parallel subtasks, but upon receiving collision constraint violation reports from the control synthesis tool, they may restructure the plan by serializing the two subtasks — unintentionally abandoning the "in parallel" requirement of the original natural language objective\. In fact, the resulting plan and trajectory are physically safe and executable, and the control synthesis is successful and can not afford failure information\. We count such cases as failures under our strict evaluation criterion\. We will further explore how to guide LLMs to generate plans that conform to constraints while better preserving high\-level semantic intent in future work\.

## 6\.Related Work

Temporal logic\-based CPS control synthesis and planning\.Temporal logic has long been used to specify temporal constraints and requirements\. A line of work studies temporal logic falsification, which aims to find counterexamples in systems that violate the given temporal logic specifications\. S\-TaLiRo\([Annpureddy et al\., 2011](https://arxiv.org/html/2610.22441#bib.bib11)\)provided an advanced optimization\-based CPS falsification tool\. SNIFF\([Wang et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib7)\)designed a scenario\-based hierarchical modeling language to formalize reconfigurable CPSs and developed a path\-oriented approach to falsify temporal logic specifications for CPSs\.

A related class of temporal logic for CPS falsification is temporal logic for planning\. Luo et al\.\([Luo and Liu, 2025](https://arxiv.org/html/2610.22441#bib.bib12)\)developed a search\-based approach to synthesize plans for multi\-robot systems under temporal logic specifications\. Real\-time reactive task allocation and planning under temporal logic specifications have also been studied for large heterogeneous multi\-robot systems\([Chen and Kan, 2025](https://arxiv.org/html/2610.22441#bib.bib13)\)\. The above provide strong modeling and planning capabilities, but they typically assume that temporal logic specifications are manually given\. Our work is complementary: it focuses on converting natural language objectives into executable scenario tasks and STL specifications, enabling feasible control synthesis\.

LLMs for generating plans and temporal logic specifications\.Much existing work has used large language models \(LLMs\) to convert natural language instructions into plans or high\-level action sequences\([Huang et al\., 2022](https://arxiv.org/html/2610.22441#bib.bib14);[Ichter et al\., 2023](https://arxiv.org/html/2610.22441#bib.bib15);[Kannan et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib2);[Lin et al\., 2023](https://arxiv.org/html/2610.22441#bib.bib16)\)\. For example, SMART\-LLM\([Kannan et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib2)\)explored the use of LLMs in performing task decomposition and allocation for multi\-robot tasks\. Its final output is executable code\. Other approaches tend to leverage LLMs to generate structured representations at the first stage\. NL2HLTL2PLAN\([Xu et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib3)\)used LLMs to translate natural language instructions into a hierarchical task tree to capture logical relations\. SELP\([Wu et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib4)\)developed a method that uses LLMs to generate LTL specifications from natural language, selects the candidate, and then uses LLMs to produce a plan that conforms to it\. AutoTAMP\([Chen et al\., 2024a](https://arxiv.org/html/2610.22441#bib.bib5)\)generates STLs that describe objectives, using LLMs as translators and checkers\.

Beyond planning, DeepSTL\([He et al\., 2022](https://arxiv.org/html/2610.22441#bib.bib17)\), NL2TL\([Chen et al\., 2023](https://arxiv.org/html/2610.22441#bib.bib18)\), KGST\([Fang et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib19)\), LTLCodeGen\([Rabiei et al\., 2025](https://arxiv.org/html/2610.22441#bib.bib20)\), and so on studied natural language to temporal logic translation\. These works focus on generating temporal logic\. Our framework differs by jointly generating a hierarchical scenario task, task\-level and control\-level STL from LLMs, and finally synthesizing feasible control for multi\-component CPSs\.

LLMs for multi\-agent planning and coordination\.Recent work also explores LLMs as coordinators for multi\-agent systems\. RoCo\([Mandi et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib21)\)proposed a multi\-robot collaboration method\. Robots are equipped with LLMs to discuss and collectively reason about strategies and also get feedback from the environment\. LLM\-MARS\([Lykov et al\., 2023](https://arxiv.org/html/2610.22441#bib.bib22)\)enables dialogues between humans and robots, allowing them to generate behavior based on operator commands\. Chen et al\.\([Chen et al\., 2024b](https://arxiv.org/html/2610.22441#bib.bib23)\)compare centralized, decentralized, and hybrid LLM\-based communication architectures for multi\-robot collaboration in terms of task success and token efficiency\. These studies show the potential of LLMs for communication and coordination among agents and robots, but they are not primarily designed to produce constraints and specifications that agents should conform to\.

Feedback guided LLM planning and repair\.Prompting enables LLMs to perform new tasks from natural language instructions, examples, and contextual information\([Brown et al\., 2020](https://arxiv.org/html/2610.22441#bib.bib24)\)\. Besides, re\-prompting LLMs with additional context from the environment, execution, or validation feedback has been shown to improve task planning\([Huang et al\., 2023](https://arxiv.org/html/2610.22441#bib.bib25);[Guan et al\., 2023](https://arxiv.org/html/2610.22441#bib.bib26)\)\. Raman et al\.\([Raman et al\., 2022](https://arxiv.org/html/2610.22441#bib.bib27)\)used re\-prompting with precondition errors from failed actions to obtain more executable plans\. Silver et al\.\([Silver et al\., 2024](https://arxiv.org/html/2610.22441#bib.bib28)\)re\-prompt LLMs with feedback to repair Python programs synthesized as generalized planners\. Skreta et al\.\([Skreta et al\., 2023](https://arxiv.org/html/2610.22441#bib.bib29)\)use iterative prompting to incorporate verifier\-reported errors into subsequent prompts, improving the validity of generated task programs\. AutoTAMP\([Chen et al\., 2024a](https://arxiv.org/html/2610.22441#bib.bib5)\)uses syntax checking and planner\-generated state sequences to correct STL translations\. Our framework uses control synthesis diagnostics to guide revisions of the task plan itself\. We extend the underlying tool to identify violated constraints, conflicting component assignments, and failures involving component guards or invariants, together with the associated tasks\. This feedback allows the LLM to reconsider task decomposition and component allocation in response to failures arising from component dynamics and interactions\.

## 7\.Conclusion

This paper presents a hierarchical feedback framework for generating executable plans for multi\-component CPSs from natural language missions\. A consistency checking algorithm detects contradictions between LLM\-generated task plans and STL specifications before control synthesis\. When synthesis fails, diagnostic information guides revisions to task decomposition and allocation\. Experimental results demonstrate that early consistency checking and execution\-guided replanning complement each other in improving execution success, and that informative diagnostics make replanning more effective\.

## References

- Annpureddyet al\.\(2011\)Y\. Annpureddy, C\. Liu, G\. Fainekos, and S\. SankaranarayananS\-taliro: a tool for temporal logic falsification for hybrid systems\.InTools and Algorithms for the Construction and Analysis of Systems,P\. A\. Abdulla and K\. R\. M\. Leino \(Eds\.\),Berlin, Heidelberg,pp\. 254–257\.Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p1.1)\.
- Brownet al\.\(2020\)T\. B\. Brown, B\. Mann, N\. Ryder, M\. Subbiah, J\. Kaplan, P\. Dhariwal, A\. Neelakantan, P\. Shyam, G\. Sastry, A\. Askell, S\. Agarwal, A\. Herbert\-Voss, G\. Krueger, T\. Henighan, R\. Child, A\. Ramesh, D\. M\. Ziegler, J\. Wu, C\. Winter, C\. Hesse, M\. Chen, E\. Sigler, M\. Litwin, S\. Gray, B\. Chess, J\. Clark, C\. Berner, S\. McCandlish, A\. Radford, I\. Sutskever, and D\. AmodeiLanguage models are few\-shot learners\.InProceedings of the 34th International Conference on Neural Information Processing Systems,NIPS ’20,Red Hook, NY, USA\.External Links:ISBN 9781713829546Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p6.1)\.
- Chenet al\.\(2024a\)Y\. Chen, J\. Arkin, C\. Dawson, Y\. Zhang, N\. Roy, and C\. FanAutoTAMP: autoregressive task and motion planning with llms as translators and checkers\.In2024 IEEE International Conference on Robotics and Automation \(ICRA\),pp\. 6695–6702\.External Links:[Document](https://dx.doi.org/10.1109/ICRA57147.2024.10611163)Cited by:[§1](https://arxiv.org/html/2610.22441#S1.p2.1),[§6](https://arxiv.org/html/2610.22441#S6.p3.1),[§6](https://arxiv.org/html/2610.22441#S6.p6.1)\.
- Chenet al\.\(2024b\)Y\. Chen, J\. Arkin, Y\. Zhang, N\. Roy, and C\. FanScalable multi\-robot collaboration with large language models: centralized or decentralized systems?\.In2024 IEEE International Conference on Robotics and Automation \(ICRA\),pp\. 4311–4317\.External Links:[Document](https://dx.doi.org/10.1109/ICRA57147.2024.10610676)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p5.1)\.
- Chenet al\.\(2023\)Y\. Chen, R\. Gandhi, Y\. Zhang, and C\. FanNL2TL: transforming natural languages to temporal logics using large language models\.InProceedings of the 2023 Conference on Empirical Methods in Natural Language Processing,H\. Bouamor, J\. Pino, and K\. Bali \(Eds\.\),Singapore,pp\. 15880–15903\.External Links:[Document](https://dx.doi.org/10.18653/v1/2023.emnlp-main.985)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p4.1)\.
- Chen and Kan \(2025\)Z\. Chen and Z\. KanReal\-time reactive task allocation and planning of large heterogeneous multi\-robot systems with temporal logic specifications\.Int\. J\. Rob\. Res\.44\(4\),pp\. 640–664\.External Links:[Document](https://dx.doi.org/10.1177/02783649241278372)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p2.1)\.
- DeepSeek\-AI \(2026\)DeepSeek\-AIDeepSeek\-V4: towards highly efficient million\-token context intelligence\.Note:arXiv preprint arXiv:2606\.19348Cited by:[§5\.1](https://arxiv.org/html/2610.22441#S5.SS1.p1.1)\.
- Fanget al\.\(2025\)Y\. Fang, Z\. Jin, J\. An, H\. Chen, X\. Chen, and N\. ZhanEnhancing transformation from natural language to signal temporal logic using LLMs with diverse external knowledge\.InFindings of the Association for Computational Linguistics: ACL 2025,W\. Che, J\. Nabende, E\. Shutova, and M\. T\. Pilehvar \(Eds\.\),Vienna, Austria,pp\. 10446–10458\.External Links:[Document](https://dx.doi.org/10.18653/v1/2025.findings-acl.544)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p4.1)\.
- Guanet al\.\(2023\)L\. Guan, K\. Valmeekam, S\. Sreedharan, and S\. KambhampatiLeveraging pre\-trained large language models to construct and utilize world models for model\-based task planning\.InProceedings of the 37th International Conference on Neural Information Processing Systems,NIPS ’23,Red Hook, NY, USA\.Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p6.1)\.
- Heet al\.\(2022\)J\. He, E\. Bartocci, D\. Ničković, H\. Isakovic, and R\. GrosuDeepSTL: from english requirements to signal temporal logic\.InProceedings of the 44th International Conference on Software Engineering,ICSE ’22,New York, NY, USA,pp\. 610–622\.External Links:ISBN 9781450392211,[Document](https://dx.doi.org/10.1145/3510003.3510171)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p4.1)\.
- Henzinger \(1996\)T\.A\. HenzingerThe theory of hybrid automata\.InProceedings 11th Annual IEEE Symposium on Logic in Computer Science,Vol\.,pp\. 278–292\.External Links:[Document](https://dx.doi.org/10.1109/LICS.1996.561342)Cited by:[Definition 2\.1](https://arxiv.org/html/2610.22441#S2.Thmtheorem1.p1.1.1)\.
- Huanget al\.\(2022\)W\. Huang, P\. Abbeel, D\. Pathak, and I\. MordatchLanguage models as zero\-shot planners: extracting actionable knowledge for embodied agents\.InProceedings of the 39th International Conference on Machine Learning,K\. Chaudhuri, S\. Jegelka, L\. Song, C\. Szepesvari, G\. Niu, and S\. Sabato \(Eds\.\),Proceedings of Machine Learning Research, Vol\.162,pp\. 9118–9147\.Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p3.1)\.
- Huanget al\.\(2023\)W\. Huang, F\. Xia, T\. Xiao, H\. Chan, J\. Liang, P\. Florence, A\. Zeng, J\. Tompson, I\. Mordatch, Y\. Chebotar, P\. Sermanet, T\. Jackson, N\. Brown, L\. Luu, S\. Levine, K\. Hausman, and b\. ichterInner monologue: embodied reasoning through planning with language models\.InProceedings of The 6th Conference on Robot Learning,K\. Liu, D\. Kulic, and J\. Ichnowski \(Eds\.\),Proceedings of Machine Learning Research, Vol\.205,pp\. 1769–1782\.Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p6.1)\.
- Ichteret al\.\(2023\)B\. Ichter, A\. Brohan, Y\. Chebotar, C\. Finn, Hausman,et al\.Do as i can, not as i say: grounding language in robotic affordances\.InProceedings of The 6th Conference on Robot Learning,K\. Liu, D\. Kulic, and J\. Ichnowski \(Eds\.\),Proceedings of Machine Learning Research, Vol\.205,pp\. 287–318\.Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p3.1)\.
- Kannanet al\.\(2024\)S\. S\. Kannan, V\. L\. N\. Venkatesh, and B\. MinSMART\-llm: smart multi\-agent robot task planning using large language models\.In2024 IEEE/RSJ International Conference on Intelligent Robots and Systems \(IROS\),pp\. 12140–12147\.External Links:[Document](https://dx.doi.org/10.1109/IROS58592.2024.10802322)Cited by:[§1](https://arxiv.org/html/2610.22441#S1.p2.1),[§5\.1](https://arxiv.org/html/2610.22441#S5.SS1.p5.1),[§5\.4](https://arxiv.org/html/2610.22441#S5.SS4.p1.1),[§6](https://arxiv.org/html/2610.22441#S6.p3.1)\.
- Kolveet al\.\(2022\)E\. Kolve, R\. Mottaghi, W\. Han, E\. VanderBilt, L\. Weihs, A\. Herrasti, M\. Deitke, K\. Ehsani, D\. Gordon, Y\. Zhu, A\. Kembhavi, A\. Gupta, and A\. FarhadiAI2\-thor: an interactive 3d environment for visual ai\.Note:arXiv preprint arXiv:1712\.05474Cited by:[§5\.1](https://arxiv.org/html/2610.22441#S5.SS1.p2.1)\.
- Liet al\.\(2026\)P\. Li, Z\. An, S\. Abrar, and L\. ZhouLarge language models for multi\-robot systems: a survey\.Autonomous Robots50\(3\),pp\. 30\.External Links:ISSN 1573\-7527,[Document](https://dx.doi.org/10.1007/s10514-026-10257-4)Cited by:[§1](https://arxiv.org/html/2610.22441#S1.p2.1)\.
- Linet al\.\(2023\)K\. Lin, C\. Agia, T\. Migimatsu, M\. Pavone, and J\. BohgText2Motion: from natural language instructions to feasible plans\.Autonomous Robots47\(8\),pp\. 1345–1365\.External Links:[Document](https://dx.doi.org/10.1007/s10514-023-10131-7)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p3.1)\.
- Luo and Liu \(2025\)X\. Luo and C\. LiuSimultaneous task allocation and planning for multirobots under hierarchical temporal logic specifications\.IEEE Transactions on Robotics41,pp\. 5040–5059\.External Links:[Document](https://dx.doi.org/10.1109/TRO.2025.3598139)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p2.1)\.
- Lykovet al\.\(2023\)A\. Lykov, M\. Dronova, N\. Naglov, M\. Litvinov, S\. Satsevich, A\. Bazhenov, V\. Berman, A\. Shcherbak, and D\. TsetserukouLLM\-mars: large language model for behavior tree generation and nlp\-enhanced dialogue in multi\-agent robot systems\.Note:arXiv preprint arXiv:2312\.09348Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p5.1)\.
- Maler and Nickovic \(2004\)O\. Maler and D\. NickovicMonitoring temporal properties of continuous signals\.InFormal Techniques, Modelling and Analysis of Timed and Fault\-Tolerant Systems,Y\. Lakhnech and S\. Yovine \(Eds\.\),Berlin, Heidelberg,pp\. 152–166\.Cited by:[Definition 2\.4](https://arxiv.org/html/2610.22441#S2.Thmtheorem4.p1.1.1)\.
- Mandiet al\.\(2024\)Z\. Mandi, S\. Jain, and S\. SongRoCo: dialectic multi\-robot collaboration with large language models\.In2024 IEEE International Conference on Robotics and Automation \(ICRA\),pp\. 286–299\.External Links:[Document](https://dx.doi.org/10.1109/ICRA57147.2024.10610855)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p5.1)\.
- Rabieiet al\.\(2025\)B\. Rabiei, M\. K\. A\. R\., Z\. Dai, S\. L\. S\. R\. Pilla, Q\. Dong, and N\. AtanasovLTLCodeGen: code generation of syntactically correct temporal logic for robot task planning\.Note:arXiv preprint arXiv:2503\.07902Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p4.1)\.
- Ramanet al\.\(2022\)S\. S\. Raman, V\. Cohen, E\. Rosen, I\. Idrees, D\. Paulius, and S\. TellexPlanning with large language models via corrective re\-prompting\.External Links:[Link](http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=127989)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p6.1)\.
- Silveret al\.\(2024\)T\. Silver, S\. Dan, K\. Srinivas, J\. B\. Tenenbaum, L\. Kaelbling, and M\. KatzGeneralized planning in pddl domains with pretrained large language models\.InProceedings of the Thirty\-Eighth AAAI Conference on Artificial Intelligence and Thirty\-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence,AAAI’24/IAAI’24/EAAI’24\.External Links:ISBN 978\-1\-57735\-887\-9,[Document](https://dx.doi.org/10.1609/aaai.v38i18.30006)Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p6.1)\.
- Skretaet al\.\(2023\)M\. Skreta, N\. Yoshikawa, S\. Arellano\-Rubach, Z\. Ji, L\. B\. Kristensen, K\. Darvish, A\. Aspuru\-Guzik, F\. Shkurti, and A\. GargErrors are useful prompts: instruction guided task programming with verifier\-assisted iterative prompting\.Note:arXiv preprint arXiv:2303\.14100Cited by:[§6](https://arxiv.org/html/2610.22441#S6.p6.1)\.
- Wanget al\.\(2024\)J\. Wang, W\. Liu, M\. Zhang, J\. Wei, Y\. Shi, L\. Bu, and X\. LiScenario\-based flexible modeling and scalable falsification for reconfigurable cpss\.InComputer Aided Verification,A\. Gurfinkel and V\. Ganesh \(Eds\.\),Cham\.Cited by:[§2\.1](https://arxiv.org/html/2610.22441#S2.SS1.p2.1),[§4\.3](https://arxiv.org/html/2610.22441#S4.SS3.p2.1),[§5\.1](https://arxiv.org/html/2610.22441#S5.SS1.p1.1),[§6](https://arxiv.org/html/2610.22441#S6.p1.1)\.
- Wuet al\.\(2025\)Y\. Wu, Z\. Xiong, Y\. Hu, S\. S\. Iyengar, N\. Jiang, A\. Bera, L\. Tan, and S\. JagannathanSELP: generating safe and efficient task plans for robot agents with large language models\.In2025 IEEE International Conference on Robotics and Automation \(ICRA\),pp\. 2599–2605\.External Links:[Document](https://dx.doi.org/10.1109/ICRA55743.2025.11128420)Cited by:[§1](https://arxiv.org/html/2610.22441#S1.p2.1),[Table 1](https://arxiv.org/html/2610.22441#S5.T1.4.4.3.1.1),[§6](https://arxiv.org/html/2610.22441#S6.p3.1)\.
- Xuet al\.\(2025\)S\. Xu, X\. Luo, Y\. Huang, L\. Leng, R\. Liu, and C\. LiuNl2Hltl2Plan: scaling up natural language understanding for multi\-robots through hierarchical temporal logic task specifications\.IEEE Robotics and Automation Letters10\(10\),pp\. 10482–10489\.External Links:[Document](https://dx.doi.org/10.1109/LRA.2025.3598648)Cited by:[§1](https://arxiv.org/html/2610.22441#S1.p2.1),[§5\.1](https://arxiv.org/html/2610.22441#S5.SS1.p5.1),[§5\.4](https://arxiv.org/html/2610.22441#S5.SS4.p1.1),[§6](https://arxiv.org/html/2610.22441#S6.p3.1)\.