謝國汕，殷志宏，楊 一，李澗青，李超勇

（1.浙江大學(xué) 電氣工程學(xué)院，浙江 杭州 310027；2.海鷹航空通用裝備有限責(zé)任公司，北京 102401）

0 引言

一直以來，無人機(jī)運(yùn)動(dòng)規(guī)劃問題都關(guān)注于生成一條到達(dá)某個(gè)目的地的避障軌跡［1-3］，涌現(xiàn)出許多經(jīng)典的算法，例如快速探索隨機(jī)樹（RRT）算法［4］、基于人工勢(shì)場的改進(jìn)算法［5］等。然而這些算法都存在一個(gè)缺點(diǎn)，那就是只能完成簡單的點(diǎn)到點(diǎn)的單目標(biāo)路徑規(guī)劃，而無法完成諸如無人機(jī)按照順序訪問目標(biāo)區(qū)域、按照時(shí)間順序做出某些動(dòng)作之類的復(fù)雜任務(wù)。對(duì)于這些復(fù)雜的運(yùn)動(dòng)規(guī)劃問題，基于時(shí)序邏輯的運(yùn)動(dòng)規(guī)劃算法是一種有效的解決方案。該算法的一個(gè)重點(diǎn)是使用時(shí)序邏輯語言來描述復(fù)雜的任務(wù)，其中線性時(shí)序邏輯（LTL）［6-7］是最常用的一種語言。值得注意的是，隨著無人機(jī)的快速發(fā)展，人們急需一種高階描述語言對(duì)多功能無人機(jī)的復(fù)雜任務(wù)進(jìn)行規(guī)范化表述，而其中LTL 和計(jì)算樹邏輯語言（CTL）［8］受到了廣泛的關(guān)注和研究。因此，引入時(shí)序邏輯語言以解決無人機(jī)復(fù)雜運(yùn)動(dòng)規(guī)劃的算法不僅在理論上有意義，而且也具有很大的實(shí)踐價(jià)值。

基于時(shí)序邏輯的運(yùn)動(dòng)規(guī)劃算法主要借鑒了模型檢測的概念，也就是檢驗(yàn)一個(gè)離散系統(tǒng)是否滿足某些時(shí)序邏輯形式的屬性。FAINEKOS 等將時(shí)序邏輯語言引入到任務(wù)描述里面，提出了一種該算法的基本框架［9-11］，其中主要包括3 個(gè)步驟：首先，將連續(xù)的工作環(huán)境進(jìn)行區(qū)域劃分，以獲得連續(xù)工作空間的離散模型；然后，利用模型檢測的原理，綜合工作空間的離散模型和時(shí)序邏輯公式對(duì)應(yīng)的Büchi 自動(dòng)機(jī)［12］以獲得離散任務(wù)規(guī)劃；最后，根據(jù)無人機(jī)的運(yùn)動(dòng)約束設(shè)計(jì)一個(gè)連續(xù)控制器，驅(qū)使無人機(jī)在現(xiàn)實(shí)工作環(huán)境中實(shí)現(xiàn)離散任務(wù)規(guī)劃。這種算法框架被廣泛應(yīng)用于很多復(fù)雜的場景，TUMOVá 等［13］針對(duì)復(fù)雜廣闊的環(huán)境，研究了一種基于滾動(dòng)時(shí)序的控制方法，該方法將整個(gè)運(yùn)動(dòng)過程分為許多個(gè)小的時(shí)間窗口來處理，以降低計(jì)算的復(fù)雜度。KRESS-GAZIT等［14］針對(duì)具有傳感器功能的機(jī)器人，研究了一種具備實(shí)時(shí)信息反饋的算法框架，提高了系統(tǒng)的魯棒性。殷翔等［15］將時(shí)序邏輯引入到多機(jī)器人倉庫自動(dòng)化系統(tǒng)中。STEPHEN 等［16］將機(jī)器人運(yùn)動(dòng)模型抽象為具有連續(xù)狀態(tài)和動(dòng)作空間的馬爾可夫決策過程（MDP），同時(shí)結(jié)合深層神經(jīng)網(wǎng)絡(luò)，生成一條滿足時(shí)序邏輯任務(wù)的連續(xù)軌跡。李澗青等［17］將時(shí)序邏輯引入到地球觀測衛(wèi)星的任務(wù)調(diào)度中。

