SP-開発者

SP-DEVS は「Schedule-Preserving Discrete Event System Specifications」の略で、シミュレーションと検証の両方の方法で離散イベント システムをモデル化および分析するための形式です。SP-DEVS は、Classic DEVSから継承されたモジュール式および階層型のモデリング機能も提供します。

SP-DEVS は、約 30 年間 DEVS 形式の未解決問題であった元のネットワークの有限頂点到達可能性グラフを取得することを保証することにより、ネットワークの検証分析をサポートするように設計されています。ネットワークのこのような到達可能性グラフを取得するために、SP-DEVS には 3 つの制限が課されています。

1. 事象集合と状態集合の有限性、
2. 国家の寿命は有理数または無限大でスケジュールすることができ、
3. 外部イベントから内部スケジュールを保護します。

したがって、 SP-DEVS はDEVSとFD-DEVSの両方のサブクラスです。これら 3 つの制限により、状態の数が有限であっても、 SP-DEVS クラスは結合に対して閉じています。この特性により、 SP-DEVS 結合モデルであっても、いくつかの質的特性と量的特性について有限頂点グラフベースの検証が可能になります。

システム要件

横断歩道システムについて考えてみましょう。赤信号 (それぞれ歩行禁止信号) は緑信号 (それぞれ歩行者信号) と逆の動作をするため、簡単にするために、図 1 に示すように、緑信号 (G) と歩行者信号 (W) の 2 つの信号と 1 つの押しボタンだけを考えます。一連のタイミング制約を使用して、G と W の 2 つの信号を制御したいと思っています。

2 つのライトを初期化するには、G が点灯するのに 0.5 秒かかり、0.5 秒後に W が消えます。その後、30 秒ごとに、誰かが押しボタンを押すと、G が消灯し、W が点灯する可能性があります。安全上の理由から、G が消えてから 2 秒後に W が点灯します。26 秒後に W が消え、さらに 2 秒後に G が再び点灯します。これらの動作が繰り返されます。

コントローラ設計

上記の要件を満たすコントローラを構築するには、1 つの入力イベント「push-button」（略称 ?p）と、青信号と歩行信号のコマンド信号として使用される 4 つの出力イベント「green-on」（!g:1）、「green-off」（!g:0）、「walk-on」（!w:1）、「walk-off」（!w:0）を検討します。コントローラの状態セットとして、「booting-green」（BG）、「booting-walk」（BW）、「green-on」（G）、「green-to-red」（GR）、「red-on」（R）、「walk-on」（W）、「delay」（D）を検討します。図 2 に示すように状態遷移を設計してみましょう。最初、コントローラは寿命が 0.5 秒の BG から開始します。寿命が過ぎると、BW 状態に移動し、この時点で「green-on」イベントも生成します。 BW に 0.5 秒間留まった後、30 秒間存続する G 状態に移行します。コントローラは、出力イベントを生成せずに G から G にループすることで G に留まり続けることも、外部入力イベント ?p を受信したときに GR 状態に移行することもできます。ただし、 GR での実際の滞在時間は、G でのループの残り時間です。GR から、出力イベント !g:0 を生成して R 状態に移行し、R 状態は 2 秒続き、その後、出力イベント !w:1 を生成して W 状態に移行します。26 秒後、!w:0 を生成して D 状態に移行し、D で 2 秒間留まった後、出力イベント !g:1 を生成して G に戻ります。

上記の横断歩道信号機のコントローラは、アトミックSP-DEVSモデルでモデル化できます。正式には、アトミックSP-DEVSは7つのタプルです。 $${\displaystyle M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>}$$

どこ

• ${\displaystyle X}$入力イベントの有限集合です。
• ${\displaystyle Y}$出力イベントの有限集合です。
• ${\displaystyle S}$状態の有限集合である。
• ${\displaystyle s_{0}\in S}$初期状態です。
• ${\displaystyle \tau :S\rightarrow \mathbb {Q} _{[0,\infty ]}}$は、負でない有理数と無限大の集合である状態の寿命を定義する 時間進行関数です。${\displaystyle \mathbb {Q} _{[0,\infty ]}}$
• ${\displaystyle \delta _{x}:S\times X\rightarrow S}$入力イベントがシステムの状態をどのように変化させるかを定義する外部遷移関数です。
• ${\displaystyle \delta _{y}:S\rightarrow Y^{\phi }\times S}$は出力と内部遷移関数であり、はサイレントイベントを表します。出力と内部遷移関数は、状態がどのように出力イベントを生成するかを定義すると同時に、状態が内部的にどのように変化するかを定義します。^[1]${\displaystyle Y^{\phi }=Y\cup \{\phi \}}$${\displaystyle \phi \notin Y}$

