【研究分野】情報学基礎

【研究領域課題番号】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千円)

【研究分野】計算機科学

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

【研究キーワード】

タイプ理論 / 線形理論 / 項書換理論 / プログラミング言語理論 / 証明論 / 形式仕様・形式検証 / 高階項書換系 / 実時間システム / 線形論理 / プログラミング言語 / 並行計算 / 正規化定理 / 相意味論 / 証明の正規化定理 / (強)停止性 / 計算モデル / 高階論理 / カット消去定理 / セマンティクス / 実現可能計算量

【研究成果の概要】

第1年度(平成9年度)においては一般的な論理体系の正規化定理の分析に対する意味論的方法論を確立した。申請者が与えた意味論的方法はGirardが線形論理の証明可能性概念を捉えるために導入した意味論を、証明の正規化定理のための意味論に造り替えて得られたものである。第2年度において、タイプ推論機構をタイプ付き関数型言語のプログラミングパラダイムと抽象データ型の発展的定義構造を持つ対数的仕様言語のプログラミングパラダイムを結合したマルチ・パラダイム言語の計算モデルを我々の意味論的枠組みを応用して構成した。この目的のためには、タイプ付き関数型言語の経産婦デルである高階(タイプ付き)ラムダ計算と代数的仕様言語の計算モデルである項書換え系との融合による統一的な計算モデルの確立が重要である。我々は第1年度に確立した意味論的手法で、高階ラムダ研鑽の正規化定理と項書き換え系の正規化定理を統合した融合言語に対する正規化定理を証明し、これによって融合言語の計算モデルを確立した。第3年度においては、第2年度までに形成されたマルチ・パラダイム・プログラミング言語の計算モデルをさらに線形論理の計算モデルと融合することにより、線形論理のプログラミング・パラダイムと取り込んだマルチ・パラダイム・プログラミング言語の計算モデルを構成した。そのため、まず線形論理の正規化定理と種々の並行計算プログラミング言語の計算モデルとの関係を確立した。そしてこの成果を用いて第2年目で完成させたマルチ・パラダイム言語の論理エンジンを線形論理に代えることにより、並行計算パラダイムを取り込んだマルチ・パラダイム言語を完成させた。
伝統的論理の正規化定理に基づいた種々の論理的計算モデルが得られるが、ここで得られる計算モデルはどれも伝統的な継起的計算モデルであった。これに対してGirardによって導入した線形論理は計算資源の消費関係を直接表し得る全く新しい論理である。よって、これまで用いたれていた伝統論理に代えてこの線形論理を用いることにより、種々の継起的計算モデルの代わりに種々の並行計算モデルが得られることとなった。この基本的アイデアをプログラミング言語の計算モデルの理論に適用して、伝統的な論理的プログラミング言語(関数型、論理型、等式(代数仕様)型)の計算モデルを構成した。この目的のために、線形論理の正規化定理を我々の意味論的枠組のなかで分析し、線形理論の正規化と並行計算プログラミングの計算モデルの一般論との関係を確立した。

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

【研究期間】1997 - 1999

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