在上述算法框架中，算法能夠成功運(yùn)行的一個(gè)前提是LTL 任務(wù)在當(dāng)前環(huán)境中是可以實(shí)現(xiàn)的。然而，正如FAINEKOS 等［18］所提出的，在現(xiàn)實(shí)環(huán)境中總是會(huì)存在LTL 任務(wù)無法在當(dāng)前環(huán)境中實(shí)現(xiàn)的情況，其中包括LTL 任務(wù)存在邏輯上的矛盾、無人機(jī)的運(yùn)動(dòng)約束等，在這種情況下整個(gè)算法將會(huì)失敗。針對(duì)這種情況，我們希望系統(tǒng)可以將任務(wù)失敗的原因反饋給用戶，并基于初始的LTL 任務(wù)提供一個(gè)可行的替代方案。為了解決這個(gè)問題，F(xiàn)AINEKOS 等基于松弛自動(dòng)機(jī)提出了一種近似算法，該算法首先基于初始Büchi 自動(dòng)機(jī)構(gòu)建一個(gè)松弛任務(wù)自動(dòng)機(jī)，然后利用該自動(dòng)機(jī)構(gòu)建相應(yīng)的松弛乘積自動(dòng)機(jī)，以此獲取一個(gè)可行的離散任務(wù)規(guī)劃。該算法的主要缺點(diǎn)是構(gòu)建松弛任務(wù)自動(dòng)機(jī)的過程比較復(fù)雜，且生成的離散任務(wù)規(guī)劃并不是唯一的。RAMAN 等［19］研究了一個(gè)用于機(jī)器人任務(wù)規(guī)劃的LTLMoP 工具包的擴(kuò)展框架，該框架將控制器的生成過程包含在自動(dòng)推理層中，以解決類似問題。但是該框架僅指出了時(shí)序任務(wù)中無法實(shí)現(xiàn)的部分，而沒有給出進(jìn)一步的解決措施。解決該問題的關(guān)鍵是從數(shù)學(xué)的角度解釋任務(wù)無法實(shí)現(xiàn)的根本原因，并且在重規(guī)劃算法中，需要將原子命題集之間的距離用數(shù)學(xué)公式來描述，作為衡量離散規(guī)劃偏離初始任務(wù)的標(biāo)準(zhǔn)。

本文借鑒了文獻(xiàn)［18］中的思路，通過構(gòu)建松弛乘積自動(dòng)機(jī)的方法來獲得在最小程度上違反初始時(shí)序任務(wù)的可行離散規(guī)劃。算法首先基于初始Büchi自動(dòng)機(jī)構(gòu)建一個(gè)松弛乘積自動(dòng)機(jī)；然后通過該自動(dòng)機(jī)生成一個(gè)可行的離散規(guī)劃；最后根據(jù)獲取的離散規(guī)劃對(duì)初始Büchi自動(dòng)機(jī)進(jìn)行修改，以此獲得松弛任務(wù)自動(dòng)機(jī)。此外，本文還構(gòu)造了一個(gè)新的權(quán)重函數(shù)，該函數(shù)可以幫助我們找到一條在最小程度上違反初始時(shí)序任務(wù)的離散規(guī)劃。與文獻(xiàn)［18］的算法相比較，本文重規(guī)劃算法直接利用初始Büchi自動(dòng)機(jī)來構(gòu)建松弛乘積自動(dòng)機(jī)，降低了構(gòu)建松弛乘積自動(dòng)機(jī)的復(fù)雜度，同時(shí)通過構(gòu)造新的權(quán)重函數(shù)，算法給出了最優(yōu)解，解決了生成的離散規(guī)劃不唯一的問題。為了避免破壞LTL 任務(wù)中的安全性保障，一般將LTL 任務(wù)分為“硬任務(wù)”和“軟任務(wù)”，其“硬任務(wù)”主要是無人機(jī)運(yùn)動(dòng)中的安全保障任務(wù)。本文提出的重規(guī)劃算法主要是針對(duì)“軟任務(wù)”進(jìn)行一定程度上的修改，在確保任務(wù)安全性的前提下獲取最優(yōu)解，增加了時(shí)序邏輯在無人機(jī)運(yùn)動(dòng)規(guī)劃中的適應(yīng)性。

1 問題描述和預(yù)備知識(shí)

1.1 問題描述

本文的主要目的是研究一個(gè)基于時(shí)序邏輯的無人機(jī)運(yùn)動(dòng)重規(guī)劃算法，其解決的主要問題是驅(qū)使無人機(jī)在給定的工作環(huán)境中實(shí)現(xiàn)由LTL 公式描述的時(shí)序任務(wù)，并且當(dāng)該時(shí)序任務(wù)無法在當(dāng)前環(huán)境中實(shí)現(xiàn)時(shí)，對(duì)初始任務(wù)進(jìn)行最小程度的修改以獲取一個(gè)可行的離散任務(wù)規(guī)劃?？紤]一個(gè)無人機(jī)在二維環(huán)境中執(zhí)行任務(wù)，無人機(jī)的動(dòng)力學(xué)p滿足如下公式：

式中：p=[x y]T∈P?R2為無人機(jī)在X-Y坐標(biāo)系中的坐標(biāo)；θ為當(dāng)前航向角；v、ω分別為無人機(jī)的當(dāng)前運(yùn)動(dòng)速度和角速度。

