面向無人駕駛時(shí)空同步約束制導(dǎo)的安全強(qiáng)化學(xué)習(xí)

王金永 黃志球 楊德艷 Xiaowei Huang 祝 義 華高洋

1(南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 南京 211106) 2(高安全系統(tǒng)的軟件開發(fā)與驗(yàn)證技術(shù)工信部重點(diǎn)實(shí)驗(yàn)室(南京航空航天大學(xué)) 南京 211106) 3(江蘇師范大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 江蘇徐州 221116) 4(利物浦大學(xué)計(jì)算機(jī)科學(xué)系 英國利物浦 L69 3BX)

無人駕駛系統(tǒng)可以看作是自車車輛和環(huán)境在時(shí)間空間上的轉(zhuǎn)移，其安全性一直是阻礙無人駕駛普及的首要問題.系統(tǒng)安全性(safety)可定義為壞的事情永遠(yuǎn)不要發(fā)生，無人駕駛安全指的是車輛之間和車輛與周圍的環(huán)境之間不要發(fā)生碰撞.無人駕駛決策模塊需要根據(jù)動(dòng)態(tài)的時(shí)鐘和空間信息做出正確安全的決策，提供安全的時(shí)空道路通行權(quán)(right-of-way)，避免在某一時(shí)刻自車車輛與周圍環(huán)境車輛的空間重疊.安全攸關(guān)的無人駕駛車輛處在復(fù)雜的時(shí)空運(yùn)動(dòng)軌跡中，在面對(duì)沒有訓(xùn)練過的未知不確定場景時(shí)，系統(tǒng)設(shè)計(jì)者不僅需要采用強(qiáng)化學(xué)習(xí)(reinforce-ment learning, RL)的方法來訓(xùn)練車輛，使得車輛獲得最優(yōu)的策略和累計(jì)獎(jiǎng)勵(lì)，而且更加需要特定領(lǐng)域的形式化規(guī)約方法，為強(qiáng)化學(xué)習(xí)提供安全約束和保障.

無人駕駛決策的方法可以分為2類：1)基于規(guī)則(rule-based)的方法，比如有限狀態(tài)機(jī)(finite state machine)；2)數(shù)據(jù)驅(qū)動(dòng)(data-driven)的方法，比如機(jī)器學(xué)習(xí)(machine learning)的方法.基于規(guī)則的決策系統(tǒng)可以根據(jù)事先定義好的規(guī)則輸出事先規(guī)定好的動(dòng)作，從而實(shí)現(xiàn)系統(tǒng)的安全與可解釋性[1-4].盡管基于規(guī)則的方法可以為安全的系統(tǒng)操作提供保障，但是只有復(fù)雜的現(xiàn)實(shí)環(huán)境與待驗(yàn)證的模型相匹配才可以滿足系統(tǒng)設(shè)計(jì)的需要[5].對(duì)于復(fù)雜的無人駕駛交通場景，系統(tǒng)狀態(tài)轉(zhuǎn)換較多，決策系統(tǒng)不能理解周圍復(fù)雜的交通環(huán)境，而且對(duì)于未識(shí)別的系統(tǒng)狀態(tài)無法給出較好的決策行為[6].基于數(shù)據(jù)驅(qū)動(dòng)的方法，通過與環(huán)境交互大量的學(xué)習(xí)訓(xùn)練，可以理解學(xué)習(xí)周圍的環(huán)境.對(duì)于深度強(qiáng)化學(xué)習(xí)來說，學(xué)習(xí)的過程受獎(jiǎng)勵(lì)函數(shù)的指導(dǎo)，產(chǎn)生從觀測輸入到動(dòng)作輸出的策略.但是基于學(xué)習(xí)的決策方法，較多依賴數(shù)據(jù)和黑盒訓(xùn)練，缺少學(xué)習(xí)過程的安全約束和決策結(jié)果的可解釋性[7-12].因此本文主要關(guān)注無人駕駛系統(tǒng)設(shè)計(jì)與運(yùn)行部署階段的安全性與獎(jiǎng)勵(lì)函數(shù)設(shè)置的可解釋性，具體研究無人駕駛車輛在時(shí)間空間同步約束系統(tǒng)中不發(fā)生時(shí)空重疊(no spatio-clock overlaps)以及形式化規(guī)約制導(dǎo)的安全強(qiáng)化學(xué)習(xí)方法(formal specification guided safeRL).

近期的研究工作顯示無人駕駛系統(tǒng)已經(jīng)廣泛采用時(shí)間空間約束的形式化規(guī)約和強(qiáng)化學(xué)習(xí)相關(guān)技術(shù).在無人駕駛領(lǐng)域空間建模方面，協(xié)同無人駕駛系統(tǒng)安全性需要采用專用的領(lǐng)域特定的空間邏輯來描述車輛的物理空間位置和邏輯空間關(guān)系[13-14].無人駕駛系統(tǒng)包含連續(xù)狀態(tài)變化和離散狀態(tài)遷移，無人車變道控制器可以用來保證空間位置不發(fā)生重疊[15-16].在無人駕駛領(lǐng)域時(shí)間建模方面，時(shí)間自動(dòng)機(jī)被用來建模通信無人駕駛車輛之間的行為[17]，時(shí)鐘約束規(guī)約語言(clock constraint specification language, CCSL)被用來建模系統(tǒng)的安全約束[18-19].時(shí)空同步約束系統(tǒng)中的事件觸發(fā)不僅受嚴(yán)格的時(shí)序和物理時(shí)間的約束，同時(shí)還要邏輯和物理空間關(guān)系的約束[20-21].無人駕駛決策系統(tǒng)的核心問題是如何安全高效地分配路權(quán)來解決可能的時(shí)空重疊.無人駕駛行為需要在滿足時(shí)間約束的同時(shí)滿足空間關(guān)系的約束，反之亦然，這種方法可以保證在某一時(shí)刻和空間位置，只允許最多一輛車存在.時(shí)空安全攸關(guān)的事件包括安全衛(wèi)士和不變式規(guī)約，需要滿足邏輯時(shí)序和物理時(shí)鐘關(guān)系，同時(shí)需要滿足邏輯空間關(guān)系和物理空間位置.然而在無人駕駛領(lǐng)域，現(xiàn)有的時(shí)空同步約束規(guī)約方法和驗(yàn)證技術(shù)是不充分的.

無人駕駛系統(tǒng)是一類典型的信息物理系統(tǒng)(cyber-physical systems, CPS)，高保真的物理模型開發(fā)成本很高并且難以驗(yàn)證.隨著計(jì)算能力的提高和可用交通數(shù)據(jù)的增加，越來越多的數(shù)據(jù)驅(qū)動(dòng)的機(jī)器學(xué)習(xí)技術(shù)可以用來解決無人系統(tǒng)的智能決策.基于強(qiáng)化學(xué)習(xí)的無人駕駛基本思想是智能體(agent)直接與環(huán)境(environment)之間不斷試錯(cuò)，通過不斷的交互，從環(huán)境中尋求最優(yōu)策略(optimal policy)，智能體會(huì)接收到環(huán)境發(fā)來的獎(jiǎng)勵(lì)(reward)，強(qiáng)化學(xué)習(xí)的目標(biāo)就是通過改進(jìn)策略以期獲得最大化累計(jì)獎(jiǎng)勵(lì)(maximize cumulative future rewards)[22-23].安全強(qiáng)化學(xué)習(xí)(safeRL)是指在學(xué)習(xí)訓(xùn)練和執(zhí)行過程中，學(xué)習(xí)最優(yōu)策略的過程需要滿足嚴(yán)格的形式化安全約束[24-25].目前強(qiáng)化學(xué)習(xí)多數(shù)應(yīng)用在模擬環(huán)境中，沒有大規(guī)模被應(yīng)用在實(shí)車訓(xùn)練和實(shí)踐中，主要是用于2個(gè)原因：1)由于強(qiáng)化學(xué)習(xí)的狀態(tài)空間和動(dòng)作空間輸入來自黑盒的卷積神經(jīng)網(wǎng)絡(luò)和全連接神經(jīng)網(wǎng)絡(luò)，缺乏可解釋性成為深度強(qiáng)化學(xué)習(xí)部署到現(xiàn)實(shí)系統(tǒng)的主要障礙之一；2)由于面對(duì)新的沒有訓(xùn)練過的交通場景，強(qiáng)化學(xué)習(xí)不能為安全攸關(guān)的無人駕駛系統(tǒng)提供嚴(yán)格的安全約束和負(fù)責(zé)任的規(guī)則約束.

