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

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

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

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

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

近期的研究工作顯示無人駕駛系統(tǒng)已經(jīng)廣泛采用時間空間約束的形式化規(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)域時間建模方面，時間自動機(jī)被用來建模通信無人駕駛車輛之間的行為[17]，時鐘約束規(guī)約語言(clock constraint specification language, CCSL)被用來建模系統(tǒng)的安全約束[18-19].時空同步約束系統(tǒng)中的事件觸發(fā)不僅受嚴(yán)格的時序和物理時間的約束，同時還要邏輯和物理空間關(guān)系的約束[20-21].無人駕駛決策系統(tǒng)的核心問題是如何安全高效地分配路權(quán)來解決可能的時空重疊.無人駕駛行為需要在滿足時間約束的同時滿足空間關(guān)系的約束，反之亦然，這種方法可以保證在某一時刻和空間位置，只允許最多一輛車存在.時空安全攸關(guān)的事件包括安全衛(wèi)士和不變式規(guī)約，需要滿足邏輯時序和物理時鐘關(guān)系，同時需要滿足邏輯空間關(guān)系和物理空間位置.然而在無人駕駛領(lǐng)域，現(xiàn)有的時空同步約束規(guī)約方法和驗(yàn)證技術(shù)是不充分的.

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

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

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

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

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

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

5)設(shè)計了無人駕駛汽車在高速公路變道超車的案例，在無人駕駛仿真環(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á)和攝像機(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í)行模塊，動作控制信息包括縱向運(yùn)動的加速和減速等規(guī)劃動作，以變道、超車、轉(zhuǎn)向等橫向運(yùn)動規(guī)劃信息.智能體的決策能力是實(shí)現(xiàn)車輛全自動化的基本要素，目前大量的研究采用強(qiáng)化學(xué)習(xí)來實(shí)施無人自主決策[26-29]，綜合周圍交通環(huán)境和自車信息，產(chǎn)生安全通明安全的駕駛行為.在無人駕駛應(yīng)用中，無人車做動作或者做決策，強(qiáng)化學(xué)習(xí)中的智能體就是無人車；而環(huán)境是與無人車交互的對象，無人車所處的真實(shí)交通物理世界就是環(huán)境，包括交互過程中的道路信息、交通標(biāo)志、交通規(guī)則、駕駛經(jīng)驗(yàn)等規(guī)則和推理機(jī)制.動作空間是決策模塊輸出給執(zhí)行模塊的行為決策信息，獎勵表示交通環(huán)境對智能體基于當(dāng)前狀態(tài)產(chǎn)生動作的打分，需要系統(tǒng)設(shè)計人員設(shè)計獎勵函數(shù)，本文主要針對如何獲得非Markov性質(zhì)的安全可解釋獎勵函數(shù)的設(shè)置展開研究.

Fig.1 The RL architecture for autonomous driving systems

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

貝爾曼方程式(1)和式(2)表示狀態(tài)價值函數(shù)和動作價值函數(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)常用的算法是時序差分算法(tem-poral difference, TD).假設(shè)有一個模型Q(s,a;w)，w是模型訓(xùn)練的參數(shù)，給定一個四元組(st,at,rt,st+1)，可推導(dǎo)出折扣回報為Gt=Rt+γGt+1，根據(jù)式(3)，當(dāng)智能體執(zhí)行動作at后，環(huán)境通過狀態(tài)轉(zhuǎn)移概率pr(st+1|st,at)可以計算出下一時刻的新狀態(tài)st+1，而第t時刻的獎勵最多只依賴于隨機(jī)變量St,At,St+1，現(xiàn)在已經(jīng)觀測到了st,at,st+1，則可得變量Rt的觀測值，記作rt，接著可以對期望做蒙特卡洛近似，可得：

(4)

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

(5)

算法1.DDQN求解最優(yōu)動作價值算法.

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

i∈{0,1};

② for eachepisode

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

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

更新;

④ while(episode

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

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

a*;w1);

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

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

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

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

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

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

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

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

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

Table 1 The Formal Semantics of Clock Relations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