本文中無人機(jī)的時(shí)序任務(wù)用LTL 公式φ來描述，該公式建立在原子命題的有限集合上，而這些原子命題標(biāo)記了工作環(huán)境中感興趣的區(qū)域或者這些區(qū)域所提供的服務(wù)。假設(shè)∏={π1，π2，…，πn}是一組感興趣的區(qū)域，則定義一個(gè)映射關(guān)系hC：P→∏，該映射將工作環(huán)境P中的坐標(biāo)映射到命題集∏中。

一般地，本文研究的主要問題可以描述如下：考慮一個(gè)無人機(jī)在二維環(huán)境上執(zhí)行復(fù)雜的任務(wù)，假設(shè)該無人機(jī)的運(yùn)動(dòng)由式（1）描述，其初始位置為p（0），則本文要解決的問題是如何構(gòu)造一種混合控制器，驅(qū)使無人機(jī)在工作環(huán)境中實(shí)現(xiàn)任務(wù)。此外，如果該任務(wù)無法在當(dāng)前環(huán)境中實(shí)現(xiàn)，則在最小程度上放寬時(shí)序任務(wù)對(duì)系統(tǒng)的約束，以此來構(gòu)建一個(gè)有效的混合控制器。

為了更好地描述上述問題，本文用一個(gè)簡單的例子來說明。假設(shè)一個(gè)無人機(jī)在具有5 個(gè)感興趣區(qū)域的正方形工作空間中執(zhí)行任務(wù)，如圖1 所示，其中的區(qū)域分別標(biāo)識(shí)為π1（藍(lán)色）、π2（青色）、π3（黃色）、π4（綠色）和π5（紅色）。這些區(qū)域的連通圖和提供的服務(wù)如圖2 所示。無人機(jī)的初始位置位于π1的某處，它分別需要完成以下兩個(gè)任務(wù)：1）訪問區(qū)域π4和π5，然后一直停留在區(qū)域π5，與此同時(shí)，無人機(jī)在移動(dòng)過程中需要獲取服務(wù)a2；2）訪問區(qū)域π4和π5，然后停留在區(qū)域π5，與此同時(shí)，無人機(jī)在運(yùn)動(dòng)期間要避免經(jīng)過提供服務(wù)a1的區(qū)域。

1.2 線性時(shí)序邏輯

圖1 包含5 個(gè)區(qū)域的工作空間Fig.1 Workspace with five regions

圖2 區(qū)域連通圖Fig.2 Connected regions graph

在邏輯學(xué)里面，術(shù)語時(shí)序邏輯（Temporal Logic）被用來描述為表現(xiàn)和推理關(guān)于時(shí)間限定的命題的規(guī)則和符號(hào)化的任何系統(tǒng)，它有時(shí)候也被稱為時(shí)態(tài)邏輯。給定一個(gè)原子命題集Σ，一個(gè)線性時(shí)序邏輯表達(dá)式符合如下語法［20］：

對(duì)于?φ∈∑，φ都是一個(gè)LTL 表達(dá)式；假如φ1和φ2都是LTL 表達(dá)式，那么○φ1、φ1∪φ2、◇φ1和□φ1都是LTL 表達(dá)式，其中，（非）、∧（與）、∨（或）都是標(biāo)準(zhǔn)的布爾邏輯運(yùn)算符，○（接下來）、∪（直到）、◇（最終）和□（永遠(yuǎn)）為時(shí)序邏輯運(yùn)算符。

對(duì)于上述時(shí)序邏輯運(yùn)算符，○φ1表示φ1在下一步為真；φ1∪φ2表示直到φ2為真，φ1一直保持為真；◇φ1表示在將來的某一時(shí)刻，φ1一定為真；□φ1表示在任意時(shí)刻，φ1都保持為真。對(duì)于前面所述的例子，其中的兩個(gè)任務(wù)可以分別表述為兩個(gè)LTL公式：

為了使用離散邏輯來解決連續(xù)狀態(tài)的任務(wù)規(guī)劃問題，我們首先需要對(duì)狀態(tài)轉(zhuǎn)移系統(tǒng)和自動(dòng)機(jī)進(jìn)行初步了解。所以得出如下兩個(gè)定義。

定義1一個(gè)有限狀態(tài)轉(zhuǎn)移系統(tǒng)（TS）可以用如下一個(gè)元組表示：

式中：S={s0，s1，…，sn}為一個(gè)包含有限狀態(tài)的集合；∏為一組有限原子命題；σ?S×S為狀態(tài)之間的轉(zhuǎn)移關(guān)系；sinit∈S為系統(tǒng)的初始狀態(tài)；L：S→2∏為一個(gè)標(biāo)簽函數(shù)，它標(biāo)識(shí)了每個(gè)狀態(tài)所滿足的原子命題。

一般地，系統(tǒng)T的路徑可以表示為狀態(tài)的無窮序列p=sinitsisi+1…，與之相對(duì)應(yīng)的原子命題序列為trace(p)=L(sinit)L(si)L(si+1)…。我們將系統(tǒng)T的所有原子命題序列所組成的集合稱為系統(tǒng)T的語言L（T），也就是L(T)={trace(p1)，trace(p2)，…}。