針對(duì)上述面向無人駕駛安全的智能決策方法研究現(xiàn)狀和存在的研究問題，本文主要關(guān)注無人駕駛領(lǐng)域?qū)Ｓ玫臅r(shí)空同步約束規(guī)約語言和時(shí)空同步行為描述自動(dòng)機(jī)，并將形式化時(shí)空同步安全約束的強(qiáng)化學(xué)習(xí)用于無人駕駛決策模塊，結(jié)合時(shí)空安全約束的強(qiáng)化學(xué)習(xí)來增強(qiáng)系統(tǒng)的安全性.主要研究貢獻(xiàn)有5個(gè)方面:

1)給出了時(shí)空同步約束系統(tǒng)的架構(gòu)，并給出了無人駕駛領(lǐng)域相關(guān)的時(shí)空同步約束安全域和交通快照的定義;

2)提出了面向無人駕駛領(lǐng)域的時(shí)空同步約束規(guī)約語言(spatio-clock synchronous constraint speci-fication language, SCSL)，該高層抽象規(guī)約語言可以處理時(shí)空同步約束的安全衛(wèi)士條件和不變式，并且提出了強(qiáng)化學(xué)習(xí)獎(jiǎng)勵(lì)函數(shù)設(shè)置可解釋性的方法;

3)設(shè)計(jì)了無人駕駛領(lǐng)域的時(shí)空同步約束自動(dòng)機(jī)(domain-specific spatio-clock synchronous constraint automata)，系統(tǒng)設(shè)計(jì)者可以用該自動(dòng)機(jī)描述無人駕駛行為和狀態(tài)-動(dòng)作空間遷移系統(tǒng)，這種方法為無人駕駛系統(tǒng)與環(huán)境之間的正確交互提供了安全保障和邏輯基礎(chǔ)，為強(qiáng)化學(xué)習(xí)狀態(tài)行為策略的生成提供了安全保障;

4)提出了安全強(qiáng)化學(xué)習(xí)的方法框架，定義了時(shí)空同步約束獎(jiǎng)勵(lì)狀態(tài)機(jī)，描述了非Markov性質(zhì)的獎(jiǎng)勵(lì)函數(shù)結(jié)構(gòu)，提供了任務(wù)目標(biāo)和獎(jiǎng)勵(lì)函數(shù)之間的映射關(guān)系，指導(dǎo)非Markov性質(zhì)獎(jiǎng)勵(lì)函數(shù)的設(shè)置;

5)設(shè)計(jì)了無人駕駛汽車在高速公路變道超車的案例，在無人駕駛仿真環(huán)境SUMO中模擬實(shí)驗(yàn)展示本文所提方法的有效性.

1 研究基礎(chǔ)

1.1 面向無人駕駛系統(tǒng)的強(qiáng)化學(xué)習(xí)架構(gòu)

無人駕駛系統(tǒng)(autonomous driving systems)相當(dāng)于強(qiáng)化學(xué)習(xí)系統(tǒng)中的智能體，集成了感知模塊(perception module)、決策模塊(decision-making module)、控制模塊(control module)等智能功能，其中決策模塊綜合環(huán)境感知信息和自車(ego vehicle)信息，經(jīng)過多次訓(xùn)練，利用強(qiáng)化學(xué)習(xí)可以實(shí)現(xiàn)模仿人類考駕照的類似人類駕駛行為，如圖1所示.環(huán)境感知模塊的主要功能是通過感知器和車輛通信獲取強(qiáng)化學(xué)習(xí)的狀態(tài)空間和動(dòng)作空間輸入信息，感知器主要包括傳感器、激光、雷達(dá)和攝像機(jī)等，車輛通信主要包括車與車(vehicle to vehicle, V2V)、車輛與道路基礎(chǔ)設(shè)施(vehicle to infrastructure, V2I)以及全球定位系統(tǒng)(global position system, GPS)等.決策模塊是無人駕駛系統(tǒng)的軟件模塊，該模塊提取出軟件模塊的輸入信息，也就是高層抽象的場景理解信息，智能體通過形式化約束制導(dǎo)的安全強(qiáng)化學(xué)習(xí)，輸出符合任務(wù)要求的最優(yōu)策略；智能體軟件模塊經(jīng)過學(xué)習(xí)與函數(shù)映射關(guān)系，輸出可執(zhí)行的行為決策信息給智能體執(zhí)行模塊，動(dòng)作控制信息包括縱向運(yùn)動(dòng)的加速和減速等規(guī)劃動(dòng)作，以變道、超車、轉(zhuǎn)向等橫向運(yùn)動(dòng)規(guī)劃信息.智能體的決策能力是實(shí)現(xiàn)車輛全自動(dòng)化的基本要素，目前大量的研究采用強(qiáng)化學(xué)習(xí)來實(shí)施無人自主決策[26-29]，綜合周圍交通環(huán)境和自車信息，產(chǎn)生安全通明安全的駕駛行為.在無人駕駛應(yīng)用中，無人車做動(dòng)作或者做決策，強(qiáng)化學(xué)習(xí)中的智能體就是無人車；而環(huán)境是與無人車交互的對(duì)象，無人車所處的真實(shí)交通物理世界就是環(huán)境，包括交互過程中的道路信息、交通標(biāo)志、交通規(guī)則、駕駛經(jīng)驗(yàn)等規(guī)則和推理機(jī)制.動(dòng)作空間是決策模塊輸出給執(zhí)行模塊的行為決策信息，獎(jiǎng)勵(lì)表示交通環(huán)境對(duì)智能體基于當(dāng)前狀態(tài)產(chǎn)生動(dòng)作的打分，需要系統(tǒng)設(shè)計(jì)人員設(shè)計(jì)獎(jiǎng)勵(lì)函數(shù)，本文主要針對(duì)如何獲得非Markov性質(zhì)的安全可解釋獎(jiǎng)勵(lì)函數(shù)的設(shè)置展開研究.

Fig.1 The RL architecture for autonomous driving systems

1.2 雙重深度Q學(xué)習(xí)網(wǎng)絡(luò)

貝爾曼方程式(1)和式(2)表示狀態(tài)價(jià)值函數(shù)和動(dòng)作價(jià)值函數(shù)之間的關(guān)系，也稱為貝爾曼期望方程(Bellman expectation equations):

(1)

Qπ(st,at)=R(st,at)+

(2)

(3)

訓(xùn)練雙重深度Q學(xué)習(xí)網(wǎng)絡(luò)(double deep Q-learning network, DDQN)常用的算法是時(shí)序差分算法(tem-poral difference, TD).假設(shè)有一個(gè)模型Q(s,a;w)，w是模型訓(xùn)練的參數(shù)，給定一個(gè)四元組(st,at,rt,st+1)，可推導(dǎo)出折扣回報(bào)為Gt=Rt+γGt+1，根據(jù)式(3)，當(dāng)智能體執(zhí)行動(dòng)作at后，環(huán)境通過狀態(tài)轉(zhuǎn)移概率pr(st+1|st,at)可以計(jì)算出下一時(shí)刻的新狀態(tài)st+1，而第t時(shí)刻的獎(jiǎng)勵(lì)最多只依賴于隨機(jī)變量St,At,St+1，現(xiàn)在已經(jīng)觀測到了st,at,st+1，則可得變量Rt的觀測值，記作rt，接著可以對(duì)期望做蒙特卡洛近似，可得：

(4)

損失函數(shù)關(guān)于參數(shù)w的梯度為

(5)

算法1.DDQN求解最優(yōu)動(dòng)作價(jià)值算法.

① 初始化動(dòng)作價(jià)值函數(shù)Qi(s,a;wi),

i∈{0,1};

② for eachepisode

/*每個(gè)回合時(shí)序差分學(xué)習(xí)*/

③ 狀態(tài)st和動(dòng)作at采樣，進(jìn)行時(shí)序差分

更新;

④ while(episode

⑤ 選擇最優(yōu)動(dòng)作a*,a*=

⑥ 進(jìn)入到下一個(gè)狀態(tài)st+1并且返回獎(jiǎng)勵(lì)rt;

a*;w1);

⑧ 計(jì)算TD-error,δt=Q0(st,at;w0)-

(rt+γQ1(st+1,a*;w1));

⑨ 更新DDQN參數(shù)w0和w1;

1.3 時(shí)鐘約束規(guī)約語言和空間邏輯

