日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

ドローン物流システムにおけるモデル検査法を用いた運行スケジュールの決定手法
辻 光顕

長谷部 浩二近年の物流業界では，物流量の増加に伴うドライバー数の不足や交通渋滞の発生などが課題となっている．このため，ドローン (無人航空機) を用いて荷物の配送を行うシステムが注目されている．ドローンを用いた効率的な配送を実現ためには，各ドローンの飛行時間が最短になるようなスケジューリング（荷物の割り当てや飛行経路の決定）を行う必要がある．また，複数のドローンが限られた空間内に同時に存在することによる衝突の危険の排除や，定期的な充電などの制約条件を満たす必要もある．本論文では，こうした効率的かつ安全なドローンのスケジューリングを行うための手法を提案する．特にここでは，実時間システムの状態を網羅的に探索するモデル検査器である
Uppaal を用いて，反例からスケジューリングを行う手法を用いる．また，本論文では，いくつかの具体例を用いて提案手法の有用性を示す．

用いて商品を保管している配送センターからそれら

1 研究の背景と目的を直接顧客の下に届けるというものである．さらに，近年，物流業界では，通信販売の普及などによる物

Amazon 社は複数のドローンが隊列編成を行うこと流量の急増に伴い，ドライバー数の不足や交通渋滞で，単一のドローンによる配送に比べ，より重量のあの発生などが大きな問題になっている．こうした問題る荷物を配送する方法も提案している．に対処する方法として，ドローン (もしくは無人航空

また，国内では KDDI 社が「スマートドローン」

機：Unmanned Aerial Vehicles, UAV) を利用した物と呼ばれるプロジェクトを進めている [1]．このプロ流システムに注目が集まっている．また，ドローンをジェクトは，災害時の物資支援やその状況の把握など用いた物流は，既存の輸送手段と比べて細かい移動がを行うことを目的としてドローンを運用するという可能となることから，商用のサービスに限らず災害時ものである．このプロジェクトでは，KDDI 社が保の支援物資の輸送手段としても期待が高まっている．

有する携帯無線基地局を利用することによって，自動こうした背景から，ドローンによる物流システムの研かつ広域でのドローン運用を提案している．

究開発が数多く行われてきた．

ドローンを用いた物流システムにおいて，効率的な例 と し て ，海 外 で は 米 国 企 業 の Amazon 社 が配送を実現するためには，複数あるドローンの飛行時「Prime Air」と呼ばれる商品の配送計画を進めて間が最短となるようなスケジューリング（輸送する荷いる [2]．これは，従来のトラックによる配送のコス物の割り当てや飛行経路の決定）が求められる．一方

トや時間を削減することを目的として，ドローンをで，複数のドローンが限られた空間内に同時に存在することによる衝突の危険の排除や，定期的な充電，Collision-free Scheduling of Drone Delivery Systems
Using Model Checking.
Mitsuaki Tsuji, 筑波大学情報学群情報科学類, Collegeof Information Science, University of Tsukuba.
Koji Hasebe, 筑波大学システム情報系情報工学域, Faculty of Engineering, Information and Systems, University of Tsukuba.

さらには隊列の編成のためのドローン間の同期など，さまざまな制約条件を満たす必要もある．
このような衝突回避に関する先行研究として，例
えば論文 [15] では，ドローン同士による衝突回避をヒューリスティクスによってスケジューリングする手法を提案している．また論文 [8] では，複数のドローンが充電を繰り返しながら運行するシステムを対象6に，メタヒューリスティクスを用いてドローンの飛5行距離を最適化する手法について述べている．また，

4

本論文と同じ手法を用いた先行研究として，論文 [5]3[6] ではタスクのスケジューリングを Uppaal [3] と呼2ばれるモデル検査器によって行う手法について述べて

1いる．

3a2b45

167c
12

3456

一方で，本論文における物流システムでは，複数のドローンが単体あるいは隊列を編成して運行するも図1運行エリアの具体例 1のとなっている．そのため，ドローン同士による衝突の危険性がない最適な運行スケジュールを求めるためには，既存の手法を直接適用することが難しいと考え

6られる．

5

このような課題に対して，著者らはモデル検査法

4を用いてシステムの状態を網羅的に探索することに

3より，ドローン同士の衝突が発生しない最適な運行ス2ケジュールの決定手法について提案する．特にここで1は，複数のドローンが隊列を編成しながら荷物の配送

3a2b4151234を行うようなシステムについてモデル化を行い，運行スケジュールを決定する手法について述べる．具体

