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

モデル検査法によるドローン物流システムの近似スケジューリング
清水 圭太 長谷部 浩二
近年，物流業界におけるドライバー不足などの問題を解決する方法として，ドローン（無人航空機）を用いた配送システムが注目されている．ドローンの運用においては，航続距離や衝突の回避などの制約条件を満たす輸送効率の高いスケジューリングが求められる．このような交通輸送システムのスケジュールを生成するために，モデル検査法を用いた手法が存在する．しかし，モデル検査法には，対象とするシステムの規模が大きくなると，しばしば状態爆発を引き起こすという問題がある．そこで本研究では，飛行区域と時間の両方を抽象化するスケジューリング手法を提案する．具体的には，飛行区域の粒度を変更し，それに応じて単位時間の粒度も変更することでモデルを抽象化する．さらに，抽象化して得られたスケジュールをもとに，それぞれの区域で詳細化を行うというものである．また本研究では，具体例をもとに提案手法の有用性を示す．

まざまなソフトウェアやハードウェアの設計に広く1 序論利用されており，SPIN [8] や NuSMV [5] など多くのモデル検査法 [6] は，システムの仕様が安全性などモデル検査器が存在する．の性質を満たしているかどうかを自動的に検証する

モデル検査法はスケジューリングなどの離散最適ための形式手法の一種である．モデル検査法では，化問題にも適用することができる．その基本的なア対象とするシステムの振る舞いを状態遷移モデルとイディアは最適化問題を到達可能性問題へと還元すして記述し，システムが満たすべき性質を線型時間るというものである．すなわち，対象とするシステム論理（Linear Temporal Logic：LTL）や計算木論理のモデルに対して，スケジュールが満たすべき条件（Computational Tree Logic：CTL）などの時相論理を記述した論理式の否定を入力として与えて検証を式で記述する．これらの入力から，システムがとりう行い，その検証によって得られた反例をスケジューる状態全てを網羅的に調べることで，システムが性質ルとして解釈するというものである．モデル検査法

を満たすかどうかを検証する．システムが性質を満を用いたスケジューリングの例としては，Behrmann

たす場合には「valid」を出力し，そうでない場合にらの研究 [1] が挙げられる．そこでは時間オートマトは初期状態から性質が満たされない状態に至るまでンを扱うことができるモデル検査器である UPPAALの実行列である反例を出力する．モデル検査法はさ[2] を用いて，さまざまなスケジューリング問題の求Approximate Scheduling for Drone Delivery SystemUsing Model Checking
This is an unrefereed paper. Copyrights belong tothe Authors.
Keita Shimizu, 筑波大学システム情報学群コンピュータサイエンス専攻, Department of Computer Science,
University of Tsukuba.
Koji Hasebe, 筑波大学システム情報系, Faculty of Engineering, Information and Systems, University ofTsukuba.

解を行なっている．また，UPPAAL を用いた例としては，製鉄所の製造工程のスケジューリングに関するFehnker の研究 [7] が挙げられる．
モデル検査法を用いたスケジューリング手法には，作成したモデルを再利用して，システムの安全性などの性質を検証できるという利点がある．一方で，モデル検査法には状態爆発が起こりやすいという課題も存在する．スケジューリングにおける状態爆発を回避するためには主に 2 つのアプローチが考えられる．

ジュールを 5 分以内に得ることができた．

1 つ目は，モデル検査法が最適化問題を解く際に必ず本論文の構成は以下の通りである．第 2 章では，対しも効率的な探索を行わないことから，モデルを改良象とするシステムの概要を述べる．第 3 章では，そのして探索を効率よく行うようにするというものであモデル化の方法について説明する．第 4 章では，提る．そのような例として，Ruys [9] による分枝限定法

案手法の 1 つである抽象化の方法について説明する．

を取り入れたモデルの作成方法がある．しかし，こう

第 5 章では抽象化によって得られた解を具体化するした方法によってモデルを作成するのは一般に容易方法について説明する．最後に，第 6 章で結論と今ではなく，探索アルゴリズムに精通していなければな

後の研究課題について述べる．

らないという問題がある．またもう 1 つの方法としては，モデルを抽象化することによって状態数を減

2 ドローンによる物流システムの概要

らすというものがある．状態爆発を回避することを

この章では，対象とするドローンによる物流システ目的とした抽象化の技術は，類似する複数の状態を 1