時(shí)鐘約束規(guī)約語言是基于時(shí)鐘和時(shí)鐘約束的形式化規(guī)約語言，時(shí)鐘表示一個(gè)信號(hào)在每個(gè)離散時(shí)間點(diǎn)的觸發(fā)狀態(tài)；時(shí)鐘約束描述信號(hào)時(shí)鐘之間的邏輯關(guān)系.下面給出邏輯時(shí)鐘、時(shí)鐘調(diào)度和時(shí)鐘歷史的相關(guān)定義[30].

定義2.時(shí)鐘調(diào)度.一個(gè)時(shí)鐘調(diào)度σ反映了所有時(shí)鐘在離散時(shí)間每個(gè)時(shí)刻的觸發(fā)狀態(tài)，是一個(gè)有限或者無限的序列σ(0)σ(1)…σ(i)…,i∈，為0和正整數(shù)的集合.σ(i)∈2c表示在時(shí)刻i觸發(fā)的時(shí)鐘集合，形式化定義為

定義3.時(shí)鐘歷史.對(duì)于給定的時(shí)鐘調(diào)度σ，時(shí)鐘歷史記錄了在σ中每一個(gè)時(shí)鐘截止到當(dāng)前時(shí)刻的觸發(fā)次數(shù)，形式化定義為

Hσ(c,i)=|{j|j∈+,j≤i,c∈σ(j)}|=

基于上述定義，下面展示6種最基本的時(shí)鐘關(guān)系的語法和語義，分別是優(yōu)先關(guān)系(precedence)、互斥關(guān)系(exclusion)、子時(shí)鐘關(guān)系(subclock)、同時(shí)關(guān)系(coincidence)、因果關(guān)系(causality)和交替關(guān)系(alternation).時(shí)鐘關(guān)系包括邏輯時(shí)鐘和二元連接操作符.時(shí)鐘關(guān)系的語法定義如下，Rel∷=c1c2|c1#c2|c1?c2|c1≡c2|c1～c2|c1?c2，時(shí)鐘關(guān)系的形式化語義見表1.

Table 1 The Formal Semantics of Clock Relations

優(yōu)先關(guān)系c1c2表示時(shí)鐘c1的觸發(fā)快于時(shí)鐘c2的觸發(fā).互斥關(guān)系c1#c2表示若時(shí)鐘c1觸發(fā)，則時(shí)鐘c2不觸發(fā)，反之亦然.子時(shí)種關(guān)系c1?c2表示在任意時(shí)刻，若時(shí)鐘c1觸發(fā).則時(shí)鐘c2必然觸發(fā).同時(shí)關(guān)系c1≡c2表示時(shí)鐘c1和時(shí)鐘c2同時(shí)觸發(fā).因果關(guān)系c1?c2表示時(shí)鐘c1的觸發(fā)不慢于時(shí)鐘c2的觸發(fā).交替關(guān)系c1～c2表示時(shí)鐘c1和時(shí)鐘c2交替觸發(fā).

時(shí)空狀態(tài)遷移表示空間關(guān)系隨著時(shí)刻變化的而不斷演化.區(qū)域連接演算(region connection calculus, RCC)主要用來描述空間區(qū)域間拓?fù)潢P(guān)系，該空間描述邏輯是Randell等人[31]在Clarke[32]的空間演算邏輯公理的基礎(chǔ)上提出的，將區(qū)域連接邏輯應(yīng)用在無人駕駛系統(tǒng)時(shí)空同步規(guī)約中，可以用來描述無人駕駛車輛間的空間邏輯關(guān)系.

無人駕駛車輛之間可以通信并且決定什么時(shí)間怎樣做出決策，并且安全的無人駕駛系統(tǒng)需要具備可以解釋的決策行為.這些決策可以幫助選擇適合的行為并且能預(yù)測危險(xiǎn)行為，無人系統(tǒng)決策涉及到安全攸關(guān)的時(shí)間和空間關(guān)系建模.系統(tǒng)行為可以描述為時(shí)鐘關(guān)系隨著空間變化而不斷同步演化，文章給出了時(shí)空同步約束系統(tǒng)的抽象架構(gòu)，如圖2所示.假設(shè)在時(shí)刻ti處，對(duì)于2種空間區(qū)域x1和x2，存在一種2個(gè)空間區(qū)域相離的空間關(guān)系DC(x1,x2)；在另外時(shí)刻tj處，存在另外一種空間區(qū)域外部相切的空間關(guān)系EC(x1,x2)；而在時(shí)刻tk處，存在空間區(qū)域部分重疊的空間關(guān)系PO(x1,x2)，兩車占用的時(shí)空區(qū)域可能存在部分重疊的空間關(guān)系.對(duì)于無人駕駛車輛來說，空間區(qū)域相切和空間區(qū)域部分重疊是危險(xiǎn)的空間位置關(guān)系，需要在決策模塊提前避免發(fā)生碰撞的時(shí)空關(guān)系出現(xiàn).無人駕駛系統(tǒng)狀態(tài)和動(dòng)作遷移不僅伴隨著空間關(guān)系的變化，還伴隨著嚴(yán)格的時(shí)鐘關(guān)系的遷移.

Fig.2 An abstract architecture of spatio-clock synchronous constraint systems

2 時(shí)空同步約束規(guī)約語言

為了安全決策和實(shí)時(shí)時(shí)空邏輯推理，本文給出無人駕駛交通快照、無人駕駛時(shí)空包絡(luò)、和特定領(lǐng)域?qū)Ｓ玫臅r(shí)空同步約束規(guī)約語言的定義.

定義5.無人駕駛交通快照(traffic snapshot).無人駕駛交通快照可以描述為七元組TS=(res,clm,posx,posy,spd,acc,td)，其中每一個(gè)元素分別代表無人駕駛系統(tǒng)相關(guān)的函數(shù).

1)res:→P()，車輛標(biāo)識(shí)符I∈，res(I)?表示車輛I占用的道路編號(hào)集合；

2)clm:→P()，車輛標(biāo)識(shí)符I∈，clm(I)?表示車輛I申請(qǐng)占用的道路編號(hào)集合；

3)posx:→，車輛標(biāo)識(shí)符I∈，posx(I)表示車輛在占用道路或者申請(qǐng)道路上的縱向位置信息；

4)posy:→，車輛標(biāo)識(shí)符I∈，posy(I)表示車輛在占用道路或者申請(qǐng)道路上的橫向位置信息；

5)spd:→，車輛標(biāo)識(shí)符I∈，spd(I)表示車輛的縱向速度信息；

6)acc:→，車輛標(biāo)識(shí)符I∈，acc(I)表示車輛的縱向加速度信息；

7)td∈{-1,0,1}表示車輛的駕駛方向，分別表示車輛右轉(zhuǎn)、直行和左轉(zhuǎn).

定義6.無人駕駛時(shí)空包絡(luò)(spatio-clock envelope).對(duì)于任意車輛I∈和交通快照TS，無人駕駛時(shí)空包絡(luò)可定義為SCE=(pid,bd,L,I,Vx,Vy)clk，其中pid∈是提前規(guī)定的最小距離(prescribed interval distance)，包含了車輛的長度和規(guī)定的最小安全距離；bd∈表示剎車距離(braking distance)，描述了車輛從開始剎車到最終停止的距離，對(duì)于自車車輛ego和剎車時(shí)間t，定義剎車距離為

加速度acc:→，安全距離(safety distance)是剎車距離加規(guī)定間隔距離sd=bd+pid.L=[l,n]?表示時(shí)空安全包絡(luò)包含的車道編號(hào)集合.

Vx=[pos(I)-h,pos(I)+h]?和Vy=[0,w]?分別表示在時(shí)刻clk和位置(posx,posy)處，車輛所能觀測到的縱向區(qū)域和橫向區(qū)域.

定義7.時(shí)空同步約束規(guī)約語言.時(shí)空同步約束規(guī)約語言(spatio-clock synchronous constraint specification language, SCSL)的語法定義：

φSCSL∷=true|φ|φ1∧φ2|?v:φ1|u(l,t)=

v(l′,t)|re(A)(l,t)|cl(A)(l,t)|e(l,t)(l′,δ)|

3 時(shí)空同步約束自動(dòng)機(jī)和時(shí)空遷移條件

基于第2節(jié)提出的領(lǐng)域特定的時(shí)空規(guī)約語言，本節(jié)給出系統(tǒng)行為建模語言，即時(shí)空同步自動(dòng)機(jī)(spatio-clock synchronous automata, SCSA)，然后給出無人駕駛行為的轉(zhuǎn)換條件，以及時(shí)空安全攸關(guān)轉(zhuǎn)換系統(tǒng)的衛(wèi)士條件和不變式.