図2

運行エリアの具体例 2

的には，論文 [5] [6] のアイデアを基に，モデル検査器

Uppaal によってドローン同士の衝突が発生しないよ2. 1 ドローン

うな反例を求めることで，各ドローンの飛行時間が最

ここで扱う物流システムは，人による操作なしで短となる運行スケジュールを求める方法について説明

飛行可能なドローンによって構成される．ドローンはする．

配送する荷物の重量に応じて，単体あるいは複数の本論文の構成は次の通りである．第 2 章では著者

ドローンが隊列を編成することによって飛行を行う．

らが対象とする物流システムの概要について説明し，また，これらのドローンは内蔵されたバッテリによっ

第 3 章で物流システムのモデル化について述べる．まて一定時間連続して飛行することが可能であり，随時た，第 4 章で物流システムの運行スケジュールを決充電を行うことで配送を継続することができる．

定する手法について説明し，第 5 章でモデル検査法による検証結果を示す．第 6 章では関連研究について述べ，最後に第 7 章で結論および今後の課題について述べる．

2. 2 運行エリア
この物流システムでは，あらかじめドローンが配送を行うためのエリアが存在し，これを運行エリアと呼ぶ．図 1 と図 2 に運行エリアの具体例を示す．

2 物流システムの概要
この章では，本研究で対象とする物流システムの概要について説明する．

運行エリアは格子状に区切られており，各マスの中には荷物を輸送するための拠点である基地や，それらを届ける場所である配送先が存在する．さらに，運行エリアには充電スペースが複数設置されており，これを利用することで随時ドローンのバッテリを充電する

ことができる．
例えば，図 1 においてマスの中に示された四角と6丸はそれぞれ基地，配送先を表し，三角は充電スペー5スを表している．各配送先に描かれた数字は基地を出4発したドローンが移動するための順番を表している．

3

また，充電スペース上の文字はこれらを区別するた2めのものである．図 1 において，ドローンは配送先 11から配送先 2 へ移動する場合に充電スペース a を通3ba2!
456c12173456過することが可能である．同様に，配送先 3 から配送先 4 へ移動する場合に充電スペース b を通過する

図3

衝突による危険性の例

ことが可能である．

2. 5 衝突の危険性
2. 3 ドローンの運行

本論文における物流システムでは，同時に複数の第 2.2 節で述べたように，ドローンは通過する配送ドローンが移動する．そのため，運行スケジュールに先の順番が決まっており，その順番に応じてマスを縦よっては，同じ時刻に複数のドローンが狭い領域に存横移動することが可能である．例として，図 1 の矢在することによって衝突が起きてしまう可能性があ印で示すような 2 つの経路が存在する．なお，マスる．その状況を図 3 に示す．

を移動するために必要な距離は全て等しいものとす

図 3 では，バツ印で示した位置に複数のドローンがる．また，ドローンは配送できる荷物の重量に制約が同時に存在しており，衝突の危険性があることを示しあるため，2 地点間を単体で移動する場合と，隊列をている．これは配送先 2 から配送先 3 へ飛行するド編成して移動する場合がある．例えば図 1 の例では，ローンと，配送先 3 から配送先 4 へ飛行するドロー

配送先 1 と配送先 2 の間は複数のドローンが隊列をンが同時に同じマスに存在していることを表してい編成して移動し，それ以外の地点間では単体のドローる．この例では 1 つのマスに 2 つ以上のドローンがンによって移動を行うというようなものである．

存在することを衝突と見なしている．しかし，どの程度の接近を衝突と見なすか，あるいはドローンの大き2. 4 隊列の編成さといった物流システムの特徴に依存してマスの大きこの物流システムでは，複数のドローンが隊列をさは変化する．また，各マスを細かくしていくことに編成して移動することができる．隊列は，行先を同一よってモデルの精度を高めることができる．一方で，とする複数のドローンによって，基地あるいは配送精度を高めた場合にはモデルの状態数が多くなるた先に存在する地上のスペースを利用して構成される．

め，運行スケジュールを決定することが困難になる可そのため，ドローンは隊列を編成する際に一度着陸す能性がある．したがって，モデル化を行う場合には実る必要がある．着陸しているドローンと飛行している際の物流システムに応じた判断を行う必要がある．

ドローンが衝突する可能性は低いため，隊列を編成する場合には，一時的に複数のドローンが同じマスに存

3 ドローン物流システムのモデル在することが可能である．ドローンは配送時間をでき