對(duì)于一個(gè)基于原子命題集Σ的LTL 公式φ，我們可以通過相對(duì)應(yīng)的Büchi 自動(dòng)機(jī)［21］來獲取滿足公式φ的命題序列。

定義2一個(gè)Büchi 自動(dòng)機(jī)是一個(gè)包含5 個(gè)元素的元組

式中：Q為有限狀態(tài)集；Σ代表所有輸入命題的組合構(gòu)成的集；δ?Q×2∑×Q為狀態(tài)之間的轉(zhuǎn)移關(guān)系，q0∈Q為初始狀態(tài)集；F?Q為可接受狀態(tài)集。

給定一個(gè)基于原子命題集Σ的輸入序列traceρ=w(0)w(1)w(2)…，Büchi 自動(dòng)機(jī)B可以生成一條包含無限個(gè)狀態(tài)的序列ρ=q0q1q2…，其中?i≥0，都有(qi，w(i)，qi+1)∈δ，我們將該狀態(tài)序列稱為Büchi 自動(dòng)機(jī)B的一條路徑。如果?qf∈F，qf在路徑ρ中循環(huán)出現(xiàn)，則將該路徑稱為B的可接受路徑，而相應(yīng)的輸入序列trace(ρ)是能夠被Büchi 自動(dòng)機(jī)接受的。類似地，我們將所有Büchi 自動(dòng)機(jī)B的可接受命題序列的集合稱為Büchi 自動(dòng)機(jī)B的語言，記為L（B）。

2 基于時(shí)序邏輯的運(yùn)動(dòng)規(guī)劃

基于時(shí)序邏輯的運(yùn)動(dòng)規(guī)劃算法包括3 個(gè)步驟，一般地可以將這3 個(gè)步驟分為兩個(gè)階段：1）上層綜合階段主要是結(jié)合工作環(huán)境的約束和LTL 任務(wù)的約束，獲取一條可行的離散規(guī)劃；2）底層綜合階段主要是考慮無人機(jī)的動(dòng)力學(xué)約束，設(shè)計(jì)一個(gè)控制器來驅(qū)使無人機(jī)按照離散規(guī)劃完成任務(wù)。本文專注于第1 階段的算法研究，并且重點(diǎn)關(guān)注在當(dāng)前環(huán)境中無法實(shí)現(xiàn)的LTL 任務(wù)的處理，而底層無人機(jī)的運(yùn)動(dòng)控制器可以根據(jù)文獻(xiàn)［21］的研究成果來設(shè)計(jì)。

2.1 無人機(jī)運(yùn)動(dòng)模型

為了能夠利用時(shí)序邏輯來處理連續(xù)系統(tǒng)，首先需要對(duì)二維環(huán)境P進(jìn)行區(qū)域劃分，文獻(xiàn)［22-23］對(duì)平面區(qū)域劃分進(jìn)行了深入的研究。本文主要采用了文獻(xiàn)［20］里面的三角形區(qū)域劃分法。該方法的主要優(yōu)點(diǎn)是便于后續(xù)設(shè)計(jì)符合三角區(qū)域特點(diǎn)的連續(xù)控制器，而且文獻(xiàn)［21］提供了一個(gè)高效的針對(duì)復(fù)雜多邊形環(huán)境進(jìn)行三角形分解的算法。

定義一個(gè)映射Γ：P→D將P中的每個(gè)位置映射到有限集D={d1，d2，…，dND}中，則Γ-1(d)包含所有位于標(biāo)記為d的單元格內(nèi)的位置，而D=被稱為工作空間P的一個(gè)區(qū)域劃分。針對(duì)該區(qū)域劃分，無人機(jī)的運(yùn)動(dòng)模型可以定義為一個(gè)有限狀態(tài)轉(zhuǎn)移系統(tǒng)：

式中：D為有限狀態(tài)集合；d0為無人機(jī)初始位置所對(duì)應(yīng)的單元格；→D?D×D是狀態(tài)轉(zhuǎn)移關(guān)系；對(duì)于工作環(huán)境P來說，當(dāng)且僅當(dāng)單元格di和dj相鄰時(shí)，才有(di，dj)∈→D且(dj，di)∈→D；hD為一個(gè)觀察映射關(guān)系，定義為hD(d)=hC(Γ-1(d))。類似地，將系統(tǒng)M的路徑定義為τ=d0d1d2…，其中?i≥0，(di，di+1)∈→D。

利用三角分解的方法，工作環(huán)境P可以劃分成如圖3 所示。

圖3 工作空間的三角分解Fig.3 Triangular decomposition of the workspace

2.2 離散任務(wù)規(guī)劃