定義8.時(shí)間空間同步約束自動(dòng)機(jī).該模型語法定義為七元組SCSA=(Q,q0,Σ,Varb,E,Grd,Inv)，其中:

1)Q是系統(tǒng)狀態(tài)的集合，每一個(gè)狀態(tài)可以看作是系統(tǒng)控制圖中的一個(gè)頂點(diǎn)；

2)q0是系統(tǒng)的初始狀態(tài)；

3)Σ是無人駕駛控制動(dòng)作的集合；

4)Varb是系統(tǒng)變量的集合，有4類變量，分別是離散變量dVar，連續(xù)變量ctVar，時(shí)鐘變量ckVar，和空間位置變量sVar；

5)E?Q×Grd×Σ×2Varb×Q是控制圖中連接狀態(tài)之間邊的集合，E代表遷移關(guān)系；

6)Grd代表遷移衛(wèi)士條件，Σ代表遷移動(dòng)作，2Varb需要重置的變量；

7)Inv:Q→ψ(Varb)表示關(guān)于變量的不變式.

時(shí)空同步約束自動(dòng)機(jī)中的狀態(tài)Q=(n,v,clk,sp)包括狀態(tài)名稱n，變量名稱v，時(shí)鐘以及時(shí)鐘關(guān)系clk，和空間位置及其關(guān)系sp.對(duì)于遷移關(guān)系中的環(huán)境標(biāo)簽λ，觸發(fā)事件evt(λ)，衛(wèi)士條件grd(λ)，和遷移動(dòng)作act(λ)，

表示當(dāng)觀測到觸發(fā)事件evt(λ)，遷移衛(wèi)士條件grd(λ)滿足，那么遷移動(dòng)作act(λ)將會(huì)被執(zhí)行.

Fig.3 An example of spatio-clock synchronous controller

定義9.無人駕駛控制器動(dòng)作.無人駕駛控制器動(dòng)作(autonomous controller action,ACA)可以定義為ACA∷=c(A,ψL)|wdc(A)|r(A)|wdr(A,ψL)|τ，其中ψL∷=n|l1|l1+l2|l1-l2，n∈,l1,l2∈LVar，c(A,l)表示車輛A申請(qǐng)道路l.動(dòng)作wdc(A)表示車輛A撤銷申請(qǐng)的道路.動(dòng)作r(A)表示車輛A占用之前申請(qǐng)的道路.動(dòng)作wdr(A,l)表示車輛A撤銷占用除了道路編號(hào)l以外的道路.τ表示空動(dòng)作，允許沒有任何動(dòng)作的交通遷移.

結(jié)合定義8和定義9，給出時(shí)空同步自動(dòng)機(jī)操作語義和控制器動(dòng)作的例子，如圖3所示.初始狀態(tài)Initial，狀態(tài)q1是碰撞檢測狀態(tài)ReserveOverlap-Check，當(dāng)接收到前方車輛同意超車Agreement信號(hào)，并且所有相關(guān)車輛和當(dāng)前車輛都不存在可能碰撞時(shí)，即?c,roc(ego,c)==false，并且申請(qǐng)道路在道路線標(biāo)號(hào)范圍內(nèi)n+1≤N，狀態(tài)遷移觸發(fā)事件滿足，衛(wèi)士條件也滿足，需要執(zhí)行遷移動(dòng)作，重置時(shí)鐘變量x，并且執(zhí)行申請(qǐng)臨近道路動(dòng)作c(ego,n+1)，接下來狀態(tài)從q1遷移到潛在碰撞檢測狀態(tài)q2，即申請(qǐng)道路空間重疊檢測ClaimOverlapCheck.在狀態(tài)q2，如果車輛接收到拒絕信號(hào)Decline，或者存在潛在碰撞的車輛，即滿足?c,coc(ego,c)==true，則需要重置時(shí)鐘變量x，并且執(zhí)行撤銷申請(qǐng)道路的動(dòng)作wdc(ego).

下面給出時(shí)空同步遷移的定義.

定義10.時(shí)空同步遷移(spatio-clock synchronous transitions).對(duì)于任何車輛I∈，經(jīng)過時(shí)間t后，速度和縱向位置的演化遷移可以根據(jù)：

spd′,acc,td)∧?I∈:spd′=

(6)

對(duì)于任何車輛I∈和道路編號(hào)n∈，車輛可以申請(qǐng)鄰近道路n+1或者n-1，并且為了保證無人駕駛的安全性和負(fù)責(zé)任，車輛必須服從交通規(guī)則，例如在右側(cè)行駛的國家(比如美國、中國和除了英國、澳大利亞以及其他英國殖民地國家以外的大部分國家)，大部分國家只允許右側(cè)行駛，但是在超車時(shí)需要申請(qǐng)左側(cè)道路超車行駛，可以根據(jù)式(7)執(zhí)行申請(qǐng)道路遷移和式(8)執(zhí)行撤銷申請(qǐng)道路的遷移：

spd,acc,td′)∧(|clm(I)|=0)∧(|res(I)|=1)∧

(td′=1)∧({n+1,n-1}∩res(I)≠?)∧

(clm′=clm⊕{I{n}}),

(7)

posy,spd,acc,td′)∧(td′=0)∧

(clm′=clm⊕{I?}).

(8)

重載算子⊕含義如下，ξ⊕{vα}可得{vα}中所有的關(guān)系，并且加上除去第一個(gè)元素在關(guān)系{vα}中，同時(shí)也在關(guān)系ξ中的關(guān)系后的所有剩余ξ中的關(guān)系.

對(duì)于任何車輛I∈和道路編號(hào)n∈，根據(jù)式(9)車輛占用之前申請(qǐng)或者占用的道路編號(hào)，根據(jù)式(10)車輛也可以撤銷占用除了道路編號(hào)n以外的道路：

spd,acc,td)∧(clm′=clm⊕{I?})∧

(res′=res⊕{Ires(I)∪clm(I)}),

(9)

posy,spd,acc,td)∧(res′=res⊕{I{n}})∧

(n∈res(I)∧|res(I)|=2).

(10)

對(duì)于任何車輛I∈和加速度acc∈，加速度可以根據(jù)式(11)進(jìn)行演化:

spd,acc′,td)∧(acc′=acc⊕{Ia}).

(11)

4 時(shí)空同步約束制導(dǎo)的強(qiáng)化學(xué)習(xí)方法

4.1 時(shí)空同步約束系統(tǒng)的安全遷移條件

根據(jù)第3節(jié)介紹的時(shí)空同步自動(dòng)機(jī)和遷移條件，本節(jié)主要介紹無人駕駛安全衛(wèi)士條件和結(jié)合形式化時(shí)空同步約束的強(qiáng)化學(xué)習(xí)方法.提出滿足系統(tǒng)安全需求的獎(jiǎng)勵(lì)函數(shù)設(shè)置方法，重點(diǎn)關(guān)注時(shí)間空間同步約束的衛(wèi)士條件和不變式.

定義 11.無人駕駛安全衛(wèi)士(autonomous driving safety guards).根據(jù)定義4，時(shí)空安全衛(wèi)士條件(即不發(fā)生碰撞)表示為申請(qǐng)和占用時(shí)空區(qū)域不發(fā)生重疊，可以檢驗(yàn)安全性條件來確保沒有交通事故發(fā)生(前提是車輛之間的通信不會(huì)發(fā)生延遲，車輛的感知器和其他硬件不會(huì)發(fā)生故障等).

safetyOverlap(c1,c2)=(c1.posx≤c2.posx≤

c1.posx+c1.sd)∨(c1.posy≤c2.posy≤

c1.posy+c1.sdy)∨(c2.posx≤c1.posx≤

c2.posx+c2.sd)∨(c2.posy≤c1.posy≤

c2.posy+c2.sdy).

(12)

safetyOverlap(c1,c2)為真說明車輛c1和c2占用道路空間存在相交的區(qū)域.這時(shí)安全衛(wèi)士條件意味著任何兩輛車輛之間不存在相交的時(shí)空區(qū)域，可表示為

safe=?c1,c2:((c1=c2)∨(res(c1)∩

res(c2)=?)∨safetyOverlap(c1,c2)).

(13)

或者根據(jù)時(shí)空同步約束語言SCSL，可以形式化規(guī)約為

safe=?c1,c2:((c1=c2)∨(res(c1)∩res(c2)=

?)∨(re(c1)(l,t)∧re(c2)(l,t))).

(14)

占用時(shí)空重疊檢測(reservation overlap check)roc(c1,c2)用來阻止任意兩輛車占用重疊的時(shí)空區(qū)域,表示為

