滋賀大学経済学部研究叢書第
1
6
号
フ。ロトコルの形式的記述と検証
森 将 豪 著
滋賀大学経済学部研究叢書第
1
6
号
プロトコルの形式的記述と検証
森
井 寺 豪 著
は し が き
並行処理系の形式的記述と検証の問題を研究テーマとし，その具体例として プロトコル (Protocol，通信制御手IJ贋〉をとりあげ、て研究を始めた頃 (1973年 当時〉は，“プロトコル とし、う言葉はきわめて特殊な技術用語であり一部の専 門家にしか知られていなかったが，今やこの言葉は計算機間通信の普及ととも に計算機を使う人達にはよく知られるようになってきた。研究開始の頃は，自 然語で書かれたプロトコル規格の仕様記述および正当性の検証， という一連の 問題は，系統的にはほとんど議論されておらず，プロトコルのプログラム化や 検証等はプログラマーの職人的技量に依存するところが大であった。それが今 日で、は， HDLC手順 (Highlevel Data Link Control Procedures)などは， すでにチップ化されており，今ではOSI(Qpen ~ystems !nterconnection)規 格の仕様を LOTOSや ESTELLE等の記述言語を用いて形式的に記述しよう とする試みさえなされている。隔世の感がひとしおである。近年，データ通信 の発展に伴い，この分野の研究者数も加速度的に増加するとともに，研究の対 象となる問題も複雑多岐にわたってきており，解決すべき問題も山積している。 本書は，この分野の研究途上における筆者の未熟な研究成果にしかすぎないが， わずかに意義があるとすれば，それはプロトコルの記述・検証に関する研究の 繋明期より問題を見続け研究してきた点で、あろうか。これを出発点として，今 後さらに研究に精進する所存ではあるが，忌障のない御批評，御教示を賜わる ことができれば，筆者の望外の喜びである。 本書を刊行するにあたり，多くの方々の御指導を賜わった。ここに記して深 甚の謝意を表したい。大阪大学教授嵩忠雄先生には，まことに博大にして創造 的な御指導をたえず賜わった。また，大阪大学教授谷口健一先生には，終始懇 切なる御指導を賜わり常に励まして戴いた。そして，大阪大学教授都倉信樹先 生，同助教授藤井護先生，同助教授荒木俊郎先生，および，岡山大学教授杉山 裕二先生には，本研究に関して適切な御指導と御助言を戴いた。また，大阪大 学助手東野輝夫先生には，研究分野を同じくする者として，不断の議論を通じて貴重な御意見を戴いた。その他， ここで逐一御尊名を掲げさせていただくこ とはできなかったが，実に多くの方々の御指導御鞭捷を戴いた。ここに，お世 話になったすべての方々に衷心より謝意を表したく思う。そして，本書刊行の 機会を与えて下さった滋賀大学経済学部に対しむより御礼申し上げる次第であ る。 なお，本研究は一部文部省科学研究費補助金(奨励研究 (A) 研究課題番号 56750240， 57750296， 58750281， 59750272， 60750317)の援助を受けた。ここ に，記して感謝する。 1988年12月 森 井 寺 豪
目
次
第1章序論…...・H ・.. 第2章 タイムペトリネットを用いたプロトコルの記述と検証...・H ・...・H ・..6 2. 1 序言・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・62
.
2
諸定義…・…・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・7
2
.
3
実数時間タイムペトリネット...・H ・H ・H ・..…...・H ・...・H ・...・H ・..…1
0
2
.
4
整数時間タイムペトリネットに関する判定問題…...・H ・...・H ・..…1
2
2
.
5
伝送制御手順の検証と問題・H ・H ・..…...・H ・...・H ・...・H ・...・H ・..…1
6
2. 6 未指定の Tへ
T**の決定...・H ・H ・H ・..………...・H ・..…...・H ・..……182
.
7
結言・…・・…...・H ・..……...・H ・...・H ・H ・H ・..………2
2
第3章 プレスブルガ配列式を用いたプロトコルの記述と検証……...・H ・..…2
4
3
.
1
序言……・・・………....・H ・-…...・H・..………2
4
3
.
2
諸定義と問題………...・H ・..……...・H ・-…....・H ・....・H・....・H ・.
2
4
3
.
3
並行処理プログラムの検証…...・H ・...・H ・H ・H・...・H ・...・H ・..……3
0
3
.
3
.
3
.
3
.
3
.
4
3
.
4
.
3
.
4
.
3
.
5
1 Stenningの 抽 象 的 プ ロ ト コ ル … … … …3
0
2
不変式の具体例...・H ・..……...・H ・...・H ・H・H ・...・H ・H ・H ・..……3
6
システムの動的な性質について...・H ・..…...・H・...・H ・..…...・H ・..…3
8
1
進行する抽象的プロトコル...・H ・...・H ・H・H ・...・H ・H ・H ・..……3
8
2 2カウンタオートマトンを模倣する抽象的プロトコル………4
0
結言・.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4
2
第4
章HDLC
手順の代数的記述...・H・..……...・H ・..……...・H ・..…...・H ・..…4
3
4
.
1
序言・…...・H ・………・……・・……・・・………・・・…4
3
4
.
2 HDLC
の代数的記述……...・H ・..…...・H ・..…...・H ・...・H ・H ・H ・..…4
4
4
.
2
.
1
フレームの代数的記述と諸定義………...・H ・....・H・...・H ・.
.
4
4
4
.
2
4
.
3
4. 4 4. 54
.
6
2 1
次局と2
次局の代数的記述…...・H ・...・H ・...・H ・...・H ・..…4
7
HDLC手順の代数的記述の性質...・H ・...・H ・...・H ・...・H ・H ・H ・..55 1 ， 2次局全体の代数的記述……...・H ・...・H ・H ・H・..…...・H ・..……58 検証法・...・・・・・・・64 結言・...65 第5章 代数的に記述された通信プロトコルの静的性質の検証...・H ・H ・H ・..…6
6
5. 1 5. 2 5. 2. 5. 2. 5. 3 5. 3. 5. 3. 5. 3. 5. 4 5. 5 5. 6 5. 7 序言・・・・・・・・...66 諸定義・.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
6
7
1
代数的記述………...・H ・...・H ・-…...・H ・...・H ・-…...・H ・....・H ・-…6
7
2
項書き換え系…...・H ・...・H ・H ・H ・...・H ・H ・H ・...・H ・...・H ・..…6
8
通信系全体の代数的記述・.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
6
9
1
フレームおよび1
次 局2
次局の代数的記述の概要...・H ・..…6
9
2
物理レベルの代数的記述…...・H ・..…...・H ・..…...・H ・..…………7
0
3
通信系全体の代数的記述...・H ・...・H ・...・H ・...・H ・-…・………7
1
通信系全体の代数的記述の性質・...75 検証法・.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
7
7
検証の具体例・...・・・・・・・・79 結言・...・・・・・・・・・・83 第6章 代数的に記述された通信プロトコルの動的性質の検証………...・H ・..84 6. 1 序言・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・84 6. 2 通信系全体の代数的記述...・H ・..………H ・H ・-一…………...・H ・..85 6. 2. 1 抽象的順序機械モデ、ル...・H ・..…...・H ・...・H ・..……...・H ・..……85 6. 2 6. 2 6. 3 6. 3. 6. 3. 6. 42 S
t
e
n
n
i
n
g
の デ ー タ 転 送 プ ロ ト コ ル の 代 数 的 記 述 … … … … …8
6
3
静的な性質の検証…...・H ・...・H ・...・H ・H ・H ・..……...・H ・..……9
2
動的な性質の検証・...・・93 1 テルポラルロジック・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・93 2 動的な性質の検証法...・H ・..………...・H ・...・H ・..…...・H ・..……95 検証例・...・・・・・・・976. 4. 6. 4. 6. 4. 6. 4. 6. 4. 6 _ 5 1 SDTプロトコルが進むための十分条件…...・H ・..…...・H ・..…97 2 局や回線に対する仮定...・H ・...・H ・...・H ・..…'"・H ・...・H ・..…98 3 動的性質の検証に用いる静的な性質...・H ・...・H ・...・H ・..… 100 4 ①，②の証明の概略...・H ・H ・H ・...・H ・...・H ・H ・H ・..…...・H ・..102 5 仮定の無矛盾性.，.・H ・...・H ・...・H ・..……...・H ・...・H ・..…… 104 結言...・H ・..……...・H ・..…...・H ・..…...・H ・...・H ・..…...・H ・H ・H ・..… 104 第7章 代数的手法のトークンリング方式LANへの応用...・H ・..………… 106 7. 1 序言・・・………...・H・...・…・・………...・H ・..………… 106 7. 2 トークンリング方式LANプロトコルの代数的仕様...・H ・..…… 108 7. 2. 1 局の代数的仕様...・H ・...・H ・...・H ・...・H ・..……….，.・H ・..… 109
7
.
2
.
2
リング全体の代数的仕様...・H ・..…...・H ・...・H ・..……...・H ・..1
1
6
7
.
3
局およびリングの仕様のもつ性質とその検証……...・H・..………1
1
7
7
.
3
.
1
性質の記述…………...・H・..……….，.・H ・...……...・H ・..1
1
7
7. 3. 2 検証のための記述…...・H・..……...・H ・H ・H ・..…...・H ・...・H ・..121 7. 3. 3 安全性および相互排他性….，.・H ・...・H ・H ・H ・...・H・H ・H ・..… 125 7. 3. 4 検証作業...・H ・...・H ・H ・H ・...・H ・...・H ・...・H ・....・H・...126 7. 4 結言………...・H・..………・・・……… 128 参考文献…...・H・..………・………...・H ・H ・H ・..………...・H ・-…H ・H ・...1291 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1ili--lili--lili--iiiiiiiill -1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
第1章 序 論
第
1
章 序
論
プロトコルと呼ばれる通信制御手順は，複数のプロセスが非同期的に動作す る並行処理系の一種である。並行処理系においては，系全体として，望ましい 諸性質が保存されているかどうかとし、う問題は重要かつ難しい問題であり，計 算機系/通信系の通信制御や計算機のシステムプログラムに関連してしばしば 現われる。提案された一つのプロトコルにおいて，それが満たすべき望ましい 性質が成立しているか否かは，一見単純な場合でも簡単にはわからないのが普 通である。いわゆる非同期系であるので，相互のプロセスのタイミングの微妙 な差異により結果が全く異なることがあり，考慮すべき場合分けを単純に列挙 することは，実用上しばしば不可能である。このような事情から，プロトコル の厳密な検証のためには，まずプロトコルの形式的な記述が必要で、あり，これ と共に，形式的に記述されたプロトコルにおいて，所期の性質が成立するか否 かの系統的な判定法の考案・開発が重要な課題の一つになっている。 従来，プロトコルの記述・検証法は，有限状態機械を用いる方法とプログラ ミング言語を用いる方法に大別されてきた。前者では，検証問題は，主として 有限状態機械が最終(受理〉状態に到達可能かどうかという観点より議論され てきたが，プロトコルの記述に必要な状態数がプロトコルの複雑化に伴って爆 発的に増加することや，本質的な構造を陽に表現するのが困難である(例えば，8
の代わりに6
4
を法として送受信順序番号を考えても論理構造は不変であるに もかかわらず，その事実が適切に表現されなしうこと，等が記述・検証の際の 問題となっている。後者では，検証問題がプログラム変数に関する所与の述語 が不変式であることを証明する問題として取り扱われているので，整数演算な どを直接利用することができ，前者の方法が有している欠点を免れてはいるが， プロトコルの記述に直接必要のないプログラム要素の意味に依存し，利用する 言語の意味の形式的定義が前提となること(一般にこのような定義自身きわめ て複雑である〉や，処理順序の一意的記述により過剰規定に陥り易いこと，等2 第1章 序 論 が大きな欠点となっており，これらが形式的な検証を困難なものとしている。 上述のような欠点を免れ得る有効な手法のーっとして，代数的仕様記述法が ある。この方法は，状態遷移図等では取り扱いが困難であった送受信順序番号 やパラメータ値の取り扱いを簡単に記述することができ，また，一般のプログ ラミング言語に比べて意味の形式的定義が容易であることなど，上述の欠点を 免れ得る有効な手法のーっと考えられる。代数的仕様記述法は，抽象データタ イフ。の形式的な仕様記述法の一つで、あり，データタイプを特徴付ける幾つかの 演算の聞に成立する関係を“公理"として記述することにより，そのデータタ イプの振舞を定義しようとするものであり，意味の定義が簡潔で，書き手が選 んだ任意の抽象化レベルで、仕様を記述することができる，等の特徴をもっ。こ のため，抽象的な仕様から具体的な関数型プログラミング言語のプログラムま で，同じ代数的枠組みの中で記述することができ，仕様の段階的な実現(具体 化〉が可能である。代数的仕様記述法における検証の問題は，一般に，仕様に 要求される所期の性質が，その仕様を表現する公理系の定理として成立するこ とを示すことである。通常，検証作業は，与えられた仕様の公理系を項書き換 え系とみなして，項を書き換えることにより進められるが，その作業は煩雑で ある。 本書は，プロトコルの記述と検証の問題を， 1) 状態遷移図， 2) プログラ ミング言語， 3) 代数的仕様記述，の三通りの方法により考察したものである。 第
2
章には，タイムペトリネットを用いる記述・検証法に関する研究結果が 述べられている[1.2.3.4¥P
.
M. M
e
r
l
i
n
によって提案されたタイムペトリネット は，並行処理系に関する理論モデ、ルの一つで、あるペトリネットに，時刻に関す る表現機能を付加して拡張したものであり，有限状態機械を簡潔に表現しうる モデ、ルで、ある。タイムペトリネットは，通常のペトリネットでは表現できない 送信データの消滅によるタイムアウトエラーからの回復の機能を表現できるの で，プロトコルなどの記述や正当性の検証に適したモデ、ルで、はあるが，これま でタイムペトリネットに関する基本的な性質はほとんど解明されていなかった。 この章では，まずタイムペトリネットの基本的性質を解明し，タイムペトリ ネットが通常のペトリネットと比べていくつかの点で、大きな能力をもつこと，第1章 序 論 3 通常のペトリネットと異なり代表的な判定問題が一般に決定不能であることを 示している。次いで，プロトコルの正当性の検証に関連するいくつかの判定問 題が決定可能であるための十分条件を示し，プロトコルの検証や構成への応用 の基礎を与えている。 第3章には，プレスブ、ルガ配列式を用いる記述・検証法に関する研究結果が 述べられている[5.6.7.8九この方法は，プロトコノレが通常のプログラミング言語 で記述されている場合，検証すべき所期の性質をプログラム変数等に関する述 語で表し，その述語がプログラムの実行の適当な区切り目で常に“真"である こと，すなわち述語が“不変式"であることを証明することにより検証しよう とする方法である。従来， プロトコルに関する不変式の検証の問題は具体例に よる直観的な取り扱いしかなされておらず厳密性を欠いていたが， この章では， この問題が決定可能な枠組みの中で形式的に議論できることを示している。近 年， プレスフゃルガ論理式の真偽判定の可解性に関する古典的結果が，一定の条 件の下に配列型変数を含むクラスに拡張できることが N.SuzukiとD.Jeffer
-s
o
n
によって示されているが，この章では，配列型変数を含む並列処理プログ ラムシステムを定義し，このシステムにおける所与の述語が不変式であるかど うかの真偽判定が，妥当な条件の下で上述のクラスの論理式の真偽判定の問題 に帰着できることを示すと共に，代表的な N.V. Stenningのプロトコルにつ いて例証している。一方， プロトコノレが進行するか否かのいわゆる動的な性質 についての検証の問題は，一見単純に見える場合でも決定不能であることを示 し，今後の問題点として示唆している。 第4
章には，代数的仕様記述法を用いる記述法に関する研究結果が述べられ ている[10.11.1九代数的仕様記述法は，記述の対象となる系の本質的構造のみを 陽に表現しうる点，および，その一般性において有限状態機械を用いる記述法 よりも優れている。また，代数的仕様記述法は，仕様を公理系として記述する ので，記述言語自体の意味が簡潔にかっ形式的に定義されており，通常のプロ グラミング言語を用いる記述法よりも厳密性において優れている。従って，代 数的仕様記述法は，有限状態機械や通常のプログラミング言語を用いる記述法 の持つ欠点を補いうる記述法の一つであり，プロトコルの仕様を厳密に表現し，4 第l章 序 論 種々の性質を検証するための有効な記述法の一つで、あると考えられる。第4章 では，ハイレベルデータリンク制御 (HDLC)手順を例にとり，代数的仕様記 述法により HDLC手順がごく自然に公理として書き下されること，得られた 記述に関しては，公理系として“矛盾がなく"かっ“不足なく"書カ通れている こと，および，その記述から仕様を実現する順序機械がごく自然に構成できる こと，さらに，代数的に記述されたプロトコルの検証に関しては，代数的記述 の同じ枠組の中で検証法を定式化できる特徴をもつことを示している。 第5章には，代数的記述法を用いる検証に関する研究結果が述べられている [13.14.15則。第4章における記述を基に， HDLC手順を用いて通信を行う通信系 全体の代数的記述を書き，この記述が公理系として“矛盾なく"かつ“不足な く"書かれていることを示すとともに，代数的記述の枠組みにおける一つの検 証法を定式化している。そして，この通信系の代数的記述において成立するい くつかの重要な論理関係式，例えば，通信系全体の動作可能性や
1
，2
次局の 状態変数聞に成立する関係等，のいわゆる“静的性質"の検証を行っている。 これらの諸性質の検証にあたっては，主として構造的帰納法を用いて行い，検 証作業の効率化と確実性を向上させるために代数的仕様検証支援システムを利 用した。この章での記述・検証の方法および支援システムは， AFFIRMの形式 化 お よ び 方 法 に 類 似 し て お り ， 利 用 し た 代 数 的 仕 様 検 証 支 援 シ ス テ ム も AFFIRMシステム同様，主として項書き換え系上での検証を支援するシステ ムではあるが， (1) 所与の項書き換え系の Church-Rosser性や有限停止性を 前提としない， (2) プレスブ、ルガ文の真偽判定機能を有するので，検証の対象 となる式がブール代数や加減算，大小比較，等で表される場合には検証が機械 的に行える， (3) 記述言語の変更に容易に対応可能である，等の特徴を持って いる。 第6章には，代数的に記述されたプロトコルの動的な諸性質の検証に関する 研究成果が述べられている[17.18.19.20J。この章では，抽象的順序機械モデ、ルを用 いて代数的に記述された通信プロトコルにおいて，データ伝送が実際に進行す るといったプロトコルの“動的性質'の検証を行うための手法について述べて いる。その概要としては，先ず，プロトコノレで、許された状態遷移を行って到達第1章 序 論 5 する任意の状態で成り立つ静的な性質(不変式〉や状態遷移の前後の状態で成 り立つ関係を代数的手法により証明し，それらを一定の規則に従ってテンポラ ルロジックの式に変換する。一方，通信回線が機能的に切断されていないこと など，プロトコルの動的性質を議論する上で局や回線に対して課すべき仮定に ついても，テンポラルロジックの式で与える。そして，これらの式およびテン ポラルロジックにおける標準的な公理(推論則〉を用いて，プロトコルの動的 性質を表す述語が真になることを証明する。そして具体的には，この手法を第 3章で述べた Stenningのデータ転送プロトコルに適用し，その進行性を検証 した過程について述べている。 第7章では，代数的に記述されたトークンリングLANプロトコルの諸性質 の検証に関する研究結果を述べ[21，22，23，24，25J 代数的手法が通信プロトコルの検 証にきわめて有効であることを示している。この章では，第4章 第6章の記 述・検証の対象となったポイント・ツー・ポイント型プロトコルよりも，分散 処理志向が強く，かつ，間接的ではあるがネットワーク全体の動作まで規定し ているローカルエリアネットワーク (LAN，Local Area N etwork)プロトコ ルを対象とし，その代数的記述・検証法について議論している。具体的には， 不特定多数のn個の局がリング状に接続されたトークンリング方式LANプロ トコル(IEEE規格802.5)の抽象度の高い代数的仕様を記述し，その仕様が 「安全性
J
(発信局から発信されたフレームはその内容が変更されることなく すべての局に伝達されるか，下流のある局まで伝達されるかのいずれかである とし、う性質〉や「相互排他性J
(リング全体でトークンは一つ， しかもただ一つ しか存在しないという性質)といった予期される性質を満たすことを代数的手 法を用いて検証することにより，代数的手法が通信プロトコルの検証に対して きわめて有効であることを示している。なお， この検証は検証支援システムを 用いて会話的に行われ、導入する補題を選定する課程やその数，検証の過程や それに要した計算機使用時間， 日数等についても詳細に述べられている。6 第2章 タ イ ム ペ ト リ ネ ッ ト を 用 い た プ ロ ト コ ル の 記 述 と 検 証
第
2
章
タ イ ム ペ ト リ ネ ッ ト を 用 い た
プ ロ ト コ ル の 記 述 と 検 証
2.1
序 言
P
.
M. M
e
r
l
i
n
によって提案されたタイムペトリネットC
T
i
m
eP
e
t
r
i
N
e
t
)
[
5
J
は，通常のペトリネットの各t節点に(そのマーキング条件が成立してからの〉 発火時刻の許容範囲を示すラベルC
T
*
，T
*
*
J
C
T
*
，T
叫はo
三五T*
三五T
*
*
を満 たす定数〉を付加したものであり，各t
節点t
jは通常のペトリネットとして マーキング条件が成立した後，時間T
!
を経過すれば発火可能となり，マーキ ング条件が継続して満たされているならば，それが成立後遅くとも時間T
γ
ま でに発火せねばならない。このようなタイムペトリネットは，通常のペトリネッ トでは表現できない送信データの消滅によるタイムアウトエラーからの回復の 機能を表現できるので，実際の通信プロセスを表現するモデ、ルとして適してい る。本章では，タイムペトリネットそのものに関する理論的性質を究明し，タ イムペトリネットで表された伝送制御手順の検証や構成の問題について言及し ている。 まず，セーフなタイムペトリネットの各t
節点のラベルの値および発火時刻 が実数で与えられている場合には，すべての発火系列における各t節点の発火 回数の組み合せの集合が“s
e
m
i
l
i
n
e
a
r
[
2
J
"
とならないことを2.3で示す。従っ て，発火系列の集合は文脈自由言語でもないので円発火系列に関連する種々 の判定問題は一般に解くことが困難であり，又ほとんど否定的な結果となるこ とが予想される。そこで，以下T*
やT
*
*
の値および発火時刻が量子化され ている(整数値をとる〉場合のみを取り扱う。個々のプロセスがそれぞれ専用 のクロック周期を基準に動作し，それらのクロック周期間に微小なゆらぎは あっても，長期的に見れば相対的な“ずれ"がないと考えられる場合は，発火 時刻が整数値をとると考えて議論してよい。 2.4で、は，有界性，被覆可能性， 到達可能性などの判定問題を考察し，必ずしも有界でないp節点が2個存在す第2章 タイムペトリネットを用いたプロトコルの記述と検証 7 ればいずれも決定不能となることを証明している。通常のペトリネットに対し ては，有界性問題と被覆可能性問題は決定可能である[4Jが，到達可能性問題は 未解決である。 一般に伝送制御手順の検証の問題は，それを表現したタイムペトリネットに おいて，特定の p節点にトークンが複数個入ることがないかどうか，特定の マーキングに到達できるかどうか，あるいは，特定のマーキングへ至るような 遷移が決して起こらないかどうかなどのいわゆる到達可能性問題またはそれと 類似の問題となるが，上記の結果は，通信システムにそのサイズが他の成分に 比べて十分に大きくなりうるバッファが2個(送信側と受信側にl個ずつ〉あ れば，その有界性を使わずに議論すれば，バッファ内のデータの個数のみを考 慮しでもそれらの問題は決定不能であることを表している。しかし，必ずしも 有界とならない p節点を高々 1個もつようなタイムペトリネットに対する到 達可能性問題は決定可能であることを
2.5
で説明する。このことは，2
つのプ ロセスが，サイズが十分に大きくなりうる 1個のバッファを共用してデータの 授受を行う場合の検証の問題が決定可能であることに対応する。 一部の t節点の T*や T**の値が未知で，かつ，有界値bが指定されたタ イムペトリネットにおいて，所与の条件(各成分中の値が bを越えず，かつ， 特定のマーキングから特定の t節点は絶対に発火してはならない，など〉を満 たすようにその未知の値を決定する問題に関して，同じ1つのt節点の T*と T**の2個のみが未知の場合には決定可能であることを2.6で証明している。2
.
2
諸
定
義
[定義2.
1
]
ペトリネットをN=
くI
I
，~，E
，Mo>
で表す。ただし，I
I
，Z
は，それぞれp
節点(
p
l
a
c
e
)
，t
節 点 (t
r
a
n
s
i
t
i
o
n
)
の有限集合で，E
は有 向枝(
a
r
c
)
の有限集合である。各枝はt
節点からp
節点へ，またはp
節点か らt
節点へ向かう。同一節点対に対し複数本の枝があってもよい。 M。は初期 マーキングCin
i
t
i
a
lm
a
r
k
i
n
g
)
で，I
I
からN
(非負整数の集合〉への写像で、あ る。もし，p
節点r
j
からt
節点t
j
(あるいはt
節点t
j
からp
節点r
j
)
への枝 があれば，r
j
はt
節点t
j
の入力p
節点(あるいは出力p
節点〉と呼ばれる。8 第2章 タイムペトリネットを用いたプロトコルの記述と検証
口
[定義2.2J 1
1
からN
への写像をマーキングという。集合H
は有限なので， マーキング M をNの上の I1
1
I次元ベクトル (S1' S2， ・・， S I n 1)によって表 すことができる。 M の第i成分の値 SiをM (ri)， riEI1で表す。口
[定義2.
3
J
p節点riから t節点tjへの枝の数を Fi (tj) で， t節点tjか らp節点rkへの枝の数を Bk (tj) で表す。また， F (tj)， B (tj) をそれぞれ 第i成分がFi (tj)， Bi (tj)で、あるような I1
1
I次元ベクトルとする。マーキン グM とt節点 tjに対し ，tjのすべての入力 p節点 riに対してM (ri)孟Fi (tj) ならば， tjは (Mにおいて〉“マーキング条件"が満たされている(+)とい う。通常のペトリネットでは，マーキング条件が満たされているt
節点は発火 することができ，M
でt
jが発火すると，マーキングはM
からM
'
二M-F
(tj)+
B (tj) になる。すなわち，すべての入力p節点riから Fi (tj)個のトー クンを取り去り，すべての出力 p節 点 九 に Bk (tj) 個のトークンを加えるこ とによりM
からM
'
が導かれる。M
でt
jが発火してM
'
になることを M~→ M'と書く。口
[定義2.
4
J
ヱの中の記号の有限長系列全体の集合をr
で表し，長さO
の 空系列をλで表す。マーキング M から M'への発火系列 (firingsequence)σ
t
を次のように帰納的に定義する。 ただし，σ
ε
ヱへt
E~， N I n IはN上の I1
1
I次元ベクトルの集合で、ある。 M~与 M' 全ョ M"ENlnl[M-O'→M"&M"よ今M'J また， M __ A _→M とする。口
[定義2.5J
M _O'→M'なる発火系列σ(σι
ヱ勺が存在するとき，マーキン グM'はマーキング M から到達可能 (reachable)であるという。口
[定義2.6J
ペトリネット N =く1
1
，ヱ，E
，Mo>
において初期マーキング M。から到達可能なマーキングの集合(到達可能集合:reachability set) RN(Mo)
を次のように定義する。 (十):通常，このことを“発火可能 (firable)"といっているが， タイムペトリネットにお ける発火可能性との混乱を避けるため，本章ではこのようにいうことにする。第2章 タイムペトリネットを用いたプロトコルの記述と検証 9
RN (Mo)
全
{MENIIIII ヨ σE~* ， Mo~M} 口[定義
2.7J
ペトリネットN=
くI
I
，~，E
， Mo>が 有 界(
b
o
u
n
d
e
d
)
であ るとは， RN (Mo)に属するすべてのマーキング M に対して，すべての p 節 点 rj について M (rJ豆bが 成 立 す る よ う な 非 負 整 数 bが存在することであ る。特にb=1の場合セーフ (safe)であるとし、う。口
次にマーキング条件の継続とし、う概念を定義する。 [定議2.8J
マーキング M， お よ びMから t節点t'の発火によって得ら れたマーキング M'=M-F (t')+B (tつ に お い て ， 共 にt節 点tjのマーキン グ条件が満たされているならば，t'の発火に際してt
jのマーキング条件は継続 して満たされるという。そうでないときは，t'の発火に際してtjのマーキング 条件は継続して満たされていないという。 特 に，tj二t'のときは，たとえ M お よ び M'に お い て ど の マ ー キ ン グ 条 件 が 満たされていても， t'のマーキング条件は (t'の発火に際して〉継続して満た されていないとする。口
[定義2.9J
タイムペトリネットを(通常のペトリネットと同じく)N
二くI
I
，ヱ，E
， Mo>で表す。ただし，I
I
， ~，E
， Moは定義2.1のそれと同じで あるが，ヱはそれぞれラベル [Tj，T?J (各 Tj，Tγ はo
~玉 Tj 三三 T*t を満 たす定数で， T ?には∞も許す(+)〉をもったt節 点tjの有限集合である。ラベ ノレ [Tj，Tγ]は発火時刻の許容範囲を示す。口
[定義2.10J タイムペトリネットにおいて， t節 点tj (そのラベルは [Tj， T*tJ)が時刻 τ で発火可能であるとは，t
節 点t
jに関して次の条件(1)， (2)が 満たされていることである。 (1) 時刻 τでt
jのマーキング条件が満たされていること。 (+) :すべての t節点について，T*=0， T**二∞の場合が通常のペトリネットに相当する。 (+ +) :すなわち， τFは次の付)， (ロ)を満足するような時刻である。マーキング Mから時 刻 τFにおいて t節点 t'が発火し，マーキング M'になったとする。 ( イ) Mでは tjのマーキング条件が満たされていない。 ( ロ)M'で tjのマーキング条件は満たされており，イからτまでしのマーキング 条件は継続して満たされている。10 第2章 タイムペトリネットを用いたプロトコルの記述と検証 時刻 τ以前で， tjのマーキング条件の最後の成立時刻をイとすると (2) Tj壬τ-τF壬Tγ 更に， t節点 tjの発火に関して次の条件がある。 (3) 発火可能であるときのみ発火できる。
(
4
)
もし発火可能な状態が時刻τ
以降も継続するならば，時刻τ'+T
ヤ 以 前に(その時刻まで1こ，またはその時刻イ+Tγ に〉必ず発火しなけれ ばならない。 上記(
2
)
，(
3
)
，(
4
)
の条件をまとめて，発火のための“時間条件"とし、う。口
マーキング M から時刻 τにおいてt
節点t
jが発火し，マーキング M'に なったとする(発火は瞬間的に起こり，それに要する時間は考えなし、〉。発火時 刻が量子化された整数値のみを取る場合には M'で、新たにマーキング条件が 満たされたt
節点h
については，次の量子化された時刻τ+1
よりマーキン グ条件成立後の経過時間のカウントを始めるものとする。従って ，Tt=0
で あってもh
は時刻τ+1
以降でしか発火できない。また，t
jも次は時刻τ+
1以降でしか発火できない。特に，時刻 τ (そのときはマーキングを M とす る〉においてt
節点 t，'t
"
が共に発火可能であって，時刻τ
でt
節点t
'
が発 火してマーキング M'になったとき M'でも t節点t"が発火可能であれば， 瞬間的に引続いて(その時刻 τで) t"も発火することができる。 [定義2.11] ペトリネットのマーキングそのものを状態とし，その状態か ら，マーキング条件が満たされている各t
節点についてそれが発火して得られ るマーキングへ遷移枝(発火t節点名を付記する〉を設ける。このようにして 作った状態機械をトークン機械C
t
o
k
e
nm
a
c
h
i
n
e
)
とし、う。口
2.3
実数時間タイムペトリネット
ペトリネットのt
節点の集合をヱ{
t
1，t
2，…，t
I~
I }とする。発火系列(+) ωE~* に対し， ω 中に含まれる tj C 1三五 i孟￨ヱ I) の 個 数 を 品 (ω〉と書く ことにし， (十):便宜上，同時刻に発火したt節点も 1次元的に並べてZ上の系列と見ている。第2章 タイムペトリネットを用いたプロトコルの記述と検証 11 ψ(ω)= (詳し (ω)，再
t
，(ω)，・・・，#
t
I ~ I (ω)) と定義する。 一般に，ペトリネットの発火系列 ω 全体の集合を W とし， 'l'= {ψ(ω〉 ￨ωεW}とおく。通常のペトリネットに対しては，有界ならば W は正規集 合になる。一方，タイムペトリネットに対しては，各t
節点のラベノレの値が一 般に実数で与えられているならば，セーフであっても W は正規集合ではなく， 更 に ? はs
e
m
i
l
i
n
e
a
r
[
2
l
で、もない。このことを以下で証明する。 [定理2. 1 ] 各t
節点のラベル [T*，T**]の値と発火時刻が実数をとる ようなセーフなタイムペトリネットにおいて，'l'は一般にs
e
m
i
l
i
n
e
a
r
ではな し、。口
[証明] 図2. 1 (a)のセーフなタイムペトリネットを考える。ただし，同図 中の T~/Tγ の値は有理数ではないように選ぶ。動作開始時刻以後のすべて (a)d
-
t.[T;， T'，d
t
，
r
n
(b) Ot
1t
2 発 火 系 列 T~ <11 T*Z* 2 発火回数:仇 (ω) 存ぷω〉 図2.1 セーフなタイムペトリネットとその発火系列の例12 第2章 タ イ ム ペ ト リ ネ ッ ト を 用 い た プ ロ ト コ ル の 記 述 と 検 証 の発火系列
ω
における t節点 t1およびt2の発火回数的ω)
(
，非t2C
ω
)
C
図 2 . 1 (b)参照〉の比の値札(
ω
)
，再t，C
ω
〉を要素とする点集合Sを考えると， S の集積点のうちで最少のものは明らかに T~/T ヤとなり，この値は仮定よ り有理数ではない。 一方，ψ(ω
〉全体の集合Vがs
e
m
i
l
i
n
e
a
r
であると仮定すれば，'l'はl
i
n
e
a
r
set[2lAiの有限個の和集合U AIで表される。ここで，各Aiは，非負整数上の 2次元ベクトルC
c
<
p
，C
<
J
)
)
，C
a
W
， a~V ，… Ca~~L a~~D E N2が存在して，Al
=
{
C
c
<
p
，C
<
J))十k<P・
C
a
W
，a~V +… +k~! ・ Ca~~L a~~D I k<P， k<J)， ・・，kWEN} の形をしている。従って，すべての ω E W Vこ対するω中の
t
1，t
zの回数の比 仇 (ω ) /九 (ω〉の値を要素とする点集合を考えると，その集積点のうちの最 小のものはすべての定数ベクトルC
a
W
，a
W
)
C
ただし 1五;; j壬r
i
o
1;;五i三五 h)の成分の比aW/aW
の最小のものと一致する。しかも，この値は有理数で ある。しかし， これは前述の議論(集積点の最小値は有理数ではない T~/Tγ の値〉と矛盾する。従って，'l'はs
e
m
i
l
i
n
e
a
r
で は な い 。 .2.4
整数時間タイムペトリネットに関する判定問題
2
.
1
で述べたように，この節以降，各t
節点のラベルの値が整数値で，かっ 量子化された時刻でのみ発火しうるようなタイムペトリネット(以下，整数時 間タイムペトリネットと呼ぶ〉を取り扱う。この節では，整数時間タイムペト リネットN
，初期マーキングMo
について，次のような判定問題を考える。 (1) 有界性問題:与えられた整数時間タイムペトリネット N が有界か否か。(
2
)
被覆可能性問題:マーキングM
fが任意に与えられたとき ，M
孟M
fか つMERNC
M
o
)
なるマーキングM
が存在するか否か。 (3) 到達可能性問題:マーキングM
f が任意に与えられたとき ，M
f がR
N
C
M
o
)
に属しているか否か。 これらの判定問題が決定不能になることを証明するために，入力をもたない 非決定性2カウンタオートマトン(以下2c
a
と略記する〉を導入する。一般に 任意に与えられた2c
a
が停止するか否かは決定不能であることが知られてお第2章 タイムペトリネットを用いたプロトコルの記述と検証 13 り[6J 更に 2caのカウンタの内容が有限である(し、くらでも大きくなること はない〉か否かとしづ問題も決定不能であることが知られている(文献
C9J
のP1の証明参照)(+)。ペトリネットで2caをシミュレートすることに関して は，文献 C1J
で既に議論されているが，そこでの議論の一部をタイムペトリ ネットに適用することにより以下に述べる結果が得られる。 [定理2. 2] 2個の p 節点を除く他のすべての p 節点には， トークンが 高々 1個しか入らないことが保証されている整数時間タイムペトリネットに対 しでも，その有界性問題は決定不能である。口
[証明] 任意に与えられた2caAから整数時間タイムペトリネット Nを作 成し，N
が有界であるための必要十分条件は， 2caA
のカウンタの内容が有 限であることである， ということを示す。ここで， 2 caAを次のようなものと する。ただし，カウンタを C~ (R，二 1，2)とする。 (1) 初期状態S
。をもち，S
。では2個のカウンタC
1，C
2の内容はOとする。 (2) 最終状態Sfをもち， Sfに入れば停止し，それ以外では動き続けるもの とする。 (3) 2 ca Aの基本動作は次の2種類とする。 タイプ1 状態SIにおいてカウンタ C~ に1を加えて状態Sjになる。 タイプ II: 状態 Si においてカウンタ C~ の内容の零判定を行い o で なければC
e
から 1をヲI
¥，、て状態Sjにo
ならば状態Skに なる。 まず最初に， 2ca Aの各状態と 1対1に対応するP節点とカウンタ C1，C2 に対応する p節点(これらの p節点の名前は状態やカウンタと同じ記号を用 いる〉をNv
こもたせる。更に， 2 ca Aの基本動作に対して，次に示すような (+) :与えられた任意のチューリング機械Mと，その1動 作 ご と に 新 し い マ ス 目 に 印 を 付 けにいくように動作変更を行ったチューリング機械M'と， M'をシミュレー卜する 2 caA'の聞には次のような対応関係がある[9J。M
~ A' 停止する ←ー→使用テープ長有限←一一→カウンタの内容が有限 停止しなL時一一→使用テープ長無限←ー→カウンタの内容が無限14 第2章 タ イ ム ペ ト リ ネ ッ ト を 用 い た プ ロ ト コ ル の 記 述 と 検 証
t
節点と枝を付け加える。タイプIの基本動作のそれぞれについて，図2.2の ようにt
節点を1
個ずつ付け加える。これらのt
節点のラベルの値は任意で、よ い(例えば， T*=T**ニ 1とする〉。タイプIIの基本動作のそれぞれについて は，図2.3のようにt
節点を2個ずつ加える。この2個ずつのt
節点にはそ れぞれT52くTi
(例えば， TN*z=TM= 1，Ti
=Tγ= 2)なる関係を満たすよ うなラベルをつける{+)。 Nの初期マーキング Moは， p節点 Soだけが1で残 りの p節点はすべてOであるとする。 Nの作り方より， 2ca Aが状態 SIにあることはp節点SIにトークンが1 C1 Si Sj 図2.2 タイプIの 基 本 動 作 C1 Sj Si Sk 図2.3 タイプ11の 基 本 動 作 (+) :これはt節点tNZとtzに対し， tNZの発火が優先すること[lJと本質的に同じである。第2章 タイムペトリネットを用いたプロトコルの記述と検証 15 個入っていることに対応している。タイプ 11 の基本動作で，カウンタ C~ の内 容が O でないときには TM く T~ ゆえ tNZ が先に発火して状態 Sf へ遷移するの で， Nは2caAのタイプ11の基本動作を正しくシミュレートすることができ る。タイプ Iについては自明である。また， 2ca Aのカウンタ ClI C2の内容 は，それぞれp節点C1，C2内のトークン数に一致している。ゆえに，Nの有 界性問題は， 2caAのカウンタの内容が有限か否かという判定問題と同じにな り，後者は決定不能であるから[3J前 者 も 決 定 不 能 で あ る 。 . [系2. 1 ] 定理2.2のような制限のついた整数時間タイムペトリネット N に対しても，その被覆可能性問題および到達可能性問題は決定不能である。
口
[証明] 定理2.2の証明で作成した整数時間タイムペトリネット Nにおい て， p節点 Sfだけが1で，残りの p節点はすべて Oであるマーキングを Mf とすると ，M
孟M
fかっMε
R
N
CMo)
なるマーキングM
が存在するための必 要十分条件は， 2caAが停止することである。ゆえに被覆可能性問題は決定不 能である。 整数時間タイムペトリネット Nに図2.4のような2個のt
節点を付加して， 整数時間タイムペトリネット N'を作成する。もし， p節点Sfがトークンをも てば，この2個のt
節点を何回か発火することによって， p節点C
1，C
2のトー C) SI 図2. 4 C. C2中のトークン除去用 t節 点16 第2章 タイムペトリネットを用いたプロトコルの記述と検証 クンをすべて取り去ることができる。従って，
ヱ
M(r)=1より N'において rヰCIC， マーキング条件Mfが到達可能であるための必要十分条件は、 2caAが停止す る こ と で あ る 。 ゆ え に ， 到 達 可 能 性 問 題 は 決 定 不 能 で あ る 。 .2.5
伝送制御手順の検証と問題
通常，伝送制御手順をタイムペトリネットで表現したとき 1個のデータや 制御信号はl個のトークンに対応し，パッファやラインに対応する P節点にそ のトークンを置くことによってデータや制御信号が現在どこにあるかを表す。 伝送制御手順の説明に必要なところだけをタイムペトリネットで表現Lた図 2.5においては.P節点P6. P5がそれぞれ送信源，受信源に.P1. P3がそれ ぞれそのパッファに，また.P2. P4がラインに対応している。簡単のため，情 報損失はライン上でのデータの消滅 (t7の発火〉によってのみ起こるものと仮 定 す る と ペ デ ー タ 送 信 (t1発火〉後それに対する受信完了の返事が，正常時 に到達する (t4発火〉までに要する最大時間を経過しても到達しないとき(し、 Pl t1 [ 1， 2 ] P2 。 。 D A 可 l l J q t u-﹁ 1 L 可 ， 4 E L t6 [1， 2 ] ts [ 2， 3 ] P 6 4 [1， 2 P 4 PS ト 一 一 送 信 側 十 ラ イ ン 十 受信側 イ 図2.5 伝送制御手順のタイムペトリネット表現 (+) :ライン上での，送信データの消滅，受信側からの返事用制御信号の消滅，送信側から の問い合せ用制御信号の消滅，の3つを考慮したモデ、ルに対するタイムペトリネッ ト表現が文献[7]に記述されている。
第2章 タ イ ム ペ ト リ ネ ッ ト を 用 い た プ ロ ト コ ル の 記 述 と 検 証 17 わゆるタイムアウトエラー)，
t
節点t
8が発火してデータの再送を行うように 各t節点の発火時刻の値が指定されている。従って，タイムアウトエラーから の回復が正しく行われているか否かは，図2.5のタイムペトリネットの動作を トークン機械の形で記述した図2.6において，t
節点t
8が状態 (P7，P8〉(+)に おいてのみ発火し， (P7' P8)以外の状態では決して t8が発火しないか否かを 調べることによってわかる。このように，伝送制御手順の検証の問題はタイム ペトリネット(トークン機械〉の上では，初期マーキングから定められたマー キングの集合へ到達で、きるか否か，または，与えられたマーキングよりあるマー キングへ到達で、きるか否か，あるいは，それらに到達していなし、かどうか等の， 到達可能性問題，またはそれと類似の問題となる。 [命題2. 1 ] 有界とは限らない p節点が高々 1個しかなく，他の p節点は すべて有界値b
以下の有界な p 節点であるような整数時間タイムペトリネッ トNにおいては，到達可能性問題は決定可能である(++)口
[証明] 与えられたタイムペトリネット Nに対し，入力をもたない非決定性 1カウンタオートマトン (1caと略記する) Aを以下のように構成する。有界 とは限らない p節点を ru とし， ru内のトークン数をカウンタの内容に対応さ せる。その到達可能性が問題にされているマーキングM
fでの ru 中のトーク ン数Mf(ru) と， Nにおける ruからの出力枝の個数のうち大きい方の値を C とする。A
は有限制御部によって，カウンタの内容 (ru中のトークン数〉がC よりも大きいか，または c以下のときは具体的な値0，1，… cのどれで あるかを知っているものとする(有限状態でそのようにできる〉。更に，A
は有 限制御部で， ru以外のすべての p節点内のトークン数(これは仮定より b以 (+) :トークンを有する p 節 点 名 を 列 挙 し て 状 態 を 表 す 。 も し ト ー ク ン が 複 数 個 入 っ て い れ ば ， そ の 個 数 回 だ けp節点を書くものとする。 (十十): 通 信 系 の パ ッ フ ア サ イ ズ が 高 々 数 個 で あ れ ば ， 伝 送 制 御 手 順 を 有 界 な タ イ ム ベ ト リネットで表現して議論してよい。しかし，有界とはいえパップアサイズがかなり 大 き け れ ば ， 有 界 な タ イ ム ペ ト リ ネ ッ ト で 表 現 し て も 判 定 手 続 き な ど の 能 率 の 良 い方法を得ることは難しい。なお，送受信側のノミッフアサイズが1で あ れ ば 通 常 セーフなタイムペトリネットで表現できる。18 第2章 タイムペトリネットを用いたプロトコルの記述と検証 (Pl PS) (P7?:8〉て tsE(P7PS〉 (P7l:3)t (P7P4P5) ) (P7P4PS) (Pl P5)て t 6 J L t 5 2 ( J L
1
t1 7 (P7P2P5) ) (P7 P5) t6 [ 各 マ ヤ グ で 発 火 可 時 移 川 誠 一 た だ し t引
の発火による遷移はデータの消滅が起ったことを示す。 図2.6 図2.5のトークン機械表現 下〉と，その現在時刻のマーキングにおいて，マーキング条件が満たされてい るt
節点のマーキング条件成立後の経過時間C
T
*
や∞でないT
*
*
の最大値ま ででよい。T**=
∞の場合は，経過時間がT
*
を越えていればT
*
を越えてい るとし、う情報だけでよい〉を記憶しておく。そうすれば，lcaA
は量子化され た各時刻で非決定的に可能なすべての発火の仕方でN
の動作をシミュレートす ることができる。マーキングM
fをもつような状態を受理状態と定義しておけ ば，N
におけるM
fへの到達可能性問題は，lca A
が受理状態に到達するか 否かとし、う問題と同じになる。しかるに，後者の非決定性 1カウンタオートマ トンに関するこの問題は決定可能であるから[ベ題意の到達可能性問題も決定 可 能 と な る 。 .2.6
未指定の
T
*，T
*
*
の決定
一部のT
節点のラベルT
*
やT
*
*
の値が未知である整数時間タイムペトリ ネット Nにおいて， Nが以下のように与えられた“[カット条件]"を満たす ように動作するためのその未知のT
*
やT
*
*
の値が存在するかどうかの判定 と，もし存在するならばその中で適切な(例えば最少の〉値を求める問題を考 える。マーキングMのすべての P節点中のトークン数がそれぞれ値b以下であ るとき，単に“M は値 bを越えなし、"といい，そうでないとき，“M は値 b第2章 タイムペトリネットを用いたプロトコルの記述と検証 19 を越えている"という。 [カット条件] (1) 指定されたある有界値bに対し， N は値 bを越えるようなマーキング に到達してはいけない。
(
2
)
N
のトークン機械の値b
を越えないマーキング間の各遷移枝には，それ ぞれタイプC
，D
，E
のいずれかが指定されており，それに従ってその 枝による遷移は次のように行われること(+)。その枝が出ているマーキン グをMとする。 タイプC :Mからこの枝による遷移は絶対に行ってはいけない。 タイプE:Nがこのマーキング M に到達したならば，その履歴にかか わらず M からこの枝の遷移で始まる発火系列が必ず存在す (++) る 。 タイプD:M
からこの枝による遷移を行っても行わなくてもよい，いわ ゆる“d
o
n
'
tc
a
r
e
"
の遷移。口
一般に，値bは例えばバッファ中に格納できるデータ数に対応しており，ま た，データ送信直後のマーキングでは問い合せ信号等を送信するための遷移枝 にはタイプC
の指定がなされている。従ってこの問題は，与えられた伝送制御 手順において，指定されたノミッフアサイズで正しく通信を行うことができ，か つ，タイムアウトエラーからの回復が正しく行われる(各遷移枝のタイプ指定 が満たされる〉ように，そのタイマー(未指定のT*
とT
*
*
)
にセットすべき 値を求める問題に対応している。 [定理2.3]
同一t
節点t
j
のT?
とT
*
j
*
の2
個のみが未知である整数時間 タイムペトリネットにおいて，任意に指定されたカット条件を満たすようなそ れらの値が存在するかどうかは決定可能である。口
(+) :例えば図2.6で，マーキング(P7P2PS)より (P7P3)への遷移はタイプEに属し， (P7 Ps)への遷移はタイプDに属している。 (P7P3)より tsの発火による (P7P2PS)への遷移はタイプc
(タイプCゆえに図 2 6では存在しない〉に属する。 (+ +) :すなわち，必要なら適当な時間を、待てばこの枝の遷移を先にできること。20 第2章 タ イ ム ペ ト リ ネ ッ ト を 用 い た プ ロ ト コ ル の 記 述 と 検 証 [証明] 与えられた整数時間タイムペトリネット N のトークン機械 TNか ら，
T
N の値b
を越えないすべてのマーキングに1
個の死状態(
d
e
a
ds
t
a
t
e
)
を加えたものを状態とするトークン機械 TN'を次のように作る。 TNで値bを 越えないマーキング M からその値を越えるマーキングに至る遷移に対しては， TN'では， M に対応するマーキングより死状態へ遷移枝を設けてその枝をタイ プC
とする。一方，T
N'での死状態以外の状態間の遷移枝は，T
Nのそれに一致 するように設け，タイプの指定はT
Nにおける指定そのものとする。このよう にして，すべての遷移枝のタイプが指定された有限状態のトークン機械T
N'を 作れば，問題は，T
N'において指定されたタイプの遷移が満たされるようなT
!
や T*j*の値が存在するかどうかとし、う問題と等価となる。従って以下では， TN' を対象として議論する。 まず最初に，有界な整数時間タイムペトリネットNが与えられたとき， Nを シミュレートする非決定性2
方向多テープ有限オートマトンA
を構成できる ことを示す。 Aは￨ヱ￨個 (t節点の個数〉のテープ11， 1 2，…， 1 1 ~ 1とそ のヘッド，および有限制御部からなり，各テープは図2.7
の形で与えられる。 入力アルファベットは {a，b， c} で，テープの左端はι
右端は8
のエンドマー T~ T*・Ti ク付である。 t節点tjのT
!
とT
γ
の値はテープ1
jに tab
$の形で与 えられる。特にTヤ=∞のときは， taTjc$で与えられる。有限制御部ではトー クン機械の現在の状態，すなわち現在のマーキングを記憶し，テープ1jのヘッ ドがt
を読んでいれば対応する t節点 tjがマーキング条件を満たさないこと をa
を読んでいればマーキンクゃ条件は満たすが未だ発火可能で、はないことを， bあるいはCあるいは8
を読んでいれば発火可能であることを，特にs
を読ん でし、れば現在の時刻には必ず発火しなければならないことを，示す。すなわち，t
の右隣からヘッドまでのマス目の数は，そのテープに対応するt
節点のマー キング条件成立後の経過時聞を示す。A
はN
の単位時間ごとの動作を以下のようにシミュレートする。現在の時 刻に発火可能なt節点が存在しなければ(すべてのヘッドはt
かa
を読んでい る)，a
を読んでいたすべてのヘッドを 1コマ右へ動かす。発火可能なt
節点， すなわち， bかCかS
を読んでいるヘッドがあれば，非決定的にそのうちの1有 限 制 御 部 1 1 ~ 1 第2章 タ イ ム ペ ト リ ネ ッ ト を 用 い た プ ロ ト コ ル の 記 述 と 検 証 21 テープの{列は， Ti= 6， Tγ=10 T~= 5， Tγ=∞ T 1;1二 3，T1*"2:I=8， の 場 合 図2. 7 非決定性2方 向 多 テ ー プ 有 限 オ ー ト マ ト ンA つ又は同時に発火可能である幾つかの
t
節点を選択し，それらを現在の時刻で 発火させ(特に8
を読んでいるテープのt
節点は必ず発火させ)， Aは次のよ うに動作する。 Aの内部状態はそれらのt
節点が発火した後のマーキングに遷 移する。発火したt
節点およびマーキング条件が不成立になったt
節点に対応 するテープのヘッドはt
記号に戻す。マーキング条件が新たに成立したt
節点 および発火したt
節点で、再び、マーキング条件が満たされているようなt
節点に 対応するテープのヘッドはt
記号の 1コマ右へ動かす。マーキング条件が継続 して満たされているt
節点に対応するテープのヘッドはすべて右へ1コマ動か す。ただし、 Cを読んでいる場合は動かさない。 さて，テープで与えられた Tへ
T**の値がカット条件を満たすような値で あるかどうかを判定するために，A
は次のように，カット条件を満たさないと22 第2章 タイムペトリネットを用いたプロトコルの記述と検証 判断したときに入力テープを受理する。まず， Aはシミュレーションの動作に Tj Tャ Tj T~ 入る前に，入力テープの構成が
r
t
a
-b $ (Tγ=∞ の と き は ね c$)の形 かどうかを調べ，そうでないときは受理する。マーキングM から t節点tjの 遷移枝があるとする。それがタイプEなら，テープ 1jのヘッドがaを読みぺ かつ，他の少なくとも一つのテープのヘッドが8
を読むような状況のときは受 理する。タイプD
なら，何のチェックも行わない。タイプC
なら，テープc
の ヘッドがbまたはCを読むような状況のときは受理する。一部の T*，T**が 未知のとき，カット条件を満たすようなそれらの値が存在するかどうかといっ た問題は，未知のTへ
T**を可変とするすべてのテープをAに与えたとき， Aが受理しないようなテープが存在するかとし、う問題と等価になる。定理2. 3では1個のt
節点のT!，T*tのみが未知数で他はすべて定数である。 T*， T**の値が定数で与えられているテープに関することは，もちろん有限制御部 でできるので，題意の整数時間タイムペトリネット Nは，未指定のTへ
T** の値が1本の入力テープで与えられる非決定性2方向1テープ有限オートマト ンA'でシミュレートできる。 A'の受理集合の補集合が空でないかどうかとい う 判 定 問 題 は 決 定 可 能 で あ る か ら 円 題 意 の 問 題 も 決 定 可 能 で あ る 。 .2.7
結
言 第1章で得られた結果を簡単にまとめておく。 (1) タイムペトリネットに関しては，セーフであっても T*やT**の値お よび発火時刻が実数をとる場合，発火系列の集合は一般に文脈自由言語でもな いことを示した。このことに基づき， T*やT**の値や発火時刻は量子化され， 整数値をとるタイムペトリネットに関する判定問題を議論した。 (2) 整数時間タイムペトリネットに関して，必ずしも有界でない成分が2
個 あれば，有界性，被覆可能性，到達可能性の各判定問題はいずれも決定不能と なることを示した。更に，必ずしも有界でない成分が1個存在するときは，到 達可能性問題は原理的に決定可能であることを示した。 (十):Mで、マーキング条件が満たされているので，ヘッドがt
上にあることはない。第2章 タ イ ム ペ ト リ ネ ッ ト を 用 い た プ ロ ト コ ル の 記 述 と 検 証 23 (3) ただ 1個のt節点の [T*，T**]の値のみが未知のとき，その整数時間 タイムペトリネットが所与のカット条件を満たすような，その [T*，T**]の 値が存在するか否かは決定不能であることを示した。 しかし， タイムペトリネットが所与の条件を満たすような T*や T**の値 が存在するか否かとしみ問題は，未知数が多い場合一般に未解決である。もし，