この章では，2.5 節で示した衝突を防ぐスケジューるだけ短くするため，隊列を編成可能であるものからルを決定するため，物流システムをモデル化する方法

順に編成を行うものとする．

について述べる．

3. 1 ドローンのモデル
ドローン全体の集合を D で表す．全てのドローン4は隊列を編成することが可能であるが，その上限を表32abす関数を max f leet : D → N と定義する．(ただし，N は自然数全体の集合である．)
また，ドローンはバッテリを使用して動作するた

23

141め，連続して飛行可能な距離に上限がある．そのた1め，その上限を超えない範囲でドローンは充電スペースを訪れる必要がある．ドローンが運行エリア上のマスを連続して移動できる回数の上限を表す関数を

max range : D → N と定義する．

図4234

対象とする運行エリア

なわち，運行ルートにおける任意の部分列に対し∀i, j, k[(ai , aj ∈ E) ∧ ∀k(i < k < j → (ak ∈/ E)) →3. 2 運行エリアのモデル

j − i ≤ max range] である．

本論文では，運行エリアを図 1 や図 2 のような格子状の m 行 n 列からなる矩形を用いて表現し，そ4 モデル検査法によるスケジュールの決定の集合を A ⊆ N × N で表す．運行エリア上の各マ

4. 1 対象とする物流システムのモデル

スをセルと呼び，その位置を順序対 ⟨x, y⟩(ただし，2.2 節において具体的な運行エリアを示したが，こ1 ≤ x ≤ n, 1 ≤ y ≤ m) で表現する．運行エリアにこでは図 4 のような簡単なモデルを対象とする．

は，ドローンのバッテリを充電することが可能な複数

また，このモデルでは複数のドローンが配送先 1の充電スペースが存在し，その集合を E ⊆ A と表す．

から配送先 2 の間を隊列によって移動するものとす

また，各マスには衝突の危険を回避するため，同時る．さらに，充電スペース a はドローンが配送先 1 かに飛行可能なドローンの数に対する上限が定められら配送先 2 を移動する途中に訪れることができるもている．そこで，その上限を表す関数を cap : A → Nのとする．同様に，充電スペース b は配送先 2 からと定義する．ただし，ドローンは隊列を編成および解配送先 3 の間を移動する途中に訪れることが可能で除する際に着陸するため，その場合は同じセル上をドあるとする．ここでは，全ての a ∈ A および d ∈ D

ローンが存在しても衝突の危険性はないものとする．

において，max f leet(d) = 2，max range(d) = 8，同様に，隊列飛行しているドローンは単一のドローン

cap(a) = 2 である．と見なし，同じセル上に存在している場合でも衝突の危険性がないものと考える．

4. 2 Uppaal による物流システムのモデル
第 3 章で用いたモデルを，モデル検査器 Uppaal に

3. 3 飛行ルートのモデルよって記述する方法について説明する．Uppaal では

ドローンの飛行ルートを a1 , . . . , an ∈ A のよう対象のシステムを GUI を用いて記述し，システムのに，運行エリア A 上におけるセルの列を用いて表各状態をロケーション，状態間の遷移をエッジとしてす．ただし，各 ai = ⟨xi , yi ⟩, (1 ≤ i ≤ n) について，表現する．前節で述べたドローンのモデルを Uppaal

xi = xi+1 かつ |yi − yi+1 | = 1，または，yi = yi+1

によって記述したものを図 5 に示す．

かつ |xi − xi+1 | = 1 であるとする．また，全てのこのモデルでは，基地や配送先などのドローンが存

ドローンは基地を起点として運行を行ってから再び在できる位置をロケーションで表し，その間を接続す基地に戻るため，a1 = an である．ドローンは連る運行経路をエッジで表現している．また，それぞれ続して飛行可能な距離に制限があるため，それを超のドローンにとって固有な時間変数 lc および，モデえない範囲で充電スペースを訪れる必要がある．すル全体の時間変数 gc を定義している．ここで扱うモ図5

Uppaal によるドローンのモデル

デルにおいて，ドローンは隣接する地点間を 1 単位4. 3 検証すべき性質時間あるいは 2 単位時間の範囲で遷移し，連続して物流システムが最低限満たされなければならない

最大 MR 個のロケーションを移動することができる．

ことは，「全てのドローンがいつかは必ず全ての目的