roc(c1,c2)=?c1,c2:((c1≠c2)∧(res(c1)∩

res(c2)≠?)∧safetyOverlap(c1,c2)).

(15)

根據(jù)時(shí)空同步約束語言SCSL，安全衛(wèi)士約束可以形式化規(guī)約為

roc(c1,c2)=?c1,c2:(re(c1)(l,t)∧

re(c2)(l,t)).

(16)

申請(qǐng)時(shí)空重疊檢測(claiming overlap check)coc(c1,c2)阻止任意兩輛車輛占用或者申請(qǐng)時(shí)空區(qū)域重疊.如果車輛c1想把申請(qǐng)信息轉(zhuǎn)換為占用道路信息并且安全地進(jìn)行換道，車輛c1需要檢查自身申請(qǐng)的時(shí)空區(qū)域與另外一輛車c2申請(qǐng)或者占用的道路空間是否有重疊，參照:

coc(c1,c2)=?c1,c2:((c1≠c2)∧((clm(c1)∩

res(c2)≠?)∨(clm(c1)∩clm(c2)≠?)∧

safeOverlap(c1,c2)).

(17)

根據(jù)時(shí)空同步約束語言SCSL，安全衛(wèi)士約束可以形式化規(guī)約為

coc(c1,c2)=?c1,c2:(cl(c1)(l,t)∧

(re(c2)(l,t)∨cl(c2)(l,t))).

(18)

4.2 形式化約束制導(dǎo)的安全強(qiáng)化學(xué)習(xí)框架

強(qiáng)化學(xué)習(xí)無法從環(huán)境交互的經(jīng)驗(yàn)中學(xué)習(xí)到獎(jiǎng)勵(lì)函數(shù)，獎(jiǎng)勵(lì)函數(shù)必須由人工編寫，而編寫?yīng)剟?lì)函數(shù)具有2個(gè)挑戰(zhàn)：1)感知數(shù)據(jù)不能直接用于獎(jiǎng)勵(lì)函數(shù)的輸入?yún)?shù)(比如像素等)，系統(tǒng)需要對(duì)數(shù)據(jù)進(jìn)行抽象來獲得強(qiáng)化學(xué)習(xí)中的狀態(tài)空間和動(dòng)作空間；2)復(fù)雜的學(xué)習(xí)任務(wù)需要分解為多個(gè)子學(xué)習(xí)任務(wù)(sub-goal task)，子任務(wù)獎(jiǎng)勵(lì)不僅與當(dāng)前的狀態(tài)和動(dòng)作有關(guān)系，還與歷史狀態(tài)的狀態(tài)和動(dòng)作有關(guān)，本文稱為非Markov性質(zhì)的獎(jiǎng)勵(lì)，所以系統(tǒng)設(shè)計(jì)人員需要對(duì)子學(xué)習(xí)任務(wù)的時(shí)序關(guān)系進(jìn)行嚴(yán)格的形式化約束，否則不能達(dá)到安全累計(jì)回報(bào)的最優(yōu)值.為了解決上述問題，需要構(gòu)建一個(gè)面向特定領(lǐng)域的狀態(tài)-動(dòng)作空間詞匯表,本文給出將智能體學(xué)習(xí)經(jīng)驗(yàn)(s,a,s′)與狀態(tài)-動(dòng)作空間詞匯聯(lián)系起來的命題標(biāo)簽函數(shù)的定義.

該標(biāo)簽函數(shù)標(biāo)注了強(qiáng)化學(xué)習(xí)中狀態(tài)和動(dòng)作的系統(tǒng)遷移，首先本文給出無人駕駛系統(tǒng)相關(guān)的狀態(tài)空間和動(dòng)作空間的抽象描述.狀態(tài)空間可以描述為

S=(numlane,numveh,idveh,rlid,clid,vr,ar,vid,

其中，numlane是道路的數(shù)量,numveh是安全區(qū)域內(nèi)車輛的數(shù)量，idveh表示車輛的標(biāo)識(shí)符，rlid表示車輛占用的道路編號(hào)集合，clid表示車輛申請(qǐng)的道路編號(hào)集合，vr表示車輛的速度區(qū)間[vmin,vmax]，ar表示車輛的加速度區(qū)間[amin,amax]，vid表示車輛id的速度，aid表示車輛的加速度，posx表示車輛的縱向位置，posy表示車輛的橫向位置，ddid表示車輛的駕駛方向，llid表示道路的長度，wlid表示道路的寬度，pdx表示兩車縱向最小間隔，pdy表示橫向最小間隔.動(dòng)作空間為

A=(cl_left,cl_right,wd_cl,res,wd_res,

keep_lane,brake,hard_brake,acc,

其中，cl_left表示申請(qǐng)左轉(zhuǎn)，cl_right表示申請(qǐng)右轉(zhuǎn)，wd_cl表示不滿足申請(qǐng)條件時(shí)撤銷申請(qǐng)，res表示占用道路(r(I))，wd_res表示撤銷道路占用(wdr(I,n))，keep_lane表示保持當(dāng)前道路，brake表示剎車減速，hard_brake表示遇到緊急情況時(shí)緊急剎車，acc表示加速行駛，maintain表示保持當(dāng)前速度行駛，roc表示占用道路時(shí)空重疊檢測(roc(c1,c2))，coc表示申請(qǐng)道路時(shí)空重疊檢測(coc(c1,c2))，overtake表示超車.

Fig.4 The research framework ofsafeRL approach

為了保證安全累計(jì)回報(bào)的最大化，需要規(guī)定智能體獲得獎(jiǎng)勵(lì)函數(shù)的時(shí)空同步約束條件，對(duì)于復(fù)雜的強(qiáng)化學(xué)習(xí)任務(wù)，各個(gè)子學(xué)習(xí)任務(wù)之間存在條件、循環(huán)和否定等時(shí)空約束關(guān)系，系統(tǒng)獎(jiǎng)勵(lì)不僅僅依賴Markov獎(jiǎng)勵(lì)決策過程，還受時(shí)空同步公式的約束，只有滿足時(shí)空同步約束的動(dòng)作才可以獲得相應(yīng)的獎(jiǎng)勵(lì)，記為rt:(s1,a1)(s2,a2)…(st,at)φ，也就是系統(tǒng)的歷史經(jīng)驗(yàn)滿足邏輯公式φ(φ是關(guān)于命題集合的時(shí)空同步約束公式)時(shí)，系統(tǒng)才能獲得獎(jiǎng)勵(lì).也可以理解為狀態(tài)-動(dòng)作空間遷移系統(tǒng)滿足公式φ.下面給出時(shí)空同步約束的獎(jiǎng)勵(lì)函數(shù)狀態(tài)機(jī)的定義，該狀態(tài)機(jī)對(duì)應(yīng)著完成相應(yīng)任務(wù)時(shí)的形式化時(shí)空同步邏輯規(guī)約公式，從而解決了非Markov決策過程的獎(jiǎng)勵(lì)函數(shù)設(shè)置問題.

定義13.時(shí)空同步約束獎(jiǎng)勵(lì)狀態(tài)機(jī)(spatio-clock synchronous constraint reward machine, SCSRM)[11].時(shí)空同步約束獎(jiǎng)勵(lì)狀態(tài)機(jī)可以定義為九元組SCSRM給定非Markov決策過程中的元素命題符號(hào)集合系統(tǒng)狀態(tài)集合以及動(dòng)作集合狀態(tài)-動(dòng)作空間遷移系統(tǒng)是該狀態(tài)機(jī)中的狀態(tài)集合；u0是該狀態(tài)機(jī)的初始狀態(tài)；表示系統(tǒng)可以接收的輸入狀態(tài)和動(dòng)作信息；狀態(tài)機(jī)的狀態(tài)轉(zhuǎn)移函數(shù)表示在狀態(tài)ut∈U時(shí)，滿足標(biāo)簽遷移命題邏輯公式時(shí)，系統(tǒng)狀態(tài)發(fā)生遷移，即狀態(tài)機(jī)的獎(jiǎng)勵(lì)函數(shù)δr:U×U→[(S×A)+×S→]表示在遷移關(guān)系中，時(shí)空同步約束狀態(tài)機(jī)為非Markov獎(jiǎng)勵(lì)函數(shù)，即根據(jù)定義，該獎(jiǎng)勵(lì)是從獎(jiǎng)勵(lì)狀態(tài)機(jī)的初始狀態(tài)到當(dāng)前狀態(tài)的滿足邏輯公式φ的獎(jiǎng)勵(lì)之和.

算法2.safe_DDQN求解最優(yōu)動(dòng)作價(jià)值算法.

輸出：形式化約束制導(dǎo)的動(dòng)作價(jià)值估計(jì).

② fort=0 toTdo

/*回合數(shù)內(nèi)迭代尋找最優(yōu)價(jià)值*/

③ 選擇子學(xué)習(xí)任務(wù)i←subtask(SCSRM,t);

⑤ while(episode

⑥ 進(jìn)入到下一個(gè)狀態(tài)st+1并且返回獎(jiǎng)勵(lì)rt;

⑧ 更新時(shí)空同步約束獎(jiǎng)勵(lì)狀態(tài)機(jī)狀態(tài);

⑨ 更新時(shí)空同步約束獎(jiǎng)勵(lì)狀態(tài)機(jī)獎(jiǎng)勵(lì);

⑩ ifst+1是終止?fàn)顟B(tài) then

/*當(dāng)前價(jià)值為獎(jiǎng)勵(lì)*/

/*更新價(jià)值，執(zhí)行新的動(dòng)作*/

/*策略梯度下降更新w*/

at←at+1;/*狀態(tài)機(jī)、狀態(tài)和動(dòng)作的

更新*/

算法2在提高安全性的同時(shí)，比算法1多了一層for循環(huán)，算法嵌套的循環(huán)迭代次數(shù)增加了，因此算法復(fù)雜度提高為O(n3)，而算法1的算法復(fù)雜度是O(n2)，原因是為了滿足非Markov性質(zhì)的獎(jiǎng)勵(lì)，需要構(gòu)建時(shí)空同步約束的獎(jiǎng)勵(lì)狀態(tài)機(jī)，然后在形式化約束制導(dǎo)的獎(jiǎng)勵(lì)狀態(tài)機(jī)里面選擇子學(xué)習(xí)任務(wù)，用來在回合數(shù)規(guī)定內(nèi)獲得子學(xué)習(xí)任務(wù)滿足形式化時(shí)空同步規(guī)約的最優(yōu)動(dòng)作價(jià)值，導(dǎo)致了算法復(fù)雜度的增加.同時(shí)，形式化時(shí)空同步約束制導(dǎo)的強(qiáng)化學(xué)習(xí)融合了安全規(guī)則和先驗(yàn)經(jīng)驗(yàn)等安全約束，智能體將不會(huì)去探索或者試錯(cuò)不正確的動(dòng)作策略，在相對(duì)較少的訓(xùn)練次數(shù)內(nèi)獲得較好的獎(jiǎng)勵(lì)，所以加快了深度強(qiáng)化學(xué)習(xí)的效率，提高了算法的收斂速度.

對(duì)于無人駕駛系統(tǒng)，系統(tǒng)設(shè)計(jì)者希望車輛能夠安全高效地行駛，同時(shí)車輛還需要遵守交通規(guī)則，所以考慮回報(bào)獎(jiǎng)勵(lì)函數(shù)時(shí)，需要綜合考慮以下3個(gè)方面：1)車輛發(fā)生碰撞或者違反交通規(guī)則，假如獎(jiǎng)勵(lì)為-2；2)如果車輛速度太慢，導(dǎo)致通行效率太低，假如速度小于2 m/s，則獎(jiǎng)勵(lì)為0；3)計(jì)算安全距離(safety distance)，并設(shè)計(jì)獎(jiǎng)勵(lì)函數(shù).同時(shí)需要限制訓(xùn)練回合的時(shí)間，因?yàn)樵谟?xùn)練過程中，可能會(huì)出現(xiàn)車輛在某一個(gè)范圍內(nèi)轉(zhuǎn)圈，需要限制回合時(shí)間，使得車輛進(jìn)入后續(xù)回合的訓(xùn)練.基于回報(bào)獎(jiǎng)勵(lì)函數(shù)，可以設(shè)置回合時(shí)間，例如發(fā)生時(shí)空重疊或者違反交通規(guī)則；汽車速度小于最低速度；碰撞時(shí)間小于設(shè)定值等.