給定一個(gè)無人機(jī)的離散模型M和需要完成的任務(wù)表達(dá)式φ，我們可以用模型檢測的方法來生成一條離散規(guī)劃。模型檢測是一個(gè)計(jì)算機(jī)領(lǐng)域的術(shù)語，它是一種用來檢測一個(gè)有限狀態(tài)系統(tǒng)是否滿足給定的屬性的方法，其中需要檢驗(yàn)的屬性一般用邏輯語言進(jìn)行描述，而有限狀態(tài)系統(tǒng)對(duì)應(yīng)本文的無人機(jī)模型M。實(shí)現(xiàn)模型檢測算法的第一步是要把離散模型M和LTL 表達(dá)式φ對(duì)應(yīng)的Büchi 自動(dòng)機(jī)結(jié)合起來，為此需要構(gòu)建一個(gè)乘積自動(dòng)機(jī)。

定義3對(duì)于離散模型M=(D，d0，→D，hD，AP，L)，LTL 表達(dá)式φ對(duì)應(yīng)的Büchi 自動(dòng)機(jī)B={Q，∑，δ，Q0，F(xiàn)}，那么乘積自動(dòng)機(jī)Pt=M×B可以表示為一個(gè)元組

式中：QP=D×Q為有限狀態(tài)集；σP?QP×QP代表狀態(tài)轉(zhuǎn)移關(guān)系，當(dāng)且僅當(dāng)(d，d′)∈→D且?l?L(d)，使得(q，l，q′)∈σ時(shí)，((d，q)，(d′，q′))∈σP；QP，0=(d0，q0)為初始狀態(tài)集；FP=D×F為可接受狀態(tài)集；APP為原子命題集；LP：QP→為一個(gè)標(biāo)簽函數(shù)，它標(biāo)識(shí)了每個(gè)狀態(tài)所滿足的原子命題集；wP：σP→R為一個(gè)取值非負(fù)的權(quán)重函數(shù)，本文采用區(qū)域劃分后各單元中心之間的距離來衡量。

在自動(dòng)機(jī)理論中，在離散系統(tǒng)M中尋找滿足某個(gè)LTL 公式φ（或者說滿足φ對(duì)應(yīng)的Büchi 自動(dòng)機(jī)B）的狀態(tài)序列，其實(shí)就是在系統(tǒng)M的語言L（M）中尋找屬于Büchi 自動(dòng)機(jī)B語言L（B）的子集，也就是L(M)∩L(B)，如圖4 所示。而這可以通過兩個(gè)自動(dòng)機(jī)的笛卡爾乘積來構(gòu)建，因此，L(P)=L(M)∩L(B)。

圖4 兩個(gè)自動(dòng)機(jī)系統(tǒng)的語言交集Fig.4 Language intersection of two automata system

一般地，我們通過構(gòu)建一個(gè)加權(quán)有向圖G=(V，E，wP)對(duì)乘積自動(dòng)機(jī)P做進(jìn)一步處理，其中，V=QP代表有向圖的節(jié)點(diǎn)；E=QP×QP代表有向圖的邊，對(duì)應(yīng)于P中的狀態(tài)轉(zhuǎn)換關(guān)系。然后，利用Dijkstra 算法［22］，可以獲取一條從初始狀態(tài)到可接受狀態(tài)的最短路徑。對(duì)于這樣一條路徑rP=(d0，q0)(d1，q1)…，如果?(di，qi)∈FP，使得(di，qi)在FP中循環(huán)出現(xiàn)，則稱rP為乘積自動(dòng)機(jī)Pt的可接受路徑。將可接受路徑rP映射到離散系統(tǒng)M中，則可以獲得相應(yīng)的離散路徑rP|M=d0d1…。一般地，可接受路徑可以寫成前綴部分和后綴部分的組合形式rP=rpre(rsuf)ω，其中rpre=(d0，q0)…(ds，qs)是有向圖里的一條有限路徑，rsuf=(dk+1，qk+1)…(ds，qs)是有向圖里的一個(gè)環(huán)，并且(dk+1，qk+1)∈FP。也就是說，rpre是一條從初始狀態(tài)到某一個(gè)可接受狀態(tài)的路徑，而rsuf是一個(gè)從某個(gè)可接受狀態(tài)回到它本身的環(huán)形路徑。另外，如果有向圖中沒有從初始狀態(tài)到任意一個(gè)可接受狀態(tài)的路徑，那么該乘積自動(dòng)機(jī)就不存在可接受路徑，也就是說該時(shí)序任務(wù)無法在當(dāng)前環(huán)境中實(shí)現(xiàn)。

對(duì)于式（2）的時(shí)序任務(wù)，采用上述算法獲取的離散任務(wù)如圖3 所示，無人機(jī)需要經(jīng)過的區(qū)域依次為π1、π2、π4和π5。式（3）對(duì)應(yīng)的Büchi 自動(dòng)機(jī)如圖5所示，該自動(dòng)機(jī)包含了3 個(gè)狀態(tài)，其中，s0是初始狀態(tài)，s2是可接受狀態(tài)。

圖5 時(shí)序邏輯任務(wù)3 的Büchi 自動(dòng)機(jī)Fig.5 Büchi automaton of the LTL specification 3

