本研究では並行システムを記述,解析するための新たな形式モデルを提案し,その理論的考察を行った.本論文ではこの新モデルをcausal event structureと呼ぶが,causal event structureは,システムが実行するイベントの間の同時性を十分に考慮にしている点が特徴である.

　動的システムは並列に動作する分散した部分システムからなることが多い.このようなシステムのモデル化には相互排他やデッドロックなどの側面を捉えるために,システムが行うイベントの間のより基本的な因果関係,すなわち,前後関係,独立性,同時性などの概念が必要となる.

　ところが既存のモデルのほとんどは,同時性を不十分にしか捉えていない.それらはイベントは他のイベントと実行時間を共有しないという仮定に基づいているため,以下のような問題を抱えている.第一は,そもそもイベント間の同時性を直接記述するしくみがないという問題である.そのためあるイベント間の同時生起を記述したい場合は,同時生起を表すためのイベントを個別に導入し,更にそのイベントと他のイベントの間の関係を追加しなければならない.このような間接的な方法は非直観的で面倒なだけでなく,同時生起の可能性の数だけ余分なイベントが必要なので,イベントの個数が爆発する危険性がある.第二は,モデルに動作意味を与えるトレースの表現力の問題である.これらのモデルでは,トレースは生起順に並んだイベントの列で与えられるのが普通である.しかしこれではイベント間の独立性(independence)と交互生起(interleave)が区別されない.なぜなら独立したイベント間の同時生起の可能性が無視されてしまうからである.これを無視しないようにすると,第一の問題が生じることになる.これらの問題点は並列計算のモデル化や,プロトコルの仕様記述のような従来の応用分野においてはあまり問題視されてこなかったようで,実際,遷移システム,ペトリネット,HoareやMazurkiewiczによるトレースモデル,event structureなど,よく知られたモデルに共通するものである.しかし例えばマルチメディアのようなシステムにおいては,イベント間の同期は大事な制約条件となる.

　本研究ではこれらの問題を解決するために,イベント間の同時性が十分考慮された新しい形式モデルを提案し,causal event structureと名付けた(以下単にstructureと呼ぶ).この新モデルの主な特徴は以下のとおりである.第一は,イベント間の同時生起が冗長なイベントを用いることなく明示的に指定できる点である.第二は,トレースにおいてもイベントの同時生起が明示的に表されるようにした点である.これは外部観測者の視点においても,独立性と交互生起が区別できるようになったことを意味する.さらに完全性をもつ変形規則の発見により,イベント生起の性質に関する推論が"完全に"可能となったことは,第三の特徴である.

　以下,少しく詳しく説明する.

　本研究において提案するcausal event structureは,event structureの研究に基づいている.event structureとは,並列システムの形式モデルで,イベントの集合およびイベント間の生起条件からなる構造である.1980年代前半にWinskelらによって提案されて以来,イベント間の生起条件に関して様々な拡張がなされるとともに,プロセス代数の意味論やペトリネットの解析などに応用されて発展してきた.

　本研究においては既存のevent structureを拡張し,基本となる生起条件を,従来の前後関係(enablingとdisabling)に同期関係(synchronization)を加えて,3種類とした.これによりイベント間の同時性も含めた様々な性質を,冗長なイベントに頼ることなく明示的に記述することが可能となった.

　またトレースは,従来のイベントの列としてではなく,イベント集合の列として定義した.この種のトレースに現れるそれぞれのイベント集合は,同時に生起するイベント群を表す.これによりトレースにおいても,同時性を明示的に捉えることができようになった.更に,トレース全体の集合をひとつのグラフにより表現する方法を考案し,これをトレースグラフと名付けた.あるstructureのトレースグラフは,そのstructureの可能な動作全体を与える意味モデルである.

　さらに本研究では,structureの変形規則について考察した.あるstructureに対して生起条件を追加したり削除したりすると,大抵そのstructureのトレースグラフは変化する.しかし,そのような変化を生じさせることなく,追加や削除が可能な生起条件が存在する.変形規則とは,あるstructureに対して,そのトレースグラフを保存しつつ生起条件の追加や削除を行なって,形の異なるstructureを導くための形式的規則のことである.

　変形規則はイベント生起の性質に関する推論規則とみることができる.あるstructureに対し,変形規則を適用して追加することが可能なイベント間の生起条件を考えよう.これはそれまで陽に得られていなかった条件が,変形規則によって導出されたものとみることができる.つまり変形規則によって追加可能な生起条件は,すでにあった生起条件によって含意されるものなので,追加してもトレースグラフが変化しないのである.こうした操作により,イベント生起についての可能性/不可能性,前後関係,同時性,排他性といった性質を,与えられた生起条件から形式的に導くことができる.