横断歩道コントローラの形式表現

図 2 に示す上記のコントローラは、次のように記述できます。ここで、={?p}; ={!g:0, !g:1, !w:0, !w:1}; ={BG, BW, G, GR, R, W, D}; =BG、(BG) =0.5、(BW) =0.5、(G )=30、(GR)=30、(R)=2、(W)=26、(D)=2; (G,?p)=GR、(s,?p)=s if s G; (BG)=(!g:1, BW), (BW)=(!w:0, G), (G)=( 、G), (GR)=(!g:0, R), (R)=(!w:1, W), (W)=(!w:0, D), (D)=(!g:1, G); ${\displaystyle M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>}$${\displaystyle X}$${\displaystyle Y}$${\displaystyle S}$${\displaystyle s_{0}}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \delta_{x}}$${\displaystyle \delta_{x}}$${\displaystyle \neq}$${\displaystyle \delta_{y}}$${\displaystyle \delta_{y}}$${\displaystyle \delta_{y}}$${\displaystyle \phi}$${\displaystyle \delta_{y}}$${\displaystyle \delta_{y}}$${\displaystyle \delta_{y}}$${\displaystyle \delta_{y}}$

原子 SP-DEVS のダイナミクスを捉えるには、時間に関連する 2 つの変数を導入する必要があります。1 つは寿命、もう 1 つは最後のリセットからの経過時間です。を寿命とします。寿命は連続的に増加するのではなく、離散イベントが発生したときに設定されます。 を経過時間 とします。経過時間は、リセットがない場合、時間の経過とともに連続的に増加します。 ${\displaystyle t_{s}\in \mathbb {Q} _{[0,\infty ]}}$${\displaystyle t_{e}\in [0,\infty ]}$

図 3 は、図 2 に示した SP-DEVS モデルのイベント セグメントに関連付けられた状態軌跡を示しています。図 3 の上部は、横軸が時間軸であるイベント トラジェクトリを示しています。したがって、イベントは特定の時間に発生します。たとえば、!g:1 は 0.5 で発生し、!w:0 は 1.0 時間単位で発生します。図 3 の下部は、上記のイベント セグメントに関連付けられた状態軌跡を示しています。ここで、状態は、その寿命と経過時間と の形式で関連付けられています。たとえば、(G, 30, 11) は、状態が G であり、寿命が であり、経過時間が 11 時間単位であることを示します。図 3 の下部の線分は、経過時間の時間フローを示しています。経過時間は、SP-DEVS で唯一の連続変数です。 ${\displaystyle s\in S}$${\displaystyle (s,t_{s},t_{e})}$

SF-DEVS の興味深い特徴の 1 つは、外部イベント ?p が発生したときに、図 3 の時刻 47 に描かれている SP-DEVS の制約 (3) のスケジュールが保存されることです。この時点では、状態が G から GR に変化しても、経過時間は変化しないため、線分は時刻 47 で途切れることはなく、この例では 30まで伸びます。入力イベントからのスケジュールがこのように保存され、時間の進み方が非負の有理数に制限されるため (上記の制約 (2) を参照)、SP-DEVS モデルでは、すべてののこぎりの高さは非負の有理数または無限大になります (図 3 の下部に示すように)。 ${\displaystyle t_{e}}$${\displaystyle t_{e}}$

SP-DEVSはDEVSのサブクラスです