ムの概要について説明する．

つの状態にまとめる方法など数多く存在するが，スケジューリングに適した抽象化については未だ十分検2. 1 飛行エリア

討されていない．

このシステムでは，あらかじめドローンが飛行できそこで本論文では，モデル検査法を用いた近似スケるエリアが定められている．これを飛行エリアと呼ジューリング手法を提案する．特にここでは，スケぶ．このシステムの目的は，デポにある荷物を飛行エジューリングの対象をドローンを用いた物流システムリア内の指定された場所に配送することである．飛とし，ドローンのバッテリ残量や衝突の回避などの制行エリアの例を図 1 に示す．飛行エリアは格子状に約を満たす最短のスケジュールの生成を目的とする．

区切られており，各マスはドローンの充電や離着陸，本研究で提案する近似化の基本的なアイディアは，2荷物の搭載などを行う 1 つ以上のデポとそれ以外の次元格子空間によってモデル化されたドローンの飛マスに分類できる．本論文では，デポ以外のマスを通行エリアに対して，複数のマス目を 1 つの大きなマス常マスと呼ぶ．通常マスに書かれている数字はその目にまとめるという抽象化を行うというものである．

通常マスにおける顧客の需要を表している．各需要その上で，抽象化によって得られたスケジュールをもは荷物を持つドローンがその通常マスを飛行して荷とに，抽象化したマス目の内部におけるスケジュー物を配送した際に，その値を 1 減らすことができる．

ルの詳細化を行うことにより，全体の具体的なスケジュールを得る．以上で述べた手法の利点としては，組み合わせるマスの数を調整することで任意の抽象化レベルを選択できる点が挙げられる．また，抽象化のためのモデルの変更が単純であるということも，利点として挙げられる．
本論文では，モデル検査器として，大規模で特に同期プロセスによるシステムの記述に適した NuSMV[5] の後継である nuXmv [4] を用いた．さらに，制約条件を満たす最短スケジュールを得るために，nuXmvが提供する有界モデル検査 [3] を用いて検証を行なった．その結果，例えば厳密解となるスケジュールが 1時間以内で求めることができなかった 4×4 で区切られた飛行エリアの場合でも，抽象化を行うことでスケ

図1

飛行エリアの例

2. 2 ドローン

3. 2 ドローンの動作のモデル化

この物流システムで扱うドローンは，内蔵されていドローン全体の集合を D とする．各ドローンはるバッテリによって 1 回の充電で飛行できる時間がバッテリが許す飛行時間以内でデポを離陸し，需要が限られている．しかし，デポで充電を行うことにより1 以上の通常マスに荷物を配達したのちにデポに着陸飛行する時間を増やすことが可能である．対象の物する必要がある．その飛行時間の上限を表す関数を流システムでは，複数のドローンがすべての通常マス

max f ly : D → N とする．

における需要を 0 にするために飛行を繰り返す．各モデルにおける時刻を，0, 1, 2, . . . ∈ T (= {N}) とマスにいるドローンは，自身が現在いるマスと縦もしする．ドローンのスケジュールは，各時刻におけるくは横に隣接するマスに移動するか，同じマスにとどそれぞれのドローンの飛行エリアの位置を定めるこまるホバリングをするものとする．なお本論文では，とによって定義される．すなわち，長さ h のドロー

1 単位時間をドローンがあるマスから隣接しているマンのスケジュールとは，関数 sche : Th × D → F のスへ移動するのに必要な時間とし，すべてのマスで移ことであるとする．（ただし，Th = {t | 0 ≤ t ≤ h}

動するために消費する時間は同じものとする．とする．）ここで，各ドローンはデポにて離着陸をす

また，スケジュールによってはある時刻に複数のドるため，sche(0, d), sche(h, d) ∈ Depot を満たすもの

ローンが狭い領域内に存在することによって衝突がとする．また，時刻 t − 1 から時刻 t へのドローンの起きてしまう可能性がある．そこで本論文では，同じ移動は縦横のマスへの移動もしくはホバリングの 3

時刻に同じ通常マスに滞在することができるドロー種類のいずれかである．したがって，任意の t ∈ Th

ン数の最大数を設けることでこの衝突を回避させると任意の d ∈ D について，sche(t, d) = (i, j) かつものとする．

sche(t + 1, d) = (i′ j ′ ) ならば，i = i′ かつ |j − j ′ | ≤ 1
または |i − i′ | ≤ 1 かつ j = j ′ を満たすものとする．