結(jié)合無人機(jī)的離散系統(tǒng)M，最終的乘積自動(dòng)機(jī)如圖6 所示。其中，紅色圓圈的狀態(tài)代表初始狀態(tài)，藍(lán)色圓圈的狀態(tài)代表可接受狀態(tài)，從中可以看出，該自動(dòng)機(jī)不存在可接受路徑。同時(shí)，根據(jù)圖2 的區(qū)域連通圖，無人機(jī)在到達(dá)區(qū)域π5之前必須經(jīng)過區(qū)域π2或者π3，而這些區(qū)域均提供服務(wù)a1，這與所給的任務(wù)相違背。因此，式（3）描述的任務(wù)在當(dāng)前工作環(huán)境中是不能夠?qū)崿F(xiàn)的。

圖6 時(shí)序邏輯任務(wù)3 的乘積自動(dòng)機(jī)Fig.6 Product automaton of the LTL specification 3

3 任務(wù)重規(guī)劃算法

在基于時(shí)序邏輯的運(yùn)動(dòng)規(guī)劃算法中，整個(gè)系統(tǒng)能夠正常運(yùn)行的一個(gè)重要前提條件是LTL 任務(wù)在所給的工作環(huán)境中是可以實(shí)現(xiàn)的，也就是上層綜合階段能夠生成一條可行的離散規(guī)劃。而對(duì)于無法實(shí)現(xiàn)的LTL 任務(wù)，系統(tǒng)將終止于乘積自動(dòng)機(jī)的構(gòu)建而無法生成最終軌跡。針對(duì)這種情況，本文基于文獻(xiàn)［19］中松弛自動(dòng)機(jī)的描述，利用離散系統(tǒng)M和初始LTL 任務(wù)對(duì)應(yīng)的Büchi 自動(dòng)機(jī)B構(gòu)建一個(gè)松弛乘積自動(dòng)機(jī)，由該自動(dòng)機(jī)生成一條在最大程度上滿足初始LTL 任務(wù)的離散規(guī)劃，而借助該離散規(guī)劃，對(duì)初始Büchi 自動(dòng)機(jī)進(jìn)行修改以獲取松弛任務(wù)自動(dòng)機(jī)。

定義4對(duì)于離散模型M和Büchi 自動(dòng)機(jī)B，松弛乘積自動(dòng)機(jī)Pr可以表示為一個(gè)元組：

式中：Qr=D×Q為一個(gè)有限狀態(tài)集；σr?Qr×Qr為狀態(tài)轉(zhuǎn)移關(guān)系，當(dāng)且僅當(dāng)(d，d′)∈→D且，使得(q，l′，q′)∈σ時(shí)，((d，q)，(d′，q′))∈σr；Qr，0=(d0，q0)為初始狀態(tài)集；Fr=D×F為可接受狀態(tài)集；APr=APP為原子命題集；Lr：Qr→是一個(gè)標(biāo)簽函數(shù)，它標(biāo)識(shí)了每個(gè)狀態(tài)所滿足的原子命題集；wr：σr→R是一個(gè)取值非負(fù)的權(quán)重函數(shù)，具體定義見下文。

注意到，松弛乘積自動(dòng)機(jī)Pr與一般乘積自動(dòng)機(jī)Pt的主要區(qū)別在于狀態(tài)轉(zhuǎn)換關(guān)系和權(quán)重函數(shù)的定義上，在一般乘積自動(dòng)機(jī)Pt里，轉(zhuǎn)換關(guān)系σP的約束條件是“?l?L(d)使得(q，l，q′)∈σ”，而在松弛乘積自動(dòng)機(jī)里面，轉(zhuǎn)換關(guān)系σr的約束條件變?yōu)榱耸沟?q，l′，q′)∈σ”。如前文所述，當(dāng)初始LTL 任務(wù)無法在當(dāng)前環(huán)境中實(shí)現(xiàn)時(shí)，系統(tǒng)M的語言和Büchi自動(dòng)機(jī)的語言是不存在交集的，對(duì)于離散系統(tǒng)M中可接受路徑的某些狀態(tài)轉(zhuǎn)換(d，d′)和Büchi 自動(dòng)機(jī)里可接受路徑的某些狀態(tài)轉(zhuǎn)換(q，l，q′)，原子命題集合L(d)和l的關(guān)系不滿足一般乘積自動(dòng)機(jī)里轉(zhuǎn)換關(guān)系的定義（即包含關(guān)系），它們之間可能是交集關(guān)系或者完全不相交。

令χ(l′，L(d))=l′-L(d)，則χ(l′，L(d))代表了要使轉(zhuǎn)移關(guān)系((d，q)，(d′，q′))在Pr中成立，命題集l′必須去除的命題。對(duì)于命題集li和lj，我們將其距離定義為兩者差的一階范式：

則松弛乘積自動(dòng)機(jī)Pr的權(quán)重函數(shù)wr可以定義為