根據(jù)無人駕駛安全衛(wèi)士條件的形式化描述，文章提出了基于時(shí)空同步約束的安全強(qiáng)化學(xué)習(xí)方法.該方法的主要思想是是指在強(qiáng)化學(xué)習(xí)訓(xùn)練和執(zhí)行過程中，學(xué)習(xí)最優(yōu)策略的過程需要滿足形式化時(shí)空同步安全約束.系統(tǒng)很難及時(shí)預(yù)測前車的動(dòng)作策略，車輛碰撞可能發(fā)生在自車與前車的距離小于安全距離時(shí).基于這個(gè)原因，需要制定形式化安全距離約束來懲罰那些與前車距離小于安全距離的車輛.在定義6的基礎(chǔ)上，再增加一個(gè)反應(yīng)時(shí)間內(nèi)行駛的距離dre，跟馳車輛(following vehicle)的剎車距離[33]dstop_f表示跟馳車輛在反應(yīng)時(shí)間內(nèi)以最大加速度和最小剎車加速度行駛的距離，計(jì)算為

(19)

其中，vf表示跟馳車輛的速度，tre是車輛的反應(yīng)時(shí)間，amax,brake是車輛緊急剎車(hard brake)的最大剎車加速度，amax,acc是后面跟馳車輛在反應(yīng)時(shí)間內(nèi)的最大加速度，amin,brake是反應(yīng)時(shí)間過后前面車輛從開始剎車到車輛停止且前后兩輛車沒有發(fā)生碰撞的最小剎車加速度.

前面車輛(preceding vehicle)的剎車距離dstop_p表示車輛以初始速度vp行駛，最大制動(dòng)加速度amax,brake剎車時(shí)車輛行駛的距離，計(jì)算為

(20)

車輛之間的最小距離dmin是后車剎車距離dstop_f與規(guī)定間隔dpid之和，減去前車剎車距離dstop_p和兩車間隔dgap距離的和，車輛之間的距離必須滿足式(21)，才保證車輛不發(fā)生碰撞.

dmin=(dstop_f+dpid)-(dstop_p+dgap)>0，

(21)

其中，dpid是規(guī)定的車輛之間的安全間隔距離，dgap是兩車停止后的實(shí)際間隔距離.

違反安全距離的規(guī)定促使無人駕駛車輛在強(qiáng)化學(xué)習(xí)的過程中保持安全距離行駛.系統(tǒng)首先給出關(guān)于最小安全距離dmin的獎(jiǎng)勵(lì)反饋函數(shù)：

(22)

利用安全強(qiáng)化學(xué)習(xí)訓(xùn)練車輛的過程中，車輛的速度不要超過允許的最大速度，同時(shí)希望車輛能夠快速的到達(dá)目的地，所以系統(tǒng)設(shè)計(jì)人員需要設(shè)置關(guān)于訓(xùn)練車輛速度的獎(jiǎng)勵(lì)函數(shù)：

(23)

為了避免車輛偏離行駛車道撞向路邊基礎(chǔ)設(shè)施發(fā)生交通事故，本文設(shè)置車輛安全駕駛行為的正強(qiáng)化學(xué)習(xí)獎(jiǎng)勵(lì)函數(shù)，系統(tǒng)設(shè)計(jì)人員應(yīng)鼓勵(lì)車輛靠近路中間的道路行駛，用dispy_mid表示車輛的橫向位置與道路中間橫向位置的距離，為此設(shè)置車道保持的獎(jiǎng)勵(lì)函數(shù)：

Rlane=exp(-1.2×dispy_mid).

(24)

本文主要關(guān)注無人駕駛車輛強(qiáng)化學(xué)習(xí)智能體的安全性和通行效率，為此給出在時(shí)刻t的獎(jiǎng)勵(lì)函數(shù)：

(25)

5 案例分析

5.1 案例需求分析

