ViTL: Temporal Logic-Guided Zero-Shot Natural Language Navigation via Vision-Language Models
January 01, 1970
Enabling robots to follow natural language commands to complete zero-shot long-horizon tasks remains challenging. It requires extracting implicit temporal and logical constraints from natural language commands and executing multiple sub-tasks accordingly. Recent zero-shot object navigation methods use vision-language models (VLMs) to guide frontier-based exploration in unknown environments, but they are limited to single-target tasks. Real-world commands such as “Clean either the chair or the couch, then turn on the tv.” require navigating to multiple targets in a temporally constrained order, which no existing zero-shot system can handle. We present ViTL, a framework that addresses this gap at two levels. At the task level, we use a large language model (LLM) to compile natural language commands into Linear Temporal Logic (LTL) formulas, which are then converted into Deterministic Finite Automata (DFA) that coordinate multi-channel value maps and trigger dynamic replanning when new objects are detected. At the navigation level, we introduce directional score: rather than producing a direction-agnostic value across the entire field of view, we label frontier directions on the observation image and extract per-direction scores from the VLM. Experiments on Habitat-Matterport 3D (HM3D) show that the full framework enables zero-shot long-horizon completion of natural language navigation tasks with temporal constraints, and that directional score improves single-target navigation accuracy and efficiency over the baseline.
Object-goal navigation (ObjectNav), the task of navigating to an object specified by its semantic category in an unknown environment, is a fundamental capability for autonomous mobile robots [1], [2]. Recent zero-shot approaches have made remarkable progress by leveraging pre-trained vision-language models (VLMs) to guide exploration without task-specific training [3]–[6].
However, current zero-shot ObjectNav methods are limited to single-target navigation. Real-world robot deployments demand capabilities beyond them. For instance, consider a household service robot that receives a natural language command: “Clean either the chair or the couch, then turn on the tv.”. Such tasks require navigating to multiple targets in a temporally constrained order. To the best of the authors’ knowledge, no existing zero-shot navigation system can handle this problem.
Solving this problem requires addressing two interleaved challenges. At the task level, the system needs a high-level planner that continuously incorporates environment observations, identifies the efficient completion path, and dynamically selects the current sub-task. At the navigation level, each sub-task demands accurate and efficient zero-shot single-target navigation executor.
We present ViTL (Vision-Language Temporal Logic Navigation), a zero-shot navigation framework that addresses both levels. At the task level, we leverage prior work on natural language to temporal logic translation [7]–[9] to compile natural language commands into Linear Temporal Logic (LTL) formulas using a large language model (LLM). For instance, the household task above can be expressed as \(\varphi = \Diamond((\textit{chair} \lor \textit{couch}) \land \Diamond\, \textit{tv})\), where \(\Diamond\) denotes the eventually operator. The LTL formula is then converted into a Deterministic Finite Automaton (DFA) [10], whose graph structure enables principled sub-task decomposition. The DFA selects the current navigation target through dynamic edge weights that decrease when a target object is detected, enabling the system to opportunistically reorder sub-tasks in real time to reduce the overall travel distance. To support this, the system maintains multi-channel value maps, one per target category, that accumulate spatial knowledge in parallel so that no exploration effort is lost when the planner switches targets. At the navigation level, we introduce directional score. Rather than computing a single direction-agnostic score from the full RGB observation, we visually label frontier directions on the observation image and query the VLM to score each direction independently. These per-direction scores are temporally fused using scene-weighted averaging and spatially smoothed through angle-based interpolation to produce dense value maps.
Our contributions are as follows.
We propose ViTL, a zero-shot framework that enables robots to execute long-horizon natural language navigation tasks with complex temporal constraints.
We introduce a novel directional score method that leverages vision-language models to generate spatially-varying navigation value maps, improving single-target zero-shot navigation accuracy.
We conduct comprehensive experiments to evaluate ViTL’s capability for complex natural language navigation tasks.
ObjectNav requires a robot to find an instance of a target object category in an unseen environment. Learned approaches train task-specific policies via reinforcement learning [1] or semantic map prediction [2], but are restricted to closed-set categories and simulated data. Zero-shot methods avoid task-specific training by leveraging foundation models. CoW [3] explores the nearest frontier until an open-vocabulary detector finds the target. ESC [11] and L3MVN [4] use large language models to evaluate frontiers based on nearby object detections converted to text. VLFM [5] instead queries a vision-language model directly on the RGB observation to produce a cosine-similarity score, which is assigned uniformly across the field of view to build a value map. More recent methods enrich spatial reasoning through learned environment predictions [12], geometric cues [13], and scene-graph representations [6]. All of these methods are designed for single-target navigation and cannot handle complex temporal dependencies.
Executing multi-step tasks from natural language requires both high-level planning and low-level navigation. InstructNav [14] re-queries an LLM at every decision step for complex navigation tasks. However, it does not model temporal constraints between sub-tasks and provides no formal guarantees on task completion. NavGPT-2 [15] aligns vision-language model features with a graph-based navigation policy for navigation tasks, but requires task-specific fine-tuning and does not operate in a zero-shot setting. SayPlan [16] grounds LLM plans in robot affordances or scene graphs for long-horizon manipulation, but assumes known environments and does not address the navigation problem in unexplored spaces. Our approach instead uses a single offline LLM call to compile the task into an LTL formula, which is then executed by a DFA that provides provable temporal constraint satisfaction and supports dynamic replanning upon new object detections.
Translating natural language commands into formal temporal logic specifications is an active research area [17]–[19]. Lang2LTL [7] fine-tunes language models to convert grounded natural language into LTL formulas for robot task planning. LTLCodeGen [8] leverages code-generation LLMs to produce syntactically correct LTL from natural language.
Once an LTL formula is obtained, recent works use temporal logic to guide robot execution. SELP [20] constructs a Büchi automaton to constrain LLM plan generation through token masking in known environments where all landmark locations are given; the automaton acts as an offline verifier and the robot executes the resulting plan without replanning. NL2HLTL2PLAN [18] extends NL-to-LTL translation to hierarchical specifications for multi-robot allocation, but similarly assumes known workspaces. In [21], the authors address LTL planning under semantic uncertainty using a product automaton with value iteration over discrete grids, updating beliefs as labels are revealed. While related in handling unknown environments, their method operates on small discrete state spaces with probabilistic label priors rather than continuous visual observations. In contrast, our work targets zero-shot navigation in completely unknown continuous environments with no prior map. The compiled automaton serves as an online reactive controller that dynamically selects navigation targets as the robot discovers objects through visual perception, combined with VLM-based scoring to guide frontier exploration.
Enabling robots to follow natural language commands to complete zero-shot long-horizon tasks in real-world environments remains challenging, as it requires extracting implicit temporal and logical constraints from natural language commands and executing multiple sub-tasks accordingly.
For example, a household service robot may receive a command such as: “Clean the chair or the couch, then turn on the tv.” Such a command defines a set of target object categories \(\mathcal{C} = \{c_1, c_2, \ldots, c_n\}\) together with temporal constraints over them, such as sequencing (chair or couch before tv) and disjunction (chair or couch). We focus on the navigation component, assuming each sub-task is completed once the robot reaches the corresponding object, therefore, we reduce all action verbs (e.g., clean, turn on) to reach objects.
We consider a zero-shot setting where no prior map is available. At each timestep \(t\), the robot receives an egocentric observation \(o_t = (I_t, D_t, \xi_t)\) consisting of an RGB image \(I_t\), a depth image \(D_t\), and the agent pose \(\xi_t\), and must output an action \(a_t \in \{\texttt{move\_forward}, \texttt{turn\_left}, \texttt{turn\_right}, \texttt{stop}\}\) to progressively complete the task.
Problem 1. Given a natural-language command specifying target object categories with temporal constraints, and without access to prior information of the environment, the robot must determine a sequence of actions based on observations \(o_t\) to reach all required targets while satisfying the temporal constraints specified by the command.
We propose ViTL, a zero-shot navigation framework illustrated in Fig. 1. Our approach is grounded in one observation: long-horizon commands require completing sub-tasks in an order that respects the embedded temporal constraints. In a zero-shot setting with no prior map, the system cannot fix this ordering in advance; it needs a task-level planner that incorporates new observations, selects the optimal sub-task online, and never violates the constraints while minimizing travel distance.
We observe that this problem maps naturally to graph search over a DFA compiled from LTL, where each path through the graph corresponds to a valid execution ordering and shortest-path search yields the optimal sub-task (Sec. 4.1). Each selected sub-task is then executed by a navigation-level executor that performs frontier-based exploration using directional score and smooth value maps (Sec. 4.2). When the task-level planner determines the current sub-task, the navigation level executes it using the corresponding value map channel.
The task-level planner receives continuously updated environment knowledge, the set of detected objects \(\mathcal{D}\), reached objects \(\mathcal{R}\), and failed objects \(\mathcal{B}\), and outputs the current optimal target \(c_k\). It operates in two stages: compiling the natural language command into a formal specification (Sec. 4.1.1), and using graph search over the resulting automaton to dynamically select and update the active target as the environment state evolves (Sec. 4.1.2).
Background: LTL and DFA. We use Linear Temporal Logic [10] to formally represent temporal constraints. An LTL formula over atomic propositions \(\Pi\) is defined recursively as: \[\phi ::= \pi \mid \lnot \pi \mid \phi_1 \lor \phi_2 \mid \phi_1 \land \phi_2 \mid \bigcirc\phi \mid \phi_1 \;\mathcal{U}\;\phi_2 \mid \Diamond\phi,\] where \(\pi \in \Pi\) is an atomic proposition, \(\lnot\), \(\land\), \(\lor\) are Boolean operators, and \(\bigcirc\) (next), \(\;\mathcal{U}\;\) (until), \(\Diamond\) (eventually) are temporal operators. LTL formula can be compiled into a deterministic finite automaton (DFA) \(\mathcal{A} = (S, \Sigma, \delta, s_0, F)\) using standard tools [22], where acceptance of a finite word certifies satisfaction of the formula. In our setting, each \(\pi \in \Pi\) corresponds to a target object category, and DFA transitions are triggered when the robot reaches the associated object.
Task compilation. To compile natural language commands into formal specifications, we prompt an LLM to extract the target categories \(\mathcal{C}\) and temporal constraints, producing an LTL formula \(\varphi\) over \(\mathcal{C}\), following established NL-to-LTL translation approaches [7]. This single offline LLM call replaces the repeated runtime queries required by LLM-based planners [14], reducing both latency and the risk of cumulative reasoning errors. The resulting formula is then compiled into a deterministic finite automaton using standard tools [22], which serves as an online reactive controller throughout the mission. Consider the running example: after reducing all action verbs to reach, the command becomes “Reach either a chair or a couch, then reach a tv.” The LLM identifies \(\mathcal{C} = \{\textit{chair}, \textit{couch}, \textit{tv}\}\) and produces: \[\varphi = \Diamond((\textit{chair} \lor \textit{couch}) \land \Diamond\,\textit{tv}) \label{eq:ltl95example}\tag{1}\] The disjunction encodes a choice: the robot may reach either object to satisfy the first sub-task while the nested \(\Diamond\) enforces sequencing: the tv must be reached afterward. The LTL can be compiled to DFA (Fig. 2) which has two equally short paths from \(s_0\): one via chair and one via couch, both leading to \(s_1\), from which reaching tv leads to the accepting state \(s_f\). This graph structure encodes all valid execution orderings, with branching representing choices and path length reflecting the number of remaining sub-tasks.
The compiled DFA \(\mathcal{A}\) drives target selection throughout the mission. The planner maintains three sets that summarize the robot’s evolving knowledge of the environment: detected objects \(\mathcal{D}\) (observed but not yet reached), reached objects \(\mathcal{R}\), and failed objects \(\mathcal{B}\) (targets the navigator failed to reach). The DFA state \(s\) advances only when the robot reaches a target (\(s \leftarrow \delta(s, c_k)\)). In case of update \(\mathcal{B}\) or \(\mathcal{R}\), the planner recomputes the shortest weighted path over the DFA to select the next target. Each edge \(e\) in the DFA corresponds to reaching a specific target object \(c_e\), and is assigned a weight \(w(e)\) based on the robot’s current knowledge:
\[w(e) = \begin{cases} w_{\text{det}} & \text{if } c_e \in \mathcal{D} \\ w_{\text{fail}} & \text{if } c_e \in \mathcal{B} \\ 1.0 & \text{otherwise} \end{cases} \label{eq:edge95weight}\tag{2}\] where \(w_{\text{det}} \ll 1\) reflects that navigating to a detected target at a known location requires far less effort than exploring for an undetected one, and \(w_{\text{fail}} \gg 1\) discourages revisiting targets that the navigator previously failed to reach. The planner then finds the shortest weighted path \(\rho^*\) through the graph search from the current state \(s_{\text{curr}}\) to the accepting state \(s_f\): \[\rho^* = \mathop{\mathrm{arg\,min}}_{\rho:\, s_{\text{curr}} \rightsquigarrow s_f} \sum_{e \in \rho} w(e) \label{eq:dijkstra}\tag{3}\] and the next navigation target \(c_k\) is the label on the first edge of \(\rho^*\). Infeasibility is detected in two cases. First, if the compiled DFA has no path from \(s_0\) to an accepting state, the command is contradictory and is rejected before execution. Second, during execution, if \(\sum_{e \in \rho^*} w(e) \geq w_{\text{fail}}\), every remaining path must traverse a failed target, and the task is declared infeasible. Note that constraints are enforced over reached targets only; passing through a region without stopping does not trigger a transition, so merely traversing an area en route does not violate the specification. Replanning is triggered whenever \(\mathcal{D}\), \(\mathcal{R}\), or \(\mathcal{B}\) changes: edge weights are recomputed and the shortest path is updated. For instance, if the robot is exploring for chair (not yet detected) and the detector spots a couch, then couch enters \(\mathcal{D}\) while chair has not: the edge \(s_0 \xrightarrow{\textit{couch}} s_1\) receives weight \(w_{\text{det}}\) while the chair edge retains weight \(1.0\), making the couch path cheaper and triggering an immediate target switch.
Multi-channel value maps. To support multi-target execution, the system maintains a separate value map channel for each target category from the natural language command: \[\mathcal{M} = \{\mathbf{V}^{(j)}\}_{j=1}^{n}\] where \(\mathbf{V}^{(j)}\) is the value map for target \(c_j\), recording per-pixel navigation scores. All channels are updated in parallel at every timestep using the procedure described in Sec. 4.2. When the planner selects target \(c_k\), it activates the corresponding channel \(\mathbf{V}^{(k)}\) for the navigation-level executor, which uses it to rank frontiers and guide exploration. When the planner changes targets, the new channel already encodes spatial knowledge from prior exploration, reducing redundant re-exploration.
Algorithm 3 summarizes the procedure. The main loop alternates between detection-triggered replanning (lines 4–10), value map updates and agent navigation to the target (lines 11–20). If the current target has been detected, the agent navigates directly to its stored location \(\ell(c_k)\); otherwise, it explores via the active value map channel. Upon reaching a target, the DFA state advances and a new target is selected; upon failure, the target is added to the failed set, edge weights are updated, and the planner replans.
Given a target \(c_k\) and its corresponding value map channel \(\mathbf{V}^{(k)}\) selected by the task-level planner, the navigation-level executor guides the robot toward it through frontier-based exploration. We use a top-down occupancy map from depth observations and odometry, following [5]. Each boundary between explored and unexplored regions yields one frontier \(f_i\), taken as its midpoint, a single 2D waypoint (Fig. 1, Occupancy Map).
Existing value-map approaches compute a single direction-agnostic score from the full RGB observation, discarding spatial information about which region within the field of view is most relevant. We instead introduce directional score: the VLM evaluates individual frontier directions, producing spatially-varying value maps that more accurately capture which regions are promising for reaching \(c_k\). Note that single-target ObjectNav is the special case where \(\varphi = \Diamond\, c_1\), reducing to one value map channel with no task-level coordination. The following subsections detail how directional scores are computed (Sec. 4.2.1) and how the value maps are constructed(Sec. 4.2.2).
Frontiers extracted from the occupancy map are projected into the current RGB frame based on the agent’s pose. Each projected frontier \(f_i\) is assigned a letter label \(L_i \in \{A, B, C, \ldots\}\) and visually annotated on the image (Fig. 1, Frontier Perception). An additional option \(L_{N_f+1}\) represents “explore elsewhere,” serving as a calibration anchor that allows the VLM to distribute probability mass away from visible frontiers when none is promising.
We construct a multiple-choice prompt for the VLM:
“Among directions (\(A\), \(B\), \(C\) ), or explore elsewhere (\(D\)), which should I choose to find a {target}? Answer with ONLY a single letter.”
The directional probability distribution is computed via softmax over the next-token logits for each option letter: \[P(f_i \mid I_t, c_k) = \frac{\exp(z_{L_i})}{\sum_{j=1}^{N_f+1} \exp(z_{L_j})} \label{eq:frontier95softmax}\tag{4}\] where \(z_{L_i}\) is the logit of the token corresponding to letter \(L_i\). This yields a probability for each frontier, providing both a ranking and a confidence measure.
We query the VLM for an overall scene relevance score:
“Does this view show paths or doorways that could lead to a {target}? Answer Yes or No.”
\[S_{curr} = P(\text{Yes} \mid I_t, c_k) = \frac{\exp(z_{\text{Yes}})}{\exp(z_{\text{Yes}}) + \exp(z_{\text{No}})} \label{eq:scene95score}\tag{5}\] Each frontier’s value blends the scene-level and direction-level signals:
\[V_{\text{curr}}(f_i) = S_{curr} \times P(f_i \mid I_t, c_k) \label{eq:v95curr}\tag{6}\]
Figure 4: Smooth value map generation. Discrete frontier scores (left) are converted into a smooth gradient within the FOV cone (right) via angle-based interpolation and temporally fused with prior observations.. a — Observation with frontier directions labeled \(A\), \(B\)., b — FOV cone projection and spatially smooth.
Given the per-frontier scores from Eq. 6 , we construct a 2D value map \(\mathbf{V}\) that records a navigation score at every explored pixel. At each timestep, frontier scores are first temporally fused with historical observations at their respective map locations, then spatially interpolated across the Field-of-View (FOV) cone to yield a dense, smoothly varying gradient as shown in Fig. 4.
Temporal fusion. We maintain a scene score map \(\mathbf{S}\), a 2D grid aligned with the value map, where each pixel stores the scene score \(S_{curr}\) from when it was last observed. Each frontier \(f_i\) occupies a specific pixel, at which we look up the stored value \(\mathbf{V}_{\text{old}}(f_i)\) and scene score \(\mathbf{S}_{\text{old}}(f_i)\). If the pixel has never been observed (\(\mathbf{S}_{\text{old}}(f_i) = 0\)), the fused value is the current score: \(\tilde{V}(f_i) = V_{\text{curr}}(f_i)\). Otherwise, the old and new values are combined using scene-weighted averaging: \[\tilde{V}(f_i) = \frac{\mathbf{V}_{\text{old}}(f_i) + V_{\text{curr}}(f_i)}{\mathbf{S}_{\text{old}}(f_i) + S_{curr}} \cdot S_{curr} \label{eq:temporal95fusion}\tag{7}\] Because both terms are weighted by their respective scene scores, observations from more informative viewpoints (higher \(S_{curr}\)) naturally contribute more to the fused value.
Spatial smoothing. The fused frontier values \(\{\tilde{V}(f_i)\}\) are point estimates at discrete locations. To produce a dense value map across the FOV, we compute each frontier’s bearing angle \(\theta_i\) relative to the camera’s forward direction. Since each frontier \(f_i\) is a single midpoint, \(\theta_i\) is one scalar per frontier. We then insert virtual edge frontiers at the FOV boundaries \(\pm\theta_{\text{fov}}/2\) with baseline score \(V_{\text{edge}} = \beta \cdot S_{curr}\), where \(\beta\) is an edge attenuation factor. For each pixel \(p\) inside the FOV cone with bearing angle \(\theta_p\), let \(\theta_i'\) and \(\theta_{i+1}'\) be the two adjacent sorted angles such that \(\theta_i' \leq \theta_p \leq \theta_{i+1}'\). The smooth value is obtained by linear interpolation: \[V_{\text{smooth}}(p) = v_i' + \frac{\theta_p - \theta_i'}{\theta_{i+1}' - \theta_i'} (v_{i+1}' - v_i') \label{eq:interpolation}\tag{8}\] where \(\{\theta_i'\}\) and \(\{v_i'\}\) are the angles and fused scores in ascending angular order. The result is a smooth gradient across the FOV cone (Fig. 4b): high values concentrate near promising frontiers and decay toward the edges. The smoothed values are then written into \(\mathbf{V}\) for pixels within the current FOV, and the scene score map is updated accordingly.
Frontier selection. The agent selects the next waypoint from the value map: \[f^* = \mathop{\mathrm{arg\,max}}_{f_i} \; \max_{p \in \mathcal{N}(f_i, r)} \mathbf{V}^{(k)}(p) \label{eq:multi95frontier95selection}\tag{9}\] where \(\mathcal{N}(f_i, r)\) is the set of pixels within radius \(r\) of frontier \(f_i\). The selected frontier serves as a waypoint for a pre-trained depth-based PointNav policy, which converts the relative goal position into low-level robot actions.
This cycle of map update, frontier selection and navigation repeats continuously: at each timestep the occupancy map and all value map channels are updated with new observations, frontiers are extracted, and the highest-scoring frontier under \(\mathbf{V}^{(k)}\) is selected, and the agent navigates toward it, until the target object is detected, reached or failed.
We evaluate on the Habitat simulator [23] using the Habitat-Matterport 3D (HM3D) dataset [24]. The agent must navigate to an instance of a specified object category in an unseen environment using only egocentric RGB-D observations and pose
estimates. We use the HM3D ObjectNav v2 validation split, which contains 2000 episodes across 20 scenes with six target categories: {chair, bed, potted plant, toilet, tv monitor, couch}. Each episode
terminates after a maximum of \(T_{\max} = 500\) steps. The agent operates a discrete action space {\(\texttt{move\_forward}\) (0.25 m), \(\texttt{turn\_left}\) (30\(^\circ\)), \(\texttt{turn\_right}\) (30\(^\circ\)), \(\texttt{stop}\)}. An episode is considered successful if the agent calls stop within 1.0 m of the target, and fail if it reaches the maximum steps.
Evaluation Metrics. We report the two metrics: Success Rate (SR), the success rate of navigation episodes, and Success weighted by Path Length (SPL), measuring the success path efficiency if success SPL = \(\frac{\text{optimal path}}{\text{actual path length}}\), otherwise SPL = 0. The higher value means a more efficient path.
Implementation Details. We use LLaVA-NeXT-34B [25] as the vision-language model, loaded with 8-bit quantization. For object
detection, we employ YOLOv7-E6E [26]. Low-level point-goal navigation is handled by a pre-trained depth-based PointNav policy [5]. The DFA is compiled from LTL specifications using the lomap library [27].
We first evaluate ViTL’s capability in the navigation level, which is to solve the single-target ObjectNav problem. Table 1 compares ViTL’s Navigation-Level Executor against other zero-shot object navigation methods on the HM3D ObjectNav v2 validation split (2000 episodes). Our method achieves the success rate (54.1%) and SPL (30.9), demonstrating that directional score improves navigation reliability over other methods. ViTL achieves competitive results using LLaVA-NeXT-34B, an open-source model without fine-tuning, despite competing against methods that rely on significantly larger closed-source VLMs such as Gemini 1.5 Pro and GPT-4V.
| Method | SR (%) | SPL |
|---|---|---|
| WMNav Gemini 1.5 Flash [12] | 53.5 | 30.7 |
| WMNav Gemini 1.5 Pro [12] | 58.1 | 31.2 |
| GAMap [13] | 53.1 | 26.0 |
| SG-Nav-GPT [6] | 54.0 | 24.9 |
| VLFM [5] | 52.4 | 30.8 |
| InstructNav (GPT4 + GPT4V) [14] | 56.0 | 22.5 |
| InstructNav (GPT4 + LLaVA 34B) [14] | 50.0 | 19.4 |
| ViTL (LLaVA-34B) (ours) | 54.1 | 30.9 |
Figure 5: Task-level planning performance across observation probabilities \(p_{\text{obs}}\) on 2000 tasks. ViTL achieves higher task completion rate with fewer exploration attempts.. a — Task completion rate., b — Avg. exploration attempts.
We next evaluate ViTL’s task-level planner: given a natural language command and a stream of environment updates (\(\mathcal{D}\), \(\mathcal{R}\), \(\mathcal{B}\)), can the planner reliably select targets that satisfy temporal constraints while minimizing total travel cost? Since no existing zero-shot navigation system supports temporally constrained multi-target tasks, we compare against an LLM-based baseline (LLM-planner) on 2000 generated natural language navigation tasks.
Benchmark and evaluation protocol. We build a benchmark of 2000 natural language navigation tasks, each paired with a ground-truth LTL formula. Each formula is constructed from a lifted template: an abstract temporal structure with placeholder propositions that is grounded by sampling concrete objects from \(\mathcal{C}\). Templates range up to complex formulas with disjunctive branches and until constraints (up to 6 targets). For example, “Reach a bed, then a tv, then a couch; or reach a toilet, then a chair” yields \(\Diamond(\textit{bed} \land \Diamond(\textit{tv} \land \Diamond\,\textit{couch})) \lor \Diamond(\textit{toilet} \land \Diamond\,\textit{chair})\).
To enable efficient large-scale evaluation independent of low level navigation, we model the single-target executor probabilistically. If the planner selects a previously observed target, the robot reaches it directly. Otherwise, it explores: with probability \(p_{\text{obs}}\) it finds the intended target, and with probability \(1 - p_{\text{obs}}\) it encounters a different object, triggering replanning. Each exploration attempt corresponds to a full navigation episode, so the total number of attempts reflects overall travel cost in real world. We sweep \(p_{\text{obs}} \in \{0.1, 0.2, \ldots, 1.0\}\) to assess the planner: low values simulate cluttered environments where exploration frequently reveals unintended objects, while high values model simpler scenes.
Baseline. Since the task is specified in natural language, the most intuitive baseline is to use an LLM directly as a task-level planner. The LLM-planner does exactly this: at every decision point, it sends a prompt containing the natural language command and the current environment state (\(\mathcal{D}\), \(\mathcal{R}\), \(\mathcal{B}\)) to the LLM, which returns the next target to pursue. The LLM is re-queried whenever the environment state changes, and the process repeats until it outputs “Done”, indicating that the task is complete or infeasible. The prompt template is shown below.
ViTL also uses an LLM, but queries it only once to translate the natural language command into an LTL formula, which is then compiled into a DFA and used for graph-based target selection. To ensure a fair comparison, both methods share the same LLM (GPT-5.2), environment information, and navigation-level executor, so any difference in performance is attributable solely to the planner.
Role: You are a navigation planner. Determine the next target object for an agent to satisfy the task as fast as possible.
Task: {Task description in natural language}
Rules: Follow the temporal ordering implied by the task. Revisiting objects is allowed. Output exactly: TARGET: <object> or "DONE".
Current State:
\(\bullet\) Observed (known location, not yet reached): {...}
\(\bullet\) Reached (in order): [...]
\(\bullet\) Failed (unreachable): {...}
Results. Fig. 5 shows the results across \(p_{\text{obs}} \in \{0.1, 0.2, \ldots, 1.0\}\). ViTL reduces the problem of multi-step temporal reasoning to NL-to-LTL translation, which achieves 95.3% accuracy (1906/2000 correct formulas). Given a correct translation, the task-level planner in ViTL guarantees 100% task completion across all \(p_{\text{obs}}\) values, as task execution reduces to graph search. The figure reports end-to-end success rate, counting incorrect NL-to-LTL translations as failures; thus ViTL’s success rate is capped at the 95.3% translation accuracy. We note that fine-tuned compact models such as T5-base also achieve near-perfect translation accuracy [7], indicating that this step is not a bottleneck and can be performed reliably with modest computational resources.
In contrast, LLM-planner must perform temporal reasoning incrementally at every decision point, and achieves only 88.3% completion with GPT-5.2. Its \({\sim}11\%\) failure rate remains roughly constant across \(p_{\text{obs}}\), confirming that failures stem from reasoning errors, temporal constraint violations or premature termination. ViTL also consistently requires fewer exploration attempts (Fig. 5 (b)). We verify that this planning-level advantage translates into real navigation savings in the full system evaluation later.
Case studies. We present two examples from the benchmark that illustrate typical LLM-planner failures.
Case 1: Temporal constraint violation.
| Step | ViTL | LLM-planner |
|---|---|---|
| 1 | bed | tv |
| 2 | potted plant | bed |
| 3 | tv | couch |
| 4 | — | chair |
| Task completion | Yes | No |
In Table. 2, ViTL identifies bed \(\rightarrow\) potted plant \(\rightarrow\) tv as the shortest path, correctly respecting all temporal constraints. The LLM-planner reaches tv at the first step, directly violating the constraint \(\neg\textit{tv}\;\mathcal{U}\;\textit{bed}\) (tv must not be reached before bed). Despite reaching 4 targets, the task remains unsatisfied because the temporal constraint was violated.
Case 2: Premature termination.
| Step | ViTL | LLM-planner |
|---|---|---|
| 1 | tv | tv |
| 2 | bed | toilet |
| 3 | toilet | couch |
| 4 | — | bed |
| 5 | — | chair |
| Task completion | Yes | No |
In Table. 3, ViTL identifies that the path with tv \(\rightarrow\) bed \(\rightarrow\) toilet is the shortest satisfying path and terminates correctly after 3 targets. The LLM-planner instead pursues a longer branch, visiting 5 targets, and falsely declares the task complete despite the specification remaining unsatisfied.
Together, these cases illustrate two fundamental limitations of LLM-planner: temporal constraint violations during execution, and premature declaration of task completion. ViTL is immune to both, as the DFA enforces constraint satisfaction and accepts only at accepting states.
End-to-end success rate is not the most informative metric for evaluating the task-level planner. With single-target ObjectNav succeeding at approximately 54%, a sequential 3-target task would succeed roughly 15% of the time even with a perfect planner,
dropping exponentially with more targets. The dominant failure mode in this regime is navigation-level, not planning-level. To isolate planning quality, we select two HM3D scenes (ziup5kvtCCR and svBbv1Pavdk) where the
single-target navigator achieves near-90% success rate, substantially reducing navigation-level noise. We run episodes in these scenes and compare path lengths on 50 mutually completed episodes (cases where both methods successfully reached all required
targets) so that any difference is attributable to target selection quality.
Both methods use the same navigation-level executor. On mutually completed episodes, ViTL achieves an average path length of 25.45 m compared to 30.05 m for LLM-planner, a 15.31% reduction. This confirms that fewer exploration attempts translate into shorter navigation paths.
We presented ViTL, a zero-shot navigation framework that enables robots to complete long-horizon natural language navigation tasks with temporal constraints. At the task level, ViTL translates natural language commands into LTL formulas and compiles them into a DFA, whose graph structure guarantees temporal constraint satisfaction and identifies the optimal execution order, adapting in real time as environment information changes. At the navigation level, directional score produces spatially-varying value maps that improve single-target navigation accuracy and efficiency. Experiments on HM3D demonstrate competitive single-target performance and reliable completion of natural language navigation tasks, where LLM-based planners can violate temporal constraints or fail to identify optimal execution paths. Our framework currently assumes that each sub-task reduces to reaching a single object. Extending ViTL to handle richer sub-task semantics such as manipulation or interaction is a promising direction for future work.