【研究分野】情報学基礎

【研究領域課題番号】15630002 (KAKENデータベースで見る）

【研究キーワード】

論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論

【研究成果の概要】

これまでの日米共同研究の成果を基にして平成15年度にこの日米共同研究プロジェクトを発展的に継続すべく研究計画の企画を日米間で行った。米国側は本年より同様な企画のため、若い世代に中核メンバーを移行しながら日米共同研究の更新の準備を開始しており、日本側も本企画研究の遂行過程で若手世代に移行していく計画を進めた。現在までは日本側は岡田(慶応大)が、又米国側はScedrov(ペンシルバニア大)、Mitchell(スタンフォード大)が幹事役として共同研究や共同主催国際会議の企画を行い、これら幹事役と同世代の研究者達が井同研究の中核となってきた。(過去3年間に3回の日米ワークショップ及び特定領域「安全」グループ(代表:米澤教授(東大))と連携したソフトウェア安全性に関する国際シンポジウムを開催し、Theoretical Computer Science誌特別号、States-of-Art Series of LNCS (Springer)等を編集し、日米共同研究の成果発表も行ってきた。)今回の企画研究ではこれらの成果やこれまでの共同研究体制を分析し、今後の改良点を検討した。米国側からScedrov、Cervesato、Nuclaらが秋に来日し今後の共同研究の企画立案を行った。特にソフトウェア及びネットワークコミュニケーションの安全性検証のための共同研究の方法論を検討した。我々のソフトウェア検証の論理的方法についての日米共同研究は欧州やカナダ等の研究グループの研究とも深く関連するため、これらの研究グループとも打合せをして我々の研究企画に役立てた。

【研究種目】基盤研究(C)

【研究期間】2003

【配分額】2,100千円 (直接経費: 2,100千円)

【研究分野】ソフトウエア

【研究領域課題番号】15300008 (KAKENデータベースで見る）

【研究キーワード】

論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論

【研究成果の概要】

次の3点を中心に研究を進めた。
1.証明論と意味論の統合的見方について研究を進めた。カット消去定理等の証明論の基本定理の成立条件がPhase semanticsによる意味論的分析により明らかになることを示した。又、Simple logic等の線形論理の基礎理論に対して、証明論と意味論の統合を進めた。さらに、直観主義論理Phase semanticsと古典論理Phase semanticsとの密接な関係を明らかにした。Phase semanticsの成果に基づいてカット消去定理の意味論的条件の研究を進めた。
2.Reduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の確立に向けた研究を進めた。ゲーム論的意味論等の観点からの分析も加えた。(岡田・Girard等フランスグループとの共同研究)これまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にするLudics等の新たな論理体系理論の分析をGirardグループらと共同で行なった。
3.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を示した。この目的でフランス及び米国共同研究グループとの共同研究を行なうとともに、計3回の成果報告会を日仏共同で行った。

【研究種目】基盤研究(B)

【研究期間】2003 - 2005

【配分額】11,500千円 (直接経費: 11,500千円)

【研究分野】計算機科学

【研究領域課題番号】13558031 (KAKENデータベースで見る）

【研究キーワード】

論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論

【研究成果の概要】

我々の形式仕様・検証ツールの設計と実装を進めた。又この仕様検証ツールを用いて、種々の実時間有限状態システムのサンプルに対して仕様、検証のケーススタディを行った。例えば実時間システムの研究分野でベンチマークとして使われている代表的な実時間システムの具体例(例えば、交通網自動制御システムの形式仕様とその安全性検証等)に我々の方法論を適用し、我々の論理的な方法論の有効性を検討した。特に、エージェントの数や時間制約が発展的に変化する並行計算システムの仕様・検証例を用いて、我々の方法論の独自性や特徴を示した。エージェントの数がダイナミックに変化する実時間システムの検証に対応するための実装の設計をフランス側共同研究グループと行った。まずユーザレベルで与えられた仕様は線形論理を用いた形式仕様に変換されグローバルな(例えば状態間の)時間制約をローカルタイマーを用いた時間制約に変換される。この時、この形式仕様レベルでは限定量化子等の意味はその時々の参加するエージェントの集合等に依存してダイナミックに変化することとなる。この形式仕様を使って効率的な検証を行う目的でエージェントの総数や各状態にあるエージェント数等をカウントするカウンターを用いた仕様への自動変換を行う。さらに稠密時間概念の消去手続きを行う。手続きの基礎となる基本定理は先行研究の中でKanovitch-Okada-Scedrovによって与えられていたが、この定理からアルゴリズムを抽出することにより安全性検証(reachability)のための稠密時間消去手続きの実装が行われた。又、このアルゴリズム抽出過程の分析を通じて安全性以外の(例えばAppointment problemや種々のスケジューリング)手続きへの拡張を行った。又、同様な方法論を用いてSecurity Protocolsの安全性検証を行う目的で、安全性検証のための論理推論体系の研究を進めた。又、我々の形式仕様検証言語として採用している線形論理の構文論と意味論に関する関連研究も進めた。

【研究種目】基盤研究(B)

【研究期間】2001 - 2003

【配分額】6,700千円 (直接経費: 6,700千円)

【研究分野】計算機科学

【研究領域課題番号】10044094 (KAKENデータベースで見る）

【研究キーワード】

タイプ理論 / 線形論理 / 関数型言語 / プログラム言語理論 / 証明論 / 形式仕様 / 形式検証 / 実時間システム / プログラミング言語 / プログラム意味論 / 形式的プログラム検証 / 形式的仕様 / 情報科学の論理

【研究成果の概要】

第1年度は線形論理とタイプ理論を組み合わせた線形タイプ言語の計算モデルの理論を確立した。また第2年度は第1年度に確立した計算モデルの理論に基づいて、線形タイプ理論によるプログラミング言語の設計のための理論を構築した。
これらの研究を通じて、線形タイプ理論言語による並行計算プログラミング設計のための理論とこの言語とを用いた並行計算プログラミング方法論を考察した。また、実現可能計算量(多項式時間計算量及び多項式空間計算量)のための意味論的手法の確立、および我々の線形タイプ・プログラミング言語の設計への応用を行った。
線形論理とタイプ理論を組み合わせた線形タイプ言語に基づく線形タイプ・プログラム言語の線形理論証明システムとプログラム自動検証・自動抽出部分の設計の理論も構築した。特に今年度は米国側共同研究者たちとソフトウェアの形式仕様、形式検証のための方法論の開発を行った。また、フランスを中心とした欧州の共同研究者グループとは線形理論的手法のプログラミング方法論への応用に関する手法を共同で開発してきた。これらの成果はわれわれの言語設計に生かされている。
本研究課題で構築した新しいプログラミング言語をもとにして、フランス国立情報科学研究所(INRIA)などと協力して我々の言語の実装を計画している。

【研究種目】基盤研究(A)

【研究期間】1998 - 1999

【配分額】9,500千円 (直接経費: 9,500千円)