系統(tǒng)的需求描述如圖5所示，當(dāng)前道路上的自車車輛有超車意圖時(shí)，首先需要打開轉(zhuǎn)向燈，提示在時(shí)空安全包絡(luò)內(nèi)的周圍車輛超車意圖，此時(shí)有3件安全關(guān)鍵的事情需要確認(rèn)：1)需要確認(rèn)與同車道的車輛是否在安全距離內(nèi)，也就是確認(rèn)是否存在占用空間重疊；2)安全包絡(luò)內(nèi)的周圍車輛觀測到變道信號(hào)后，后面車輛不能加速；3)向前面車輛發(fā)送變道超車請(qǐng)求信息.前方車輛preceding-vehicle在接收到超車請(qǐng)求信號(hào)后，需要在一定時(shí)間(反應(yīng)時(shí)間假設(shè)2 s)內(nèi)回復(fù)同意或者拒絕，如果自車車輛在反應(yīng)時(shí)間內(nèi)接收不到回復(fù)信息或者接收到拒絕信息，自車車輛不能實(shí)施變道超車，需要保持原來的狀態(tài)前進(jìn)；如果與周圍的申請(qǐng)道路車輛不滿足安全距離約束，也就是存在申請(qǐng)道路的空間重疊，同樣不能實(shí)施變道超車.需要同時(shí)滿足在約定的反應(yīng)時(shí)間內(nèi)接收到同意信息和滿足安全距離的情況下，才可以實(shí)施變道超車.超車動(dòng)作可以分解成2次變道，首先是第1次變道到申請(qǐng)的道路，變道之后需要加速前進(jìn)，在這個(gè)過程中，之前回復(fù)同意的車輛不能加速，當(dāng)自車車輛的相對(duì)空間位置超過自車車輛前方車輛時(shí)，并且它們之間滿足變道的安全距離時(shí)，自車車輛實(shí)施第2次變道，2次變道超車的時(shí)間間隔不能超過超車規(guī)定時(shí)間.

Fig.5 An example of autonomous lane-change and overtaking in highway scenario

Fig.6 Combine RL and SUMO simulation platform

建立時(shí)間空間同步自動(dòng)機(jī)理論模型包含3個(gè)步驟：1)車輛左轉(zhuǎn)信號(hào)Turn_left必須優(yōu)先變道申請(qǐng)Claiming_req，變道申請(qǐng)優(yōu)先于互斥的時(shí)鐘事件同意申請(qǐng)Change_claim_agr和不同意申請(qǐng)信號(hào)No_change_claim_agr，該需求形式化規(guī)約為CTurn_leftCClaiming_req(CChange_claim_agr#CNo_change_claim_agr).其次，當(dāng)前面車輛回復(fù)同意超車信號(hào)后，占用道路碰撞檢測roc(ego,c)嚴(yán)格優(yōu)先于占用道路動(dòng)作Reserving，而且占用道路動(dòng)作又嚴(yán)格優(yōu)先于前方車輛不能左轉(zhuǎn)信號(hào)No_turn_left，該需求可以形式化規(guī)約為roc(ego,c)CReservingCNo_turn_left.2)申請(qǐng)鄰近道路信號(hào)c(I,n)與撤銷申請(qǐng)信號(hào)交替發(fā)生wdc(I)，該需求形式化規(guī)約為c(I,n)～wdc(I)，同樣地，占用道路事件r(I)與撤銷占用道路事件wdr(I,n)交替發(fā)生，該需求形式化規(guī)約為r(I)～wdr(I,n).3)碰撞檢測時(shí)鐘roc(ego,c)的發(fā)生不慢于申請(qǐng)變道的時(shí)鐘Claiming_req，2個(gè)時(shí)鐘滿足因果關(guān)系，即roc(ego,c)?CClaiming_req，同樣地，潛在碰撞檢測coc(ego,c)觸發(fā)互斥時(shí)鐘占用之前申請(qǐng)的道路Reserving和存在潛在碰撞Potentialcol，該需求可以形式化規(guī)約為coc(ego,c)?(CReserving#CPotentialcol).

5.2 SUMO仿真平臺(tái)及實(shí)驗(yàn)設(shè)計(jì)分析

結(jié)合強(qiáng)化學(xué)習(xí)的SUMO仿真平臺(tái)是一個(gè)開源、微觀和連續(xù)的交通仿真軟件包，支持動(dòng)態(tài)路由的生成和輸入，擁有可視化的圖形界面，可以對(duì)時(shí)間和空間進(jìn)行良好的定義和模擬，利用TraCI接口(traffic control interface)實(shí)現(xiàn)用Python語言進(jìn)行模型開發(fā)與仿真，所以本文選擇了SUMO作為仿真驗(yàn)證工具，如圖6所示系統(tǒng)由3個(gè)部分組成：1)駕駛環(huán)境，該模塊路網(wǎng)文件(.net.xml)和路由文件(.rou.xml)，路網(wǎng)文件描述了交通道路信息，包括節(jié)點(diǎn)文件(.node.xml)和連接邊文件(.edge.xml)；路由文件定義車輛行為、行駛路徑和車流信息.2)TraCI接口，它作為仿真平臺(tái)和強(qiáng)化學(xué)習(xí)算法之間的接口，將仿真網(wǎng)絡(luò)里的觀測狀態(tài)信息傳遞給算法，而后又將算法輸出的高層動(dòng)作傳回給目標(biāo)車輛智能體.3)智能體模塊，借助TensorFlow庫開發(fā)的DDQN算法和改進(jìn)的safe_DDQN算法，實(shí)現(xiàn)智能體的智能安全決策.這里需要注意，DDQN和safe_DDQN算法只輸出高層控制動(dòng)作，而對(duì)目標(biāo)車輛的底層控制由SUMO模擬器實(shí)現(xiàn).對(duì)于道路信息，SUMO還可以通過netconvert程序?qū)⒑芏嗟牡谌降穆肪W(wǎng)文件轉(zhuǎn)化為SUMO可讀的文件，例如可以選定真實(shí)物理世界的osm格式的地圖文件，直接生成一個(gè)可以運(yùn)行仿真的SUMO路網(wǎng)文件；車輛的行為主要靠無人駕駛的感知模塊獲得，所以只要實(shí)際無人車系統(tǒng)的車輛感知系統(tǒng)滿足道路運(yùn)行測試條件的話，就可以將文中的方法部署在實(shí)際的無人駕駛車輛.

在SUMO中生成案例中的交通仿真場景如圖7所示，交通場景中包含3條道路，車輛信息由路由文件生成，圖7中的紅色車輛是需要強(qiáng)化學(xué)習(xí)訓(xùn)練的自車車輛，黃色車輛是交通駕駛環(huán)境視窗中的其他周圍車輛.

Fig.7 Overtaking scenario screenshot in SUMO platform

Fig.8 Experimental results and analyses

本文對(duì)2個(gè)算法分別進(jìn)行了500回合的深度強(qiáng)化學(xué)習(xí)訓(xùn)練，其中每一回合表示自車車輛完成了一次在規(guī)定道路上的駕駛行為，并對(duì)仿真結(jié)果進(jìn)行了比較.圖8(a)顯示了算法在每一回合訓(xùn)練中獲得的平均獎(jiǎng)勵(lì)，首先可以看到隨著訓(xùn)練回合數(shù)的增加，2個(gè)算法的平均獎(jiǎng)勵(lì)都在上升，但是safe_DDQN的平均獎(jiǎng)勵(lì)相比于普通的DDQN更高而且在較短的時(shí)間內(nèi)趨于穩(wěn)定，這也意味著本文提出的算法safe_DDQN更容易收斂.圖8(b)顯示了算法指導(dǎo)的智能車在每一回合訓(xùn)練中發(fā)生的總碰撞次數(shù)，在2個(gè)算法中，智能車的碰撞次數(shù)隨著訓(xùn)練回合數(shù)的增加而不斷減少，說明智能車通過探索強(qiáng)化學(xué)習(xí)學(xué)得了正確的駕駛動(dòng)作，減少了碰撞次數(shù)的發(fā)生，但是普通的DDQN算法不夠穩(wěn)定，在400回合后，仍有較高頻率的碰撞發(fā)生，而safe_DDNQ此時(shí)已經(jīng)幾乎不會(huì)發(fā)生碰撞.在實(shí)驗(yàn)中設(shè)置每一個(gè)回合進(jìn)行1 000時(shí)間步(timesteps)的狀態(tài)-動(dòng)作空間采樣，對(duì)應(yīng)算法1行③和算法2行④，根據(jù)算法描述，有時(shí)候遇到終止?fàn)顟B(tài)仿真會(huì)提前終止回合的迭代，500回合仿真大約有40萬時(shí)間步，為了方便觀察，每20個(gè)時(shí)間步選取一個(gè)數(shù)據(jù)，并繪制了如圖8(c)所示的智能體車輛的速度變化圖.從圖8中可以看到，safe_DDQN算法指導(dǎo)的智能車，在20萬時(shí)間步后，速度就趨于平穩(wěn)，且始終維持在目標(biāo)車速附近，而普通的DDQN算法指導(dǎo)的小車，速度波動(dòng)始終很大，這不僅會(huì)影響乘車舒適度，還會(huì)帶來安全隱患.由此可見，本文提出的safe_DDQN算法相比于普通的DDQN算法，在算法收斂速度、算法穩(wěn)定性，以及其指導(dǎo)的智能車所帶來的駕駛安全性、乘車舒適性方面都有較大的提高.