3 対象とする物流システムのモデル化
この章では，ドローンのスケジューリングのためのモデル化について述べる．

4 モデル検査によるスケジューリング手法
この章では，第 3 章でモデル化したシステムをスケジューリングする方法について説明する．さらに，

3. 1 飛行エリアのモデル化対象とするシステムを抽象化することによる近似ス

飛行エリア F は m 行 n 列の 2 次元格子空間からなケジューリング方法について説明する．

り，通常マスとデポと呼ばれる特別なマス目から構成される．ここで，i 行 j 列のマス目を (i, j) と表記す

4. 1 モデル検査法によるスケジューリング

る．なお，本論文では一般性を失うことなく議論を単

まず，前節で述べたモデルを NuSMV の後継の純化するために，先の図 1 で示すように，デポを 1 つ

nuXmv の仕様記述言語である SMV で記述する．次だけ格子空間の外側で隣接するマス目として配置するにスケジュールが満たすべき条件の連言の否定を表すこととする．ここで，デポの集合を Depot，通常マス論理式をモデル検査法で検証し，反例が出るかを確認の集合を C とし，F = Depot ∪ C ，Depot ∩ C = ∅する．もし，反例が生成された場合，その反例は与えであるとする．また，通常マスには客の需要が存在られた条件の否定の否定，すなわち条件を満たした実し，これを表す関数を needs : C → N とする．さら行過程であり，求めるべきスケジュールとみなすことに，ドローン同士の衝突を避けるための各通常マスができる．また，本研究では検証方法として nuXmvに同時に滞在可能なドローンの最大数を表す関数をの有界モデル検査を用いる．有界モデル検査は初期状

cap : C → N とする．

態から決められた遷移数までのモデル検査を行う手法である．また，遷移数が少ない方から検証を行い，反例が出ると同時に検証を終了するため，最も短いス

ケジュールのうちの 1 つを得ることができる．

こ こ で ，現 在 の ド ロ ー ン の バ ッ テ リ ー 残 量で 移 動 で き る 時 間 表 す 変 数 を f lytimed ∈4. 2 スケジュールが満たすべき条件{0, 1, · · · , max f ly(d)} とする．この f lytime は

