<p>Symbolic planning methods for continuous state spaces have traditionally relied on model-checking techniques being applied to a discrete model of the space in question. Such models are usually obtained as dual graphs to tilings of the state space by contractible regions (finite polytopes, usually), converting the planning problem into a graph search problem. The inherently high computational complexity of these methods motivates considering discretizations that are more frugally constructed, while retaining all the pertinent topological information about the state space. Moreover, Farber’s theory of topological complexity of continuous planning favors the requirement that the homotopy types of the state space and its models coincide. The Nerve Lemma indicates it may be possible to obtain the desired models of a state space as particular sub-complexes of the barycentric subdivision of the nerve <InlineEquation ID="IEq1"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="41468_2025_217_Article_IEq1.gif" Format="GIF" Height="19" Rendition="HTML" Resolution="72" Type="Linedraw" Width="39" /> </InlineMediaObject> <EquationSource Format="TEX">${{\mathcal {N}}\!({\mathbb {U}})}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="script">N</mi> <mspace width="-0.166667em" /> <mo stretchy="false">(</mo> <mi mathvariant="double-struck">U</mi> <mo stretchy="false">)</mo> </mrow> </math></EquationSource> </InlineEquation> of a good open cover <InlineEquation ID="IEq2"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="41468_2025_217_Article_IEq2.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="13" /> </InlineMediaObject> <EquationSource Format="TEX">${\mathbb {U}}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="double-struck">U</mi> </math></EquationSource> </InlineEquation> indexed by the symbols. This article develops the basic theory required for conducting symbolic planning over models obtained in this way. The obstructions to deploying the model-checking paradigm for path-planning over an open cover <InlineEquation ID="IEq3"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="41468_2025_217_Article_IEq2.gif" Format="GIF" Height="14" Rendition="HTML" Resolution="72" Type="Linedraw" Width="13" /> </InlineMediaObject> <EquationSource Format="TEX">${\mathbb {U}}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="double-struck">U</mi> </math></EquationSource> </InlineEquation> are identified and characterized, resulting in a model <InlineEquation ID="IEq4"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="41468_2025_217_Article_IEq4.gif" Format="GIF" Height="19" Rendition="HTML" Resolution="72" Type="Linedraw" Width="55" /> </InlineMediaObject> <EquationSource Format="TEX">${{\mathcal {N}}_{\scriptscriptstyle {red}}({\mathbb {U}})}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <msub> <mi mathvariant="script">N</mi> <mstyle displaystyle="false" scriptlevel="2"> <mrow> <mi mathvariant="italic">red</mi> </mrow> </mstyle> </msub> <mrow> <mo stretchy="false">(</mo> <mi mathvariant="double-struck">U</mi> <mo stretchy="false">)</mo> </mrow> </mrow> </math></EquationSource> </InlineEquation> called the reduced nerve of the cover, and an algorithm for solving LTL-planning problems is presented. Furthermore, in the case of a good cover, it is shown that all the vertices of the complement of <InlineEquation ID="IEq5"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="41468_2025_217_Article_IEq4.gif" Format="GIF" Height="19" Rendition="HTML" Resolution="72" Type="Linedraw" Width="55" /> </InlineMediaObject> <EquationSource Format="TEX">${{\mathcal {N}}_{\scriptscriptstyle {red}}({\mathbb {U}})}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <msub> <mi mathvariant="script">N</mi> <mstyle displaystyle="false" scriptlevel="2"> <mrow> <mi mathvariant="italic">red</mi> </mrow> </mstyle> </msub> <mrow> <mo stretchy="false">(</mo> <mi mathvariant="double-struck">U</mi> <mo stretchy="false">)</mo> </mrow> </mrow> </math></EquationSource> </InlineEquation> may be deleted from the subdivided nerve without altering its homotopy type.</p>

Topology-aware planning under linear temporal logic constraints

期刊论文
发表日期：

2025年6月23日

查看全文

Dan P. Guralnik,
Yu Wang,
Warren E. Dixon

摘要

Symbolic planning methods for continuous state spaces have traditionally relied on model-checking techniques being applied to a discrete model of the space in question. Such models are usually obtained as dual graphs to tilings of the state space by contractible regions (finite polytopes, usually), converting the planning problem into a graph search problem. The inherently high computational complexity of these methods motivates considering discretizations that are more frugally constructed, while retaining all the pertinent topological information about the state space. Moreover, Farber’s theory of topological complexity of continuous planning favors the requirement that the homotopy types of the state space and its models coincide. The Nerve Lemma indicates it may be possible to obtain the desired models of a state space as particular sub-complexes of the barycentric subdivision of the nerve ${{\mathcal {N}}\!({\mathbb {U}})}$ $N (U)$ of a good open cover ${\mathbb {U}}$ $U$ indexed by the symbols. This article develops the basic theory required for conducting symbolic planning over models obtained in this way. The obstructions to deploying the model-checking paradigm for path-planning over an open cover ${\mathbb {U}}$ $U$ are identified and characterized, resulting in a model ${{\mathcal {N}}_{\scriptscriptstyle {red}}({\mathbb {U}})}$ $N_{red} (U)$ called the reduced nerve of the cover, and an algorithm for solving LTL-planning problems is presented. Furthermore, in the case of a good cover, it is shown that all the vertices of the complement of ${{\mathcal {N}}_{\scriptscriptstyle {red}}({\mathbb {U}})}$ $N_{red} (U)$ may be deleted from the subdivided nerve without altering its homotopy type.