Logical Approach

論理学的アプローチ (福田)

分散システムでは各コンピュータは並列に動作し互いに 通信を行います。このため一つのコンピュータのための プログラムが正しいだけでは不十分で、他のコンピュータの プログラムについても考慮する必要があります。 また、コンピュータは互いに通信するため通信のタイミングも 重要になります。例えば、通信相手同士が互いに相手からの 情報を待っていたら、両者は永遠に待ち続けてしまいます。 このように分散アルゴリズムの設計は通常のアルゴリズムと 比較して格段に難しいものなのです。

われわれは論理学の枠組みを使って、分散計算のための アルゴリズムの正しさを事前に証明する方法を作ろうと しています。ただし、普通の論理学では並列性や通信と いった分散計算の特有の特性が十分に表現できません。 そこで、線形論理と呼ばれる新しい論理体系をもとにして、 分散システムの並列性や通信などが容易に表現できる まったく新しい理論体系を構築し、現在、これを用いて 分散アルゴリズムの設計や解析を行っています。