この節では，システムがスケジュールを生成する際ドローンが現在いるマスの種類によって以下のに，モデル検査法に与える制約について説明する．こように値が変化する．
{の制約はスケジュールの終了条件と物流システムそのものの制約の 2 種類に分類される．また本研究では，スケジュールとなる実行パスについて検証を行う
ため，時相論理式として LTL を用いる．

(F-1) 「いつかすべてのドローンがいずれかのf lytimed =max f ly(d)(posd ∈ Depot)

f lytime′d − 1(otherwise)

ただしここで f lytime′d は現在の 1 つ前のステップにおけるドローンのバッテリー残量を表すもデポにいる．」のとする．この f lytimed を用いると，LTL 式はここで，現在のドローンの位置を表す変数を以下のように表すことができる．なお，□ は内側

posd ∈ F とする．これを用いると LTL 式は以下のようになる．なお，♢ は内側の論理式が未来のある時点で成り立つときに真になるような様の論理式が常に成り立つときに真になるような様相演算記号である．

∧相演算記号である．

□(posd ∈ Depot ∨ f lytimed > 0)d∈D∧♢(posd ∈ Depot)d∈D(F-2) 「すべての通常マスについて，いつか需(S-2) 「すべての通常マスについて，通常マス内に滞在しているドローンの台数はその通常マスの最大数以下である．」
ここで，現在通常マスに止まっているドローンの要が 0 になる．」
こ こ で ，現 在 通 常 マ ス に 止 ま っ て い る 荷物を持つドローンの台数を表す変数をhasBagc ∈ {0, 1, · · · , |D|} とする．また，現在の通常マスの需要を表す変数を nowneedsc ∈{0, 1, · · · , needs(c)} とする．この nowneeds は0 ≤ nowneeds ≤ needs を 取 る も の と し ，台数を parkc ∈ {0, 1, · · · , cap(c)} とする．これと 3.1 節で述べた通常マスに滞在できるドローンの最大数を表す関数の cap を用いると，LTL 式は以下のように表すことができる．

∧□(parkc ≤ cap(c))

c∈ChasBag の値によって非決定的に変化する．

nowneedsc =以下，本論文では，すべての通常マスの cap = 1 とnowneedsc − hasBagc

し，すべてのドローンの max f ly = 30 とする．さnowneedsc

らに，対象の物流システムのモデルに対して，上記の4 項目の論理積の否定の式をモデル検査法にて検証す
この nowneedsc を用いると，LTL 式は以下のよると，スケジュールを表す反例を得ることができる．

うに表すことができる．

♢∧

4. 3 モデルの抽象化(nowneedsc ≤ cap(c))

c∈C

この節では，ドローンのスケジュールの近似解を求めるために，提案手法の 1 つである飛行エリアの抽(S-1) 「すべてのドローンについて，デポにい象化について説明する．本研究では，複数の通常マスる，もしくは通常マスにいるときのバッテリーのを 1 つの大きな通常マスにまとめる抽象化を行うこ

残量が 0 以上である．
」とで，スケジュールの近似解を求める手法を提案する．ここで，km , kn ∈ N(> 1) とする．また，m 行 n

さらに，抽象化に伴って増える 3 種類のシステム

列の矩形で表されていた飛行エリアの通常マスの部の制約について説明する．まず 1 つ目として，抽象分について，縦が km 個，横が kn 個の通常マスから通常マスの 1 辺から出るドローンの台数が km また構成される新たな通常マス capp ∈ Capp , Capp ⊆ C をは kn 台以下にする必要がある．2 つ目として，抽象生成することで，m/km 行 n/kn 列の新たな飛行エリ通常マスの隣接する 2 辺から出るドローンの合計台アに抽象化する．この抽象化した通常マス capp を抽数について，km + kn − 1 台以下にする必要がある．

象通常マスと呼ぶことにする．なお，デポは通常マス

3 つ目は，抽象通常マスの隣接する 2 辺へ入るドローと変数等の扱いが異なるため結合しないものとする．

ンの合計台数について，km + kn − 1 台以下にする必

図 2 は図 1 の飛行エリアを km = 2，kn = 2 で抽象要がある．

化したときの新しい飛行エリアである．

最後に，抽象化したモデルに対して，これらの抽象化した値を第 4.2 節における検証式で元の値の代わりに置き換えたものの論理積の否定の式をモデル検査法にて検証することで，スケジュールの近似解を生成することができる．例えば，図 1 を抽象化した図 2をスケジューリングを行うと図 3 のような近似解を得ることができた．図 3 では，各ドローンが通常マスにて配達したときは緑色で塗りつぶしてある．

図2

図 1 で示した飛行エリアを km = 2，kn = 2 で抽象化したときの飛行エリア

次に，抽象化によって変更が必要になる関数について説明する．ここで，抽象通常マスに含まれる元の通常マスを表す関数を cons : Capp → 2C とする．
まず，3.1 節で述べた需要 needs について，抽象化した状態における新しい需要を needsapp : Capp → N∑
は，needsapp (capp ) =c∈cons(capp ) needs(c) とす

図3

図 2 のスケジュールを具体化した結果ることができる．次に，各通常マスにおけるドロー5 近似解の具体化ンの最大数 cap について，抽象通常マスにおける第 4 章で説明した方法だけでは，抽象通常マス内ドローンの最大数 capapp : Capp → N は，capapp =∑3.2 節で述べたc∈cons(c) cap(c) となる．最後に，部のスケジュールまではわからない．そこでこの章

ドローンの飛行時間の上限 max f ly が抽象化によってについて説明する．また本論文では，スケジュール生変更されたときの値を max f lyapp : D → N とすると，成時間を短縮するために，複数の通常マス内部のスケmax f lyapp (d) = ⌊max f ly(d)/(2 ∗ max(km , kn ) +ジューリングを並行して行う．そのため，隣接していmin(km , kn ) − 1)⌋ となる．これは，元の飛行時間る抽象通常マス同士の内部のスケジュールの整合性の上限を抽象通常マスにおいて同じ辺から入っが合わない場合が存在する，そこで，抽象通常マス内て同じ辺から出るまでにかかる最大の飛行時間で部のスケジュールの整合性を合わせることで，スケ割ったものである．このとき，時刻の粒度として，ジュールを完成させる方法についても説明する．

app)

kt = 2 ∗ max(km , kn ) + min(km , kn ) − 1 とする．