なお，この値は関数 max range によって与えられる地を通過して戻ってくる」ような運行スケジュールがが，図 5 の例では全て 8 としている．ドローンは図 5存在することである．すなわち，以下の性質が満たさの赤い四角で囲まれたロケーションである P33 を起れる必要がある．

点とし，最終的にロケーション finish に遷移する．また，隊列の編成は Uppaal におけるバイナリチャネルを用いて表現され，これによって複数のドローンが通信を行って協調動作することができる．

(P1)

全てのドローンは，全ての配送先を通過してから出発地点に到達可能である．
この性質が満たされれば，全てのドローンが配送を行ってから出発地に戻るようなスケジュールを決定することができる．反対に満たされなければ，運行スケジュールを決定することができない問題であることがなわち論理式 (L1) は，ドローン d1 およびドローン分かる．この性質を検証することによって，対象とすd2 が，いつかはロケーション finish に到達するようる物流システムにおける運行スケジュールがあらかじな実行列が存在することを意味する．

め決定されている場合に，衝突が発生することなく運行が可能か否かを確認することができる．性質 (P1)

また，性質 (P2) を検証する論理式は以下のように記述することができる．

が満たされる場合は，論文 [5] の手法と同様に，性質(P1) の否定となる性質を検証することによって最小(L2)A□ not (d1.finish and d2.finish)

時間かつ衝突が発生しないような運行スケジュールを論理式 (L2) において，A はシステムの実行列にお求めることができる．すなわち，以下の性質を検証すいて全てのパスを表し，□ はある命題が常に成立するればよい．

(P2)ことを表す．すなわち論理式 (L2) は，d1 および d2全てのドローンは，出発してから再び出発地点に到達することはない．
性質 (P2) を検証することによって，Uppaal はこの性質が満たされないような反例を検出して出力する．また，Uppaal ではモデル全体の経過時間 gc がが，ロケーション finish に到達することがないことを意味している．

5 検証結果
この章では，第 4 章で説明したモデルおよび論理式を用いて実際に検証した結果について述べる．

最小となるような反例を出力することができる．これによって，衝突の発生がなくドローン全体の運行時間

5. 1 2 つのドローンにおける検証結果が最小となるような運行スケジュールを得ることがで

4.1 節に示した運行エリアに対し，2 つのドローンきる．

が運行するモデルについて検証した結果，性質 (P1)

なお，ドローンの衝突が発生しないような運行スは満たされる結果となった．また，性質 (P2) についケジュールを求めたい場合には，性質 (P2) のみを検て検証すると反例が得られ，衝突が発生しないような証してもよい．なぜなら，性質 (P2) が満たされる場

最小時間の運行スケジュールを検出することができ合はドローンが衝突を回避できないことを意味してた．なお，検証にかかった時間は 0.002 秒であり，最おり，これは性質 (P1) が満たされないことと同値な小時間は 13 単位時間である．

ためである．同様に，性質 (P2) が満たされない場合は，性質 (P1) が満たされることと同値である．

5. 2 4 つのドローンにおける検証結果
また本研究では，前節の例よりもドローンの数を4. 4 TCTL 式による検証増やして検証を行った．4 つのドローンが存在する場

Uppaal における検証式は，時間付計算木論理 TCTL

合でも，性質 (P2) を検証した結果，先の例と同様に，の部分論理を使って記述することができる [4]．まず，衝突が発生しないような最小時間の運行スケジュー

性質 (P1) については，以下にように記述することがルを得ることができた．なお，検証にかかった時間はできる．

8.6 秒であり，最小時間は 15 単位時間である．

(L1)

E♢ (d1.finish and d2.finish)

5. 3 6 つのドローンにおける検証結果

論理式 (L1) において，E はシステムの実行列におこれまでに述べた例に対し，さらにドローンの数をけるあるパスの存在を表し，♢ はある命題がいつかは増やして検証を行った結果について述べる．モデルに成立することを表す．また，d1.finish はドローンおけるドローンの数を 6 つにして検証を行うと，検d1 がロケーション finish に存在することを示す．す証に必要なメモリ量が不足してしまうことによって検証ができないという結果になった．これはモデル検査法を用いる場合によく見られる問題であり，状態爆発と呼ばれる．このような問題の対策としてはモデルにおける変数を減らしたり，より小規模な問題に切り分けて考えるなどの工夫が必要となる．