6 相關(guān)工作

首先介紹關(guān)于時(shí)間和空間形式化約束規(guī)約的相關(guān)工作.Chouhan等人[34]利用形式化時(shí)間自動(dòng)機(jī)模型和統(tǒng)計(jì)模型檢測方法，為啟發(fā)式無人駕駛交叉路口管理提供了相關(guān)的建模和驗(yàn)證技術(shù).Cuer等人[35]提出了從自然語言到形式化狀態(tài)機(jī)的建模架構(gòu)，并且不斷刪掉潛在的自然語言模糊性和不一致性.Briola等人[36]用本體來描述空間關(guān)系，并且用Prolog來規(guī)約可解釋的規(guī)則信息，方便系統(tǒng)設(shè)計(jì)者重復(fù)使用形式化的領(lǐng)域空間知識(shí).多道路空間邏輯(multi-lane spatial logic)被用來建模無人駕駛領(lǐng)域的道路知識(shí)，包括鄉(xiāng)村道路的應(yīng)用[37]、城市道路的應(yīng)用[13]和高速場景的應(yīng)用[38].無人駕駛時(shí)間行為建模方面，文章[39]設(shè)計(jì)了隨機(jī)混合時(shí)空規(guī)約語言和自動(dòng)機(jī)，并提出了無人駕駛車輛發(fā)生碰撞時(shí)刻和位置的預(yù)測方法.Tan等人[40]展示了空間時(shí)序事件建模的方法，該方法規(guī)約事件的觸發(fā)不僅根據(jù)嚴(yán)格的時(shí)序和物理時(shí)間，而且還受空間關(guān)系的制約.上述研究關(guān)注了空間或者時(shí)間的建模，但是對(duì)于時(shí)空同步約束的自動(dòng)駕駛系統(tǒng)來說，仍然缺乏領(lǐng)域相關(guān)的形式化規(guī)約語言，增強(qiáng)系統(tǒng)需求和任務(wù)的嚴(yán)格描述，減少自然語言的二義性，同時(shí)用來增強(qiáng)系統(tǒng)決策的安全性.

然后介紹結(jié)合安全約束的強(qiáng)化學(xué)習(xí)方法.對(duì)于安全攸關(guān)的無人駕駛系統(tǒng)，為了增強(qiáng)系統(tǒng)決策的安全性，結(jié)合形式化安全約束的強(qiáng)化學(xué)習(xí)技術(shù)得到越來越多的關(guān)注和研究.文獻(xiàn)[6,41]結(jié)合可解釋的基于規(guī)則的策略和黑盒的強(qiáng)化學(xué)習(xí)來實(shí)現(xiàn)系統(tǒng)的安全性和魯棒性.紀(jì)守領(lǐng)等人[42]回顧了機(jī)器學(xué)習(xí)中的可解釋性問題，分析了可解釋性機(jī)器學(xué)習(xí)的安全性面臨的挑戰(zhàn)和研究方向.Krasowski等人[43]通過擴(kuò)展強(qiáng)化學(xué)習(xí)安全層來限制動(dòng)作空間，利用基于集合的方法來增強(qiáng)強(qiáng)化學(xué)習(xí)的安全保障.Wachi等人[44]提出了一種帶約束Markov決策過程的強(qiáng)化學(xué)習(xí)方法，該方法通過擴(kuò)展安全區(qū)域來不斷學(xué)習(xí)安全約束.Gao等人[45]設(shè)計(jì)了一個(gè)結(jié)合形式化線性時(shí)序規(guī)約(linear temporal logic, LTL)的獎(jiǎng)勵(lì)回報(bào)函數(shù)，可以更準(zhǔn)確地估計(jì)損失函數(shù)的梯度和改善訓(xùn)練過程的穩(wěn)定性.Wolf等人[46]指出僅僅對(duì)專家知識(shí)進(jìn)行建模是比較困難的，提出結(jié)合語義狀態(tài)和交通規(guī)則來增強(qiáng)強(qiáng)化學(xué)習(xí)的安全性.Wang等人[47]在無人駕駛?cè)蝿?wù)決策方法中結(jié)合基于規(guī)則約束和強(qiáng)化學(xué)習(xí)的方法，實(shí)現(xiàn)了安全高效的變道行為.Chen等人[48]提出了一種基于經(jīng)驗(yàn)指導(dǎo)的深度學(xué)習(xí)多行動(dòng)者-評(píng)論家算法，從優(yōu)秀經(jīng)驗(yàn)中學(xué)習(xí)指導(dǎo)網(wǎng)絡(luò)，并對(duì)動(dòng)作價(jià)值函數(shù)進(jìn)行更新指導(dǎo).Garca和Fernández[49]給出了安全強(qiáng)化學(xué)習(xí)的定義，并給出在系統(tǒng)學(xué)習(xí)和部署的過程中增加安全約束的相關(guān)文獻(xiàn)綜述.

7 總結(jié)與展望

針對(duì)基于強(qiáng)化學(xué)習(xí)的無人駕駛系統(tǒng)決策安全性問題，本文首先給出了時(shí)空同步軌跡的介紹，指出無人駕駛系統(tǒng)是時(shí)間空間安全攸關(guān)的系統(tǒng)，并給出了無人駕駛特定領(lǐng)域的時(shí)空同步約束規(guī)約語言.其次，無人駕駛的安全性主要是關(guān)心系統(tǒng)的時(shí)空是否重疊，本文基于時(shí)空同步約束語言和自動(dòng)機(jī)的定義，展示了無人駕駛控制器和占用/申請(qǐng)(撤銷占用/申請(qǐng))空間的動(dòng)作，規(guī)約了安全狀態(tài)遷移的條件，給出了如何檢測占用時(shí)空重疊和申請(qǐng)時(shí)空重疊的檢測標(biāo)準(zhǔn).然后，針對(duì)學(xué)習(xí)任務(wù)非Markov性質(zhì)的獎(jiǎng)勵(lì)函數(shù)，本文給出系統(tǒng)狀態(tài)-動(dòng)作空間遷移系統(tǒng)的安全遷移條件，提出形式化時(shí)空同步約束獎(jiǎng)勵(lì)狀態(tài)機(jī)，來提高獲得強(qiáng)化學(xué)習(xí)非Markov性質(zhì)獎(jiǎng)勵(lì)函數(shù)的安全性，進(jìn)而來提高形式化約束制導(dǎo)的獎(jiǎng)勵(lì)函數(shù)設(shè)置的可解釋性.最后通過無人駕駛高速場景下變道超車的案例，在SUMO仿真平臺(tái)上驗(yàn)證所提方法的有效性.

在將來的研究工作中，首先需要優(yōu)化強(qiáng)化學(xué)習(xí)安全約束的設(shè)計(jì)與訓(xùn)練，考慮交通規(guī)則對(duì)無人駕駛系統(tǒng)的影響，建立遵守交通規(guī)則的負(fù)責(zé)任的和安全的無人駕駛決策系統(tǒng).其次，需要改進(jìn)強(qiáng)化學(xué)習(xí)獎(jiǎng)勵(lì)回報(bào)函數(shù)的設(shè)計(jì)與訓(xùn)練，提升學(xué)習(xí)的效率和學(xué)習(xí)策略的可解釋性.最后，目前實(shí)驗(yàn)驗(yàn)證是在模擬的環(huán)境下進(jìn)行，而且駕駛場景比較簡單，在今后的工作中，需要在其他交通場景比如交叉路口和環(huán)島等加強(qiáng)仿真實(shí)驗(yàn)，同時(shí)還需要在實(shí)際無人駕駛系統(tǒng)中部署結(jié)合安全約束的強(qiáng)化學(xué)習(xí)研究與應(yīng)用，逐步推進(jìn)安全強(qiáng)化學(xué)習(xí)在無人駕駛系統(tǒng)中的推廣與實(shí)際應(yīng)用.

作者貢獻(xiàn)聲明：王金永負(fù)責(zé)閱讀文獻(xiàn)和初稿寫作，黃志球提供研究基金和科學(xué)問題，楊德艷提出算法思路和文獻(xiàn)整理，Xiaowei Huang提供實(shí)驗(yàn)方案和safeAI論文思路，祝義負(fù)責(zé)形式化理論與論文審查，華高洋負(fù)責(zé)實(shí)驗(yàn)設(shè)計(jì)與結(jié)果分析.