式中：((d，q)，(d′，q′))∈σr，w(d，d′)為從單元格d移動(dòng)到單元格d′ 的代價(jià)，λ(q，q′)=Dist(λ(q，q′)，L(d))計(jì)算了松弛乘積自動(dòng)機(jī)里從狀態(tài)(d，q)到(d′，q′)的命題序列和從單元格d移動(dòng)到單元格d′的命題序列之間的距離，也就是該狀態(tài)轉(zhuǎn)移關(guān)系違背初始任務(wù)的程度。當(dāng)該值等于0 時(shí)，說明初始任務(wù)沒有被違背；而值越大說明該狀態(tài)轉(zhuǎn)移關(guān)系越偏離初始任務(wù)。α≥0是一個(gè)設(shè)計(jì)參數(shù)，它可以調(diào)節(jié)偏離程度在權(quán)重函數(shù)中的比重，體現(xiàn)了用戶偏向于盡量獲取一個(gè)可行離散計(jì)劃還是使最終的離散計(jì)劃盡可能接近初始任務(wù)。α的值越大，得到的離散規(guī)劃越接近初始任務(wù)。

任務(wù)重規(guī)劃算法的偽代碼在算法1 中給出。該算法由兩部分組成：第1 部分是從第1 行到第15 行，它的主要內(nèi)容是建立松弛乘積自動(dòng)機(jī)；第2 部分是從第16 行到末尾，它的主要內(nèi)容是利用Dijkstra 算法尋找出可接受的路徑，然后利用改路徑對(duì)初始Büchi 自動(dòng)機(jī)進(jìn)行修改，以獲取松弛任務(wù)自動(dòng)機(jī)B′。

算法1任務(wù)重規(guī)劃算法

輸入：離散系統(tǒng)M，LTL 任務(wù)相應(yīng)的Büchi 自動(dòng)機(jī)B，設(shè)計(jì)參數(shù)α

輸出：離散任務(wù)規(guī)劃rP，松弛任務(wù)自動(dòng)機(jī)B′

1）Qr：=?，σr：=?，Qr，0：=?，F(xiàn)r：=?，B′：=B

2）foreachd∈Ddo

3）foreachq∈Qdo

4）if(d，q)?Qrthen

5）將(d，q)添加到Qr

6）ifq∈Q0then

7）將(d，q)添加到Qr，0

8.）ifq∈Fthen

9）將(d，q)添加到Fr

10）for 所有滿足(d，d′)∈→D的d′do

11）Φ=

12）foreachq′∈Φdo

13）將轉(zhuǎn)換關(guān)系((d，q)，(d′，q′))添加到σr

14）根據(jù)式（6）計(jì)算權(quán)重wr((d，q)，(d′，q′))

15）構(gòu)建松弛乘積自動(dòng)機(jī)Pr

16）利用Dijkstra 算法從Pr中求出離散任務(wù)規(guī)劃rP

17）foreach((d，q)，(d′，q′))∈rPdo

18）if(q，L(d)，q′)?σthen

19）將轉(zhuǎn)換關(guān)系（q，L（d），q′）添加到B′

給定一個(gè)工作環(huán)境P和LTL 任務(wù)表達(dá)式φ，如果LTL 任務(wù)在當(dāng)前環(huán)境中是可以實(shí)現(xiàn)的，則一般的路徑規(guī)劃算法可以快速地提供一條最優(yōu)離散規(guī)劃。而如果任務(wù)在當(dāng)前環(huán)境中是無法實(shí)現(xiàn)的，則必須放松LTL 任務(wù)的約束，構(gòu)建一個(gè)在一定程度上偏離初始LTL 任務(wù)的松弛乘積自動(dòng)機(jī)，然后利用該自動(dòng)機(jī)獲取一條可行的離散規(guī)劃?；跁r(shí)序邏輯的任務(wù)重規(guī)劃算法總結(jié)于算法2 中。值得注意的是，盡管最終的可接受路徑是通過松弛乘積自動(dòng)機(jī)獲取的，但離散系統(tǒng)M是沒有改變的，因此最終的離散規(guī)劃仍然是可以實(shí)現(xiàn)的。

算法2基于時(shí)序邏輯的任務(wù)重規(guī)劃算法

輸入：工作空間P，LTL 任務(wù)表達(dá)式φ，設(shè)計(jì)參數(shù)α

輸出：離散路徑rP|M，松弛任務(wù)自動(dòng)機(jī)B′

1）對(duì)P進(jìn)行區(qū)域劃分，得到離散系統(tǒng)M

2）獲取φ相應(yīng)的Büchi 自動(dòng)機(jī)，構(gòu)建乘積自動(dòng)機(jī)Pt

3）構(gòu)建Pt相應(yīng)的有向圖，利用Dijkstra 算法求出可接收路徑rP，跳到步驟5

4）如果Pt不存在可接收路徑，則調(diào)用算法1

5）將rP映射到離散系統(tǒng)中，獲取離散路徑rP|M