では，抽象通常マス内部をスケジューリングする方法

5. 1 抽象通常マス内部のスケジューリング

ジュールに変換する．

この節では，抽象通常マスの内部のスケジューリングを行う方法について説明する，．最初に 4 章で得最後に，抽象通常マスの内部をスケジュールするられた抽象化状態のスケジュールから得ることがで際に，モデル検査器に与える LTL 式について説明きる情報について説明する．図 4 は図 2 における B2する．(F-2)，(S-2) はそのまま使うことができる．

マスを表す．ここで，抽象通常マス capp に含まれなまた，(F-1) はスケジューリング対象の抽象通常マい抽象通常マスの集合を Out = C − {capp } と呼ぶ

スがデポに隣接していない場合には，(F-1) の一部ことにする．抽象化状態のスケジュールから，スケを変更する必要がある．具体的には，スケジュールジューリング対象の抽象通常マスと out ∈ Out また対象の抽象通常マスにおけるドローンの位置の最終は depot ∈ Depot を出入りしたときの時刻がわかる．

条件として適切な out もしくは depot を返す関数を

例えばドローン D1 の B2 への出入りは図 3 より，時f inOut : Capp × D → Out ∪ Depot とする．これ

刻 1 に depot から入り，時刻 2 に A’2 へ出て，時刻により，ドローン d は適切な out∗ ∈ Out もしくは5 に A’2 から入り，時刻 6 に depot へ出ることが分

depot にいるときにスケジュールが終了するようにす

かる．

る．これを (F-1)’ とする．さらに，(S-1) は近似スケジュールが生成された時点で必ず満たすので検証する必要はない．しかし，対象の抽象通常マスとその他のマスの出入りの制約を満たすために新たな論理式を追加する必要がある．これを (E-1) とする．
各抽象通常マスにて，(F-1)’，(F-2)，(S-1)，(E-1)の 4 つ LTL 式の論理積の否定を入力として検証を行い，それらを結合したものを図 5 に示す．具体化した時刻において，抽象化状態の時刻 tapp が同じであ図4

図 2 で示した B′ 2 の内部および周辺のマスる部分は枠線の太さを変更している．さらに，赤字で示した部分は，各抽象通常マスの内部を並列にスケ次に，抽象化した状態のスケジュールから抽象通ジューリングしたために，直前の時刻と現在の時刻で常マスの内部をスケジューリングするために，抽象ドローンの位置に整合性が取れていない部分を表し化した時刻におけるスケジュールから具体化したている．

時刻におけるスケジュールへの変換について説明する．ここで，抽象化状態のスケジュールの時刻の集合

5. 2 抽象通常マス同士の整合性のとりかたを Tapp = {0, · · · , happ } とする．抽象化状態の時刻

この節では，並列にスケジューリングして組み合わtapp ∈ Tapp で表されたスケジュールを，時刻 t ∈ Tせたスケジュールの整合性を保つために，ドローンので表されたスケジュールに変換するには以下のよう位置を移動させる方法について説明する．整合性をにする．

保つために，スケジュールのはじめから，すべてのド1. tapp = 0 のとき，t = 0 のスケジュールに変換
する．

2. tapp = 1 のとき，t = 1 から t = kt − 1 のスケジュールに変換する．

ローンについて以下のルールを上から適用するものとする．

(R-1) デポと隣接している通常マスでホバリングしているならば，デポに移動する．

3. 1 < tapp < ha pp のとき，kt ∗ (tapp − 1) から(R-2) 同じ抽象通常マスの同じ辺から入る別のkt ∗ (tapp ) − 1 のスケジュールに変換する．

ドローンが存在し，かつそのドローンも整合性が4. tapp = happ のとき，t = kt ∗ (happ − 1) のスケ取れていないならば，両者の位置を入れ替える．

図5

図 3 のスケジュールを具体化したスケジュール

図6

図 5 のスケジュールを整合性が保たれるように調整したスケジュール(R-3) 隣接している通常マスに移動させる．
(R-4) (R-1)，(R-2)，(R-3) によって移動さ5. 3 冗長な時間の削除

せたあとのスケジュールの整合性を保つために，抽象化した状態のスケジュールを具体化しただけドローンを移動させる．