6 関連研究これまで，数多くの物流システムや交通システムを対象に，船舶や車両などの衝突回避に関する研究がなされてきた．例として，論文 [10] では船舶の運行における衝突の問題に注目し，蟻コロニー最適化を用いて衝突回避を行う手法について述べている．また，
論文 [13] では，災害時に複数のドローンを活用するという目的で運用した場合に，全てのドローンが要求される動作を行うか否かについて Uppaal を用いた研究を行っている．本論文と同様の手法を用いたものとしては，論文 [5] が工場の機械に対する最適な動作スケジュールを求める手法について提案している．
しかし，本研究で扱ったような隊列編成可能な複数のドローンが移動する物流システムを対象に，その運行スケジュールをモデル検査法によって決定する手法を提案した研究はこれまでに行われていない．一般的に，このような複雑な振る舞いを持つ物流システムの運行スケジュールを決定することは容易ではないため，本研究の提案した手法は有益なものであると考えられる．

7 結論と今後の課題
本論文では隊列編成可能な複数のドローンが動作する物流システムを対象に，その運行スケジュールをモデル検査法によって決定する手法について提案した．
複雑な振る舞いを持つシステムに対して，最短時間となる運行スケジュールをを決定することができた．
本論文では，ドローン物流システムを対象にその運行スケジュールを決定する手法について述べたが，この手法は他の物流システムに対しても適用することが可能であると考えられる．今後は，より複雑な問題を扱った場合に起こる状態爆発問題に対応するため，モデルを小さな問題に分割することによりスケジューリングを可能とするような課題に取り組む予定である．
参 考 文 献[ 1 ] http://news.kddi.com/kddi/corporate/
newsrelease/2017/05/09/2422.html[ 2 ] http://www.amazon.com/primeair/[ 3 ] http://www.uppaal.org/[ 4 ] E. M. Clarke, O. Grumberg, and D. Peled. Model
Checking, The MIT Press, 1999.
[ 5 ] A. Fehnker, Scheduling a Steel Plant with Timed
Automata. Real-Time Computing Systems and Applications(RTCSA1999), pp.280–286, 1999.
[ 6 ] G. Behrmann, K. G. Larsen, J. I. Rasmussen,Optimal Scheduling Using Priced Timed Automata.
SIGMETRICS Perform. Eval. Rev., pp.34–40,2005.
[ 7 ] G. Sirigineedi, A. Tsourdos, R. Żbikowski, B. A.
White, Modeling and Verification of Multiple UAVMission Using SMV. arXiv e-prints, 2010.
[ 8 ] J. Kim, B. D. Song, J. R. Morrison, On theScheduling of Systems of UAVs and Fuel Service
Stations for Long-Term Mission Fulfillment, Journal of Intelligent & Robotic Systems, vol.70, no.1,
pp.347–359, 2013.
[ 9 ] J. S. Bellingham, M. Tillerson, M. Alighanbari,J. P. How, Cooperative Path Planning for Multiple UAVs in Dynamic and Uncertain Environments. 41st IEEE Conference on Decision and Control(CDC2002), pp.2816–2822, 2002.
[10] M. C. Tsou, C. K. Kuang, The Study of Ship
Collision Avoidance Route Planning by Ant Colony
Algorithm. Journal of Marine Science and Technology, vol.18, No.5, pp. 746–756, 2010.
[11] M. M. Quottrup, T. Bek, R. I. Zamanabadi,Multi-Robot Planning: A Timed Automata Approach. International Conference on Robotics andAutomation(ICRA2004), pp.4417–4422, 2004.
[12] N. Agatz, P. Bouman, M. Schmidt, Optimization Approaches for the Traveling Salesman Problem with Drone. ERIM Report Series Reference,
No.ERS-2015-011-LIS, 2015.
[13] N. Li, D. Bai, W. Jiao, Z. Yang, Verifying
Stochastic Behaviors of Decentralized Self-Adaptive
Systems: A Formal Modeling and Simulation BasedApproach. arXiv e-prints, 2017.
[14] T. Yu, J. Tang, L Bai, S. Lao, Collision Avoidance for Cooperative UAVs with Rolling Optimization Algorithm Based on Predictive State Space.
Applied Science, vol.7, No.4, 2017.
[15] Y. Khosiawan, I. Nielsen, Indoor UAV Scheduling with Restful Task Assignment Algorithm, arXive-prints, 2017.
[16] X. Zou, R. Alexander, J. McDermid, On theValidation of a UAV Collision Avoidance System
Developed by Model-Based Optimization: Challenges and a Tentative Partial Solution. International Conference on Dependable Systems and Networks Workshop (DSN-W2016), pp.192–199, 2016.