假設(shè)集合D和Q的大小分別為|D|和|Q|，那么算法1 中第1 個(gè)和第2 個(gè)循環(huán)的時(shí)間復(fù)雜度分別為Ο(|D|)和Ο(|Q|)；在最差的情況下，對(duì)于D中的任意一個(gè)節(jié)點(diǎn)，存在|D|-1 條邊，第10 行的循環(huán)時(shí)間復(fù)雜度為Ο(|D|-1)，截至第14 行，算法的時(shí)間復(fù)雜度為Ο(|D|2×|Q|)。乘積自動(dòng)機(jī)包含了|D|×|Q|個(gè)節(jié)點(diǎn)，則Dijkstra 算法的時(shí)間復(fù)雜度為Ο(|D|×|Q|log(|D|×|Q|))，因此，算法1 的時(shí)間復(fù)雜度為Ο(|D|2×|Q|+|D|×|Q|log(|D|×|Q|))。

4 仿真驗(yàn)證

為有效驗(yàn)證本文所提出的任務(wù)重規(guī)劃算法，本節(jié)針對(duì)圖1 所示的工作環(huán)境進(jìn)行時(shí)序任務(wù)仿真。其中，各個(gè)感興趣區(qū)域的中心坐標(biāo)分別為π1（16.0，80.5），π2（80.5，90.0），π3（6.0，6.5），π4（70.0，6.5），π5（40.5，42.5）。

首先，考慮式（3）所示的LTL 任務(wù)，當(dāng)α取不同值時(shí)，最終的離散任務(wù)規(guī)劃見表1。從中可以看出，隨著α取的增大，離散任務(wù)規(guī)劃將抵達(dá)更多的區(qū)域以完成任務(wù)，而這將不可避免地違背了初始任務(wù)中的某些約束。

表1 在不同α 值得情況下，時(shí)序邏輯任務(wù)3 的離散規(guī)劃Tab.1 Discrete planning of the LTL specification 3 with different α

接下來，考慮這樣一個(gè)任務(wù)，無人機(jī)需要在區(qū)域π1和區(qū)域π5間來回訪問，同時(shí)避免經(jīng)過提供服務(wù)a2或a3的區(qū)域。相對(duì)應(yīng)的LTL 表達(dá)式如下：

從圖1 可以看出，無人機(jī)在到達(dá)區(qū)域π5之前必須經(jīng)過區(qū)域π2（提供服務(wù)a2）或者區(qū)域π4（提供服務(wù)a3），這與“避免經(jīng)過提供服務(wù)a2或a3的區(qū)域”這一要求相違背，因此，該任務(wù)在當(dāng)前工作環(huán)境中是無法實(shí)現(xiàn)的。當(dāng)取α=100 時(shí)，在只考慮感興趣的區(qū)域時(shí)，無人機(jī)的路徑規(guī)劃為

采用文獻(xiàn)［21］所提出的無人機(jī)運(yùn)動(dòng)控制算法，無人機(jī)路徑規(guī)劃里的前綴部分所對(duì)應(yīng)的運(yùn)動(dòng)軌跡如圖7 所示。

圖7 時(shí)序邏輯任務(wù)7 對(duì)應(yīng)的無人機(jī)運(yùn)動(dòng)軌跡Fig.7 The UAV trajectory of the LTL specification 7

5 結(jié)束語

本文研究了復(fù)雜環(huán)境下基于時(shí)序邏輯的無人機(jī)運(yùn)動(dòng)重規(guī)劃算法。通過深入分析模型檢測的基本過程，在離散模型M中尋找滿足時(shí)序任務(wù)φ的離散規(guī)劃其實(shí)就是尋找兩個(gè)自動(dòng)機(jī)模型的語言交集，也就是L(M)∩L(B)，而這剛好可以通過兩個(gè)系統(tǒng)的笛卡爾乘積來獲取，這就是基于時(shí)序邏輯的運(yùn)動(dòng)規(guī)劃算法的本質(zhì)。為了解決時(shí)序任務(wù)無法實(shí)現(xiàn)的問題，本文首先根據(jù)初始時(shí)序任務(wù)構(gòu)建一個(gè)松弛乘積自動(dòng)機(jī)；然后通過該自動(dòng)機(jī)生成一個(gè)可行的離散規(guī)劃；最后根據(jù)獲取的離散規(guī)劃對(duì)初始Büchi 自動(dòng)機(jī)進(jìn)行修改，以此獲得松弛任務(wù)自動(dòng)機(jī)。本文的重規(guī)劃算法主要針對(duì)的是時(shí)序邏輯任務(wù)與工作環(huán)境存在沖突的情況，而對(duì)于一些由于無人機(jī)的運(yùn)動(dòng)約束，導(dǎo)致時(shí)序任務(wù)無法實(shí)現(xiàn)的情況，則需要做進(jìn)一步的研究。此外，針對(duì)多無人機(jī)協(xié)同運(yùn)動(dòng)的情況也是以后的研究方向。