定義7.時空同步約束規(guī)約語言.時空同步約束規(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 時空同步約束自動機(jī)和時空遷移條件

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

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

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

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

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

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

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

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

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

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

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

Fig.3 An example of spatio-clock synchronous controller

定義9.無人駕駛控制器動作.無人駕駛控制器動作(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申請道路l.動作wdc(A)表示車輛A撤銷申請的道路.動作r(A)表示車輛A占用之前申請的道路.動作wdr(A,l)表示車輛A撤銷占用除了道路編號l以外的道路.τ表示空動作，允許沒有任何動作的交通遷移.

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

下面給出時空同步遷移的定義.

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

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

(6)

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

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)系，并且加上除去第一個元素在關(guān)系{vα}中，同時也在關(guān)系ξ中的關(guān)系后的所有剩余ξ中的關(guān)系.

對于任何車輛I∈和道路編號n∈，根據(jù)式(9)車輛占用之前申請或者占用的道路編號，根據(jù)式(10)車輛也可以撤銷占用除了道路編號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)

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

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

(11)

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

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

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

定義 11.無人駕駛安全衛(wèi)士(autonomous driving safety guards).根據(jù)定義4，時空安全衛(wèi)士條件(即不發(fā)生碰撞)表示為申請和占用時空區(qū)域不發(fā)生重疊，可以檢驗(yàn)安全性條件來確保沒有交通事故發(fā)生(前提是車輛之間的通信不會發(fā)生延遲，車輛的感知器和其他硬件不會發(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ū)域.這時安全衛(wèi)士條件意味著任何兩輛車輛之間不存在相交的時空區(qū)域，可表示為

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

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

(13)

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

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

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

(14)

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

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

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

(15)

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

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

re(c2)(l,t)).

(16)

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

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

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

safeOverlap(c1,c2)).

(17)

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

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

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

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

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

keep_lane,brake,hard_brake,acc,

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

Fig.4 The research framework ofsafeRL approach

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

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

算法2.safe_DDQN求解最優(yōu)動作價值算法.

輸出：形式化約束制導(dǎo)的動作價值估計.

② fort=0 toTdo

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

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

⑤ while(episode

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

⑧ 更新時空同步約束獎勵狀態(tài)機(jī)狀態(tài);

⑨ 更新時空同步約束獎勵狀態(tài)機(jī)獎勵;

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

/*當(dāng)前價值為獎勵*/

/*更新價值，執(zhí)行新的動作*/

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

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

更新*/

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

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

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

(19)

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

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

(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的獎勵反饋函數(shù)：

(22)

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

(23)

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

Rlane=exp(-1.2×dispy_mid).

(24)

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

(25)

5 案例分析

5.1 案例需求分析

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

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

Fig.6 Combine RL and SUMO simulation platform

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

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

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

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

6 相關(guān)工作

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

然后介紹結(jié)合安全約束的強(qiáng)化學(xué)習(xí)方法.對于安全攸關(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í)安全層來限制動作空間，利用基于集合的方法來增強(qiáng)強(qiáng)化學(xué)習(xí)的安全保障.Wachi等人[44]提出了一種帶約束Markov決策過程的強(qiáng)化學(xué)習(xí)方法，該方法通過擴(kuò)展安全區(qū)域來不斷學(xué)習(xí)安全約束.Gao等人[45]設(shè)計了一個結(jié)合形式化線性時序規(guī)約(linear temporal logic, LTL)的獎勵回報函數(shù)，可以更準(zhǔn)確地估計損失函數(shù)的梯度和改善訓(xùn)練過程的穩(wěn)定性.Wolf等人[46]指出僅僅對專家知識進(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í)多行動者-評論家算法，從優(yōu)秀經(jīng)驗(yàn)中學(xué)習(xí)指導(dǎo)網(wǎng)絡(luò)，并對動作價值函數(shù)進(jìn)行更新指導(dǎo).Garca和Fernández[49]給出了安全強(qiáng)化學(xué)習(xí)的定義，并給出在系統(tǒng)學(xué)習(xí)和部署的過程中增加安全約束的相關(guān)文獻(xiàn)綜述.

7 總結(jié)與展望

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

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