では，すべてのドローンがホバリングすることによる冗長な時間な時間が発生することがある．そこで，，もし，上記のルールでも整合性を保てなかった場合に整合性を保たせたスケジュールに対して，冗長な部分は，整合性を保てなかったステップの間に整合性をを削除する方法について説明する．その方法は，抽象保てなかったドローンのみを移動させるステップを化状態の 1 ステップごとに，各抽象通常マスにいる挟むことで，整合性を保つ．上記のルールに従ってすべてのドローンがホバリングしている時間を取り，整合性を保つように調整したスケジュールを図 6 にその最小値の分だけ各ドローンのホバリングしてい示す．(R-2) を適用した例としては，時刻 20 における部分を削除するというものである．ただし，ホバリるドローン 3 とドローン 5 の交換が挙げられる．まングしている時間を削除し，その結果ドローンが別のた，(R-3) を適用した例としては，時刻 5 における通常マスに移動することにより，各通常マスのドロードローン 3 や時刻 10 におけるドローン 1，ドローンンの台数が最大数に到達する場合には，削除しようと2，ドローン 5 などが挙げられる．

した長さから 1 引いた値で再度削除を試み，0 になった場合には削除は行わない．この削除によって，図 6

の冗長な部分を削除したスケジュールを図 7 に示す．

ジューリングを成功させることができた．

削除した例としては，時刻 5 から時刻 9 ではすべて

今後の課題としては，抽象化を複数段階行う必要ののドローンは少なくとも 2 単位時間分ホバリングしある大規模な飛行エリアでも本論文の提案手法を適ているので，スケジュールの長さを 2 単位時間分削用したいと考えている．また近年，荷物の輸送量が増除できる．冗長な部分を削除した結果，厳密解とのス加する中で，複数のドローンが隊列を編成して 1 つケジュールの長さの差は 7 となっている．の荷物を運ぶような新しいドローン物流システムが開発されている．このような隊列飛行する物流システムでは，ドローンの台数が多くなったり，ドローンの隊列の編成の要素が加わったりすることで，調べる状態数が増加することが懸念される．このように，ドローンの台数が増えたときにも，モデル検査法によるスケジューリングが可能となるような抽象化の方法の研究も行なっていく予定である．

参 考 文 献図7

図 6 のスケジュールから冗長な部分を削除したスケジュール

6 結論と今後の課題
本研究では，モデル検査法によるドローン物流システムの近似スケジューリングの手法を提案した．その具体的なアイディアは，ドローンの飛行エリアを区切る複数のマスを 1 つの新しい大きなマスへと変換することで，状態数を減らすというものである．さらに，その大きなマスの内部のスケジューリングを行うことで，スケジュールの近似解を生成することができる．この手法により，モデル検査法ではスケジュール生成が難しかった規模の物流システムでも，スケ[1] G. Behrmann, K. G. Larsen, and J. I. Rasmussen.: Optimal Scheduling Using Priced TimedAutomata, SIGMETRICS Performance Evaluation
Review, vol. 32(4),2005, pp. 34–40.
[2] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi.: Uppaal - a Tool Suite for Automatic Verification of Real-Time Systems, International Hybrid Systems Workshop (HS 1995), 1995,
pp. 232–243.
[3] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman,and Y. Zhu.: Bounded Model Checking, Advancesin Computers, vol.58, 2003, pp. 118–149.
[4] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio,A. Mariotti, A. Micheli, S. Mover, M. Roveri, andS. Tonetta.: The nuXmv Symbolic Model Checker,
26th International Conference on Computer Aided
Verification (CAV 2014), 2014, pp. 334–342.
[5] A. Cimatti, E. Clarke, F. Giunchiglia, and M.
Roveri.: NuSMV: A New Symbolic Model Verifier,11th International Conference on Computer Aided
Verification CAV 1999, 1999, pp. 495–499.
[6] E.M.ClarkeJr., O.Grumberg, D.Kroening, D.Peled,and H.Veith.: Model Checking (2nd edition), TheMIT Press, 2018.
[7] A. Fehnker.: Scheduling a Steel Plant with
Timed Automata, 6th International Conference on
Real-Time Computing Systems and Applications(RTCSA 99), 1999, pp. 280–286.
[8] G.J.Holzmann.: The SPIN Model Checker Primer and Reference Manual, Addision Wesley,2004.
[9] T. C. Ruys.: Optimal Scheduling using Branch
and Bound with SPIN 4.0, Interna- tional SPIN
Workshop on Model Checking of Software (SPIN2003), 2003, pp. 1–17.