　変形規則には様々なものが存在するが,それらの中でもある互いに独立な6つを基本変形規則として特定し,基本変形規則の完全性の証明に成功したことは本研究の主な成果のひとつである.この場合の完全性とは,任意の変形規則は基本変形規則から導かれる,すなわち,等しいトレースグラフをもつ2つのstructureは,一方から他方へこの6つの基本変形規則のみを用いて変形可能であることを意味する.つまりこれは,2つのstructureが動作的に等しいかどうかが,実際の振舞いを調べることなく形式的に決定司能であることを保証するわけであるから,モデルにおいて極めて望ましい結果である.また前述のイベント生起の性質に関する推論も,"完全"に可能であることがわかる.例えば生起不可能なイベントは,必ず基本変形規則のみによって検出できるのである.ここで問題となるのは,変形規則の効率的な適用方法である.本研究では,生起条件とトレースグラフの間に成り立つある関係を得ることにより,変形規則を適用するためのアルゴリズムを構築することに成功した.

　本モデルの記述力については,それがトレースグラフに関して十分であることも証明した.つまり,トレースグラフとなるために必要なある最小限の条件をみたす任意のグラフに対して,そのグラフをトレースグラフとしてもつようなstructureが常に構成可能であることを示し,その方法を与えた.さらに具体的な記述例として,従来のモデルでは複雑にしか表現できなかったイベント生起に関する条件が本モデルにより比較的簡単に記述できるものを挙げた.例えば,あるイベント集合中,実行可能なイベントの最大個数や,同時生起可能なイベントの最大および最小個数の指定方法などである.また,2つのイベント群の間における実行順序の指定方法についても述べた.つまり2つのイベント群に対して,一方の実行開始は他方の実行開始よりも早い,一方の実行開始は他方の実行終了よりも早い,一方の実行開始は他方の実行を停止する,などの条件指定が簡単に記述できることを示した.

　今後の研究においては,structureに関するより詳しい性質を記述,推論するために,モデルに様相論理を組み込むことが課題の一つである.現段階において上述のように,変形規則がstructureの性質における推論規則としても役立つことがわかっている.この方法は,仕様の記述と検証をcausal event structureという一つの枠組の中で行えるという点においてシンプルでよいが,扱える性質の記述力には限界がある.これに対して,様相結合子を組み込むことによりより高度な性質の記述が可能になると期待される.さらに再帰的なシステムの記述のために,無限個のイベントを扱えるようにstructureを拡張することが必須であると考える.また従来の研究に見られるように,structureの時間や確率による拡張も興味深い.

　本論文は、並行システムを記述・解析するために、causal event structureと名付けた新たな型式モデルを提案し、その理論的な考察を行ったものである。

　並行して動作するシステムのモデル化では、排他制御やデッドロックなどの側面を捉えるために、システムが行うイベントの間の因果関係として、たとえば、前後関係、独立性、同時性などの概念が必要となる。特に、マルチメディアの動作のモデル化では、複数のイベントが同期して起こることに意味があり、同時性が重要となる。ところが、従来の遷移システム、ペトリネット、event structureなどのモデルで使われて来た、擬似的なイベントを導入したり、便宜的にイベントに前後をつけて表すインタリーブモデルなどでは、同時性を十分扱えないという問題があった。

　本論文では、同時性を正面からとりあげ、従来のevent structureで扱われてきたイベント間の生起条件(先行関係、競合関係)に同時性を加えた3種類の関係を用いて生起条件を記述するcausal event structureを提案している。このモデルでは、イベントの交互生起と独立生起を書き分けることができるだけでなく、実行可能なイベントの最大個数の指定、同時生起可能なイベントの最大や最小個数の指定、2つのイベント集合の間の実行順序の指定、たとえば、あるイベント集合の実行開始は他のイベント集合の実行開始より早い、などの多くの条件が簡潔に記述可能であることを示した。

　つぎに、イベントの生起結果であるトレースを、同時生起を書くことができるように拡張し、与えられた生起条件を満たすトレースの全体をトレースグラフとして定義した。そして、トレースグラフにより生起条件の意味を与えるとともに、この意味に関する生起条件の「完全」な変形規則の構成に成功した。完全性を持つ変形規則は、従来のevent structureの研究で示されたものはなく、画期的な成果といえる。これにより、生起条件の形式的な変形により、冗長な生起条件を除いていくことが可能となった。さらに、causal event structureの生起条件がトレースグラフに関して「完全」である、つまり、任意のトレースグラフに対して、それを意味とする生起条件が構成できることも示している。このことは、causal event structureの生起条件の記述力が十分強力であることを示している。　以上のべたように、本論文は、並行システムの記述・解析のために、記述力にすぐれ、かつ、良い性質を持つモデルを提案していると言え、この分野に広く貢献していくものと考えられる。以上のことから、本論文は博士(学術)の学位論文としてふさわしいものであると審査委員会は認め、合格と判定する。