SP-DEVSモデルは、DEVSであり、 ${\displaystyle M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>}$ ${\displaystyle {\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >}$

• ${\displaystyle X,Y}$のは の と同じです。${\displaystyle {\mathcal {M}}}$${\displaystyle M}$
• ${\displaystyle S'=\{(s,t_{s}):s\in S,t_{s}\in \mathbb {T} ^{\infty }\}}$
• ${\displaystyle s_{0}'=(s_{0},\tau (s_{0}))}$
• 状態が与えられた場合、 ${\displaystyle (s,t_{s})\in S'}$${\displaystyle ta(s,t_{s})=t_{s}.}$
• 状態と入力イベントが与えられた場合${\displaystyle (s,t_{s})\in S'}$${\displaystyle x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.}$
• 状態が与えられた場合、 ${\displaystyle (s,t_{s})\in S'}$${\displaystyle \delta _{int}(s,t_{s})=(s',\tau (s')}$${\displaystyle \delta _{y}(s)=(y,s')。}$
• 状態が与えられた場合、 ${\displaystyle (s,t_{s})\in S'}$${\displaystyle \lambda (s,t_{s})=y}$${\displaystyle \delta _{y}(s)=(y,s')。}$

• タイムライン抽象化の適用性

有限数の状態とイベントとともに入力イベントによって変更されない非負の有理数値の寿命の特性は、経過時間の無限数の値を抽象化することによって、SP-DEVS ネットワークの動作を同等の有限頂点到達可能性グラフとして抽象化できることを保証します。

SP-DEVSネットワークの各コンポーネントの経過時間の無限の場合を抽象化するために、タイムライン抽象化と呼ばれる時間抽象化手法が導入されました[Hwang05]、[HCZF07]。この手法では、スケジュールの順序と相対的な差が保持されます。タイムライン抽象化技術を使用すると、任意のSP-DEVSネットワークの動作を、頂点と辺の数が有限である到達可能性グラフとして抽象化できます。

• 安全性の決定可能性

定性的な特性として、SP-DEVSネットワークの安全性は、（1）与えられたネットワークの有限頂点到達可能性グラフを生成し、（2）いくつかの悪い状態が到達可能かどうかを確認することによって決定できます[Hwang05]。

• 生存の決定可能性

定性的特性として、SP-DEVSネットワークの活性は、(1)与えられたネットワークの有限頂点到達可能性グラフ(RG)を生成すること、(2)RGから、頂点が強く連結された成分であるカーネル有向非巡回グラフ(KDAG)を生成すること、(3)KDAGの頂点に活性状態の集合を含む状態遷移サイクルが含まれているかどうかを確認することによって決定できます[Hwang05]。

• 最小/最大処理時間境界の決定可能性

定量的な特性として、SP-DEVSネットワークにおける2つのイベントからの最小および最大処理時間境界は、(1)有限頂点到達可能性グラフを生成し、(2.a)最小処理時間境界の最短経路を見つけ、(2.b)最大処理時間境界の最長経路（利用可能な場合）を見つけることによって計算できます[HCZF07]。

• 表現力の低下: OPNA 問題

の場合、SP-DEVS モデルの全状態をパッシブとします。それ以外の場合は、アクティブとします。 ${\displaystyle (s,t_{s},t_{e})}$${\displaystyle t_{s}=\infty }$

既知の SP-DEVS の制限の 1 つは、「SP-DEVS モデルがパッシブになると、アクティブ (OPNA) に戻ることはない」という現象です。この現象は [Hwang 05b] で最初に発見されましたが、当初は ODNR (「一度死ぬと、二度と戻らない」) と呼ばれていました。これが発生する理由は、上記の制限 (3) により、入力イベントによってスケジュールを変更できないため、パッシブ状態をアクティブ状態に起動できないためです。

たとえば、図 3(b) に描かれたトースター モデルは、SP-DEVS ではありません。「アイドル」(I) に関連付けられた全体の状態は受動的ですが、トースト時間が 20 秒または 40 秒であるアクティブ状態「トースト」(T) に遷移します。実際には、図 3(b) に示されているモデルはFD-DEVSです。

http://xsy-csharp.sourceforge.net/DEVSsharp/ には DEVS# というオープン ソース ライブラリがあり、安全性と活性、および最小/最大処理時間の境界を見つけるためのいくつかのアルゴリズムをサポートしています。

• [Hwang05] MH Hwang、「チュートリアル: スケジュール保存型 DEVS に基づくリアルタイム システムの検証」、2005 年 DEVS シンポジウム議事録、サンディエゴ、2005 年 4 月 2 ～ 8 日、ISBN  978-1-56555-293-7 (http://moonho.hwang.googlepages.com/publications で入手可能)
• [Hwang05b] MH Hwang、「再構成可能な自動化システムの有限状態グローバル動作の生成: DEVS アプローチ」、2005 IEEE-CASE の議事録、エドモントン、カナダ、2005 年 8 月 1 ～ 2 日 (http://moonho.hwang.googlepages.com/publications で入手可能)
• [HCZF07] MH Hwang、SK Cho、Bernard Zeigler、F. Lin、「スケジュール保持型 DEVS の処理時間境界」、ACIMS 技術レポート、2007 年、(http://www.acims.arizona.edu および http://moonho.hwang.googlepages.com/publications で入手可能)
• [Sedgewick02]、R. Sedgewick、C++ アルゴリズム、パート 5 グラフ アルゴリズム、Addison Wesley、ボストン、第 3 版
• [ZKP00]バーナード・ザイグラー、タグ・ゴン・キム、ハーバート・プレホファー（2000年）。モデリングとシミュレーションの理論（第2版）。アカデミック・プレス、ニューヨーク。ISBN 978-0-12-778455-7。{{cite book}}: CS1 maint: 複数の名前: 著者リスト (リンク)