共同研究・競争的資金等の研究課題

我々の研究の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築等の形式仕様・形式検証に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。 我々の方法論がダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して有効であることを示した。また、神戸大学田村研究室グループからの協力も得て、我々の理論の実装を論理型プログラム言語上で進めた。これまでの理論的研究と実装的研究の統合も行った。 論理的形式検証の方法論を認証プロトコルの安全性検証にも応用してきた。認証プロトコルの論理的検証においても、attackersの参入や新しい認証子の発行等のようなシステムのダイナミックな変化を捉える方法論を確立することが重要である。昨年度の準備研究の成果を踏まえて、protocol logicsの論理的分析を中心として、論理的検証の方法論の具体的応用を与えた。 また、特に、認証プロトコルのagreement properties検証に関するprotocol logicの基本部分を一階述語論理上で再構成し、その完全性定理及び反例生成系を与えた。この理論の応用のための反例生成系の実装試作も行った。認証プロトコルの安全性検証に関する実時間解析の手法の研究も進めた。

線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する我々のこれまでの成果をもとにして、論理的手法による実時間システム検証の理論の研究を進めた。我々の論理的検証理論は、次のような特徴を持つものとなる。 1.体系的で論理的な形式仕様の方法論及び、実時間システムの安全性・リアクティヴ性、種々のスケジューリング問題等の自動検証の方法論である。 2.ダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対する有効性である。エージェントの数が増加したり時間制約が動的に変化したりするような、ダイナミックで現実的な実時間システムに応用できる論理的検証ツールが実現できる。 3.一部に危険な状態が生じ得ることが分かっている実時間システムのなかで、システムの仕様にどのような手直しをすれば安全になるかを我々の論理的推論体系を用いて分析するツールの開発である。 又、我々の理論の実装にあたっては、フランス側INRIA-LRI-LIXグループとともに論理的形式仕様・検証言語Coq-System上で行なった実装試作を基盤として用いた。実装試作は日本側(岡田)が我々の理論的成果に基づいて検証手続の基本部分の具体的アルゴリズムを理論から抽出して進められた。この実装作業はCoq-グループの2人の大学院生により進められた。岡田-Jouannaudが共同指導教員となりこの作業を進めている。研究協力者神戸大田村グループと論理型言語を使った実装も行なった。又、この新しい方法論の実践的な応用を目的にした研究(特に、実践的な実時間制約や時刻認証を含んだ枠組での認証プロトコルのセキュリティ分析など)の準備を行なった。このために認証プロトコルの論理的検証理論や通信プロトコルの時間制約の論理的分析についての研究を進めた。

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

次の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回の成果報告会を日仏共同で行った。

特定領域研究及び国際共同研究「新しい論理学の展開」に向けた企画・調査を行った。本企画・調査研究班は、論理哲学者達だけでなく、これに認知言語学者、論理学史学者、情報科学者等も含めて形成されている。特に本年度は国際共同研究の基礎となるネットワーク作りを発展させた。 (1)企画にあたっては英米系論理哲学の分野だけでなく、認知科学・情報科学・AIなどとの学際的分野や、西洋・東洋論理哲学史や現象学的論理学をはじめ広い意味での論理の哲学的解明に関わる分野も視野に入れて進めた。又、我々哲学系論理学グループが中心となり、これに情報科学系AI及び認知科学系、数学基礎論系研究者達を交えてオントロジー工学、現象学的論理学、線形論理学等の分野を中心に学際的企画研究を進めた。 (2)哲学系論理学グループを中心に欧州及び北米の研究グループとの協議を進め、欧州グループおよび北米グループとも協力して特定領域研究を立ち上げるための調査を進めた。なお、欧米の企画グループGirard及びJoinet及びAbrusciとは欧州の論理哲学界との研究協力の企画を行った。Benoistらとは各々のグループと現象学的論理学の共同研究企画を行った。又北米の論理学者達との間でも調査を進め、特にScedrov.Mitchell等の北米の重要な論理学グループが来日して協議を行った。

論理的手法による実時間システム検証の理論を情報学的観点から完成させることを本研究課題の目的としている。又この理論の実装に関して現れる情報学的問題を研究してきた。次のような特徴を持つ論理的検証系の理論を構築してきた。 その第1は、実時間システム全体の設計に伴う、体系的で論理的な形式仕様の方法論および、実時間システムの安全性・リアクティヴ性、種々のスケジューリング問題等の自動検証の方法論の開発である。これまでに得られた我々の論理的検証系に対するPSPACE決定性定理を応用してこの方法論を開発してきた。 その第2は、ダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対する有効性の検討である。エージェントの数が増加したり、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証ツールの方法論の開発を進めた。 その第3は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析するツールの方法論の開発である。論理推論体系を(通常、定理自動証明の分野で行われているように)ボトムアップ的に用いると、我々の完全性定理を適用することにより、論理的に証明できない命題に対しては、その反例がシステマティックに生成される。この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると、その反例となるプロセススケジュール(プラン)、即ち安全なブロセススケジュール(プラン)の具体例が自動的に生成・枚挙される手続きが得られるのである。この考え方に基づいて、与えられた実時間システム内での種々のプラニングの問題の論理的な分析ツールの方法論を開発した。

特定領域研究及び国際共同研究「新しい論理学の展開」に向けた企画・調査を行った。本企画・調査研究班は、論理哲学者達だけでなく、これに認知言語学者、論理学史学者、情報科学者含めて形成されている。各々の分担者が各自の専門分野を担当する形で、特定領域研究の企画を進めた。 1.企画にあたっては英米系論理哲学の分野だけでなく、認知科学・情報科学・AIなどとの学際的分野や、西洋・東洋論理哲学史や現象学的論理学をはじめ広い意味での論埋の哲学的解明に関わる分野も視野に入れて進めた。本チームメンバー(および研究協力者グループ)との研究会を重ねて各分野から出された共同研究の企画を検討した。又、我々哲学系論理学グループが中心となり、これに情報科学系AI及び認知科学系、数学基礎論系研究者達を交えて「哲学と工学におけるオントロジー」ワークショップ、「ヒルベルト」国際ワークショップ、「ウィトゲンシュタインの数学の哲学」ワークショップ等多数の研究会を行い、学際的企画研究を進めた。 2.哲学系論理学グループを中心に欧州及び北米の研究グループとの協議を進め、欧州グループおよび北米グループのそれぞれの地域での研究費申請と連動して、日本側も特定領域研究を立ち上げるための準備を進めた。なお、欧米の企画グループvan Dalen及びJoinet及びAbrusciとは欧州の論理哲学界との研究協力の企画を行った。Benoistとは各々のグループと現象学的論理学の共同研究企画を行った。Girard及びBarendregtとは欧州の惰報論理学界との共同研究企画を行った。Mancosu及びZach及びDrummondとは北米論理哲学界との共同研究の企画を行った。Vandervekenとは北米の言語行為論者達および「AIの論理」研究者達との研究協力の企画を行った。

申請者がこれまでに確立した、線形論理に基づいた(有限状態)稠密実時間並行システムの仕様・検証の形式的体系に対する、(1)証明のPSPACE決定可能性と、(2)発展的実時間システムの検証に対する適応性と,(3)(表示的意味論に対する)完全性いう3つの結果を用いて、論理的手法による実時間システム検証の理論を完成させた。特に、我々の枠組みでは、ダイナミックな変化を許す進化的、発展的実時間システムの安全性、リアクティヴ性、種々のスケジュール問題の自動検証、解析が可能である。エージェントの数が増加したり(例えば、鉄道交通網のある状況のもとで臨時列車をダイヤに組み入れたり)、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証ツールをわれわれのこれまでの理論的成果に基づいて実現するための準備研究を行った。又、我々の論理的検証系は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、安全なスケジュールを自動的に探し出したり、与えられた条件を満たすスケジュールを自動的に探しだすことを可能とする。 フランス国立情報科学研究所と共同で申請者の理論の中核部分の実装試作を行ってきた。この試作された論理的検証系FATALIS Systemが来年度の日本側の上記実装研究の基盤として用いられる。

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

本年度は、第1年次に開発した論理的理論を基にした仕様、検証の有効性を確かめ、仕様、検証の新しい論理的方法論を開発した。とくに、まず実時間システムの研究分野でベンチマークとして使われている代表的な実時間システムの具体例を発展的システムの例に変形し、これに我々の方法論を適用し、われわれの論理的な方法論とこれまでの他の方法論とを比較した。(例えば、今までの静的な交通網モデルを、新たに交通網が複雑化したり、電車の本数が変化したり、列車ダイヤの改定や時間制約の変化が起こったりする進化的モデルに作り変えて検討した。) とくに、これまでのPVS言語やTLA言語などで代表されるような、伝統的な述語論理に基づいた論理的手法では、述語論理の表現力を用いて形式仕様が可能であるが、これらPVS言語やTLA言語の(および、その他の述語論理に基づく)枠組では、一般に証明可能性問題が非決定的であるため、形式的検証を体系的に遂行することができなかった。そこで彼らは、この言語使用者の責任において、与えられた形式仕様に特有な種々のInvariant Propertiesを見つけだし、それをもとに多重の数学的帰納法を適用して、検証の論理的証明を構成する、というアドホックな方法を採用していた。しかし現実の問題として、少し規模が大きな実時間システムを設計しようとすると、このような適当なInvariant Propertiesを一般の設計者自身が自分の責任で見いだすことは不可能であるのが実情である。これに対して、我々の線形論理に基づいた論理体系の枠組みは(PSPACE)決定可能であるので、仕様された実時間システムの安全性検証の証明構成(または危険性の証明構成)が自動的に遂行できる。この違いを具体的な例を用いて分析した。

特定領域研究「新しい論理学の展開」及びそれと並行して行う国際共同研究に向けて,その準備のための企画・調査を行った.現在進みつつある新しい論理学の展開を把握し,論理学の進むべき方向を明らかにしていくには,哲学系論理学者達が中心となり,これに西洋・東洋の論理学史の学者達および認知科学,言語学,人工知能論,情報科学基礎論,数学基礎論を含めて特定領域研究チームを形成する必要がある.このため,本企画・調査研究においても,論理哲学者だけでなく,これに認知言語学者,論理学史者,情報科学者に加わってもらった. 昨年度に引続き,岡田は論理哲学(数学基礎論やフッサール後期の論理学も含む)を,飯田は言語分析哲学を,野矢は日常言語と論理との関係を,土屋は認知科学的立場からの論理を,岩田はおもに印度論理を中心に企画調査を行った.また,これらのメンバーの各々は,哲学以外の他の分野との交流も盛んに行ってきた.例えば,土屋は言語学界および認知科学界においても哲学的立場から多くの成果をあげており,また 岡田及び佐藤は人工知能論や情報科学や数学との境界領域の研究者達との打ち合わせも進めてきた.また,これまでも哲学系の研究代表者岡田と分担者土屋は情報科学系の分担者佐藤と分野を超えて本企画調査のための学術交流を重ねてきた. これと並行して,岡田が海外における代表的な哲学系論理学の共同研究プロジェクトの視察・調査を行った.特に4月にソルボンヌ大(パリ大学第1校)哲学科において欧州側共同研究者達と共同研究企画のための会合を行ったのに続いて,7月末のヨーロッパ論理学会の折には米国側の共同研究者達も含めて上記課題の国際共同研究の企画会議を行った.

一貫した論理体系に基づき,適応性と汎用性に優れ,かつ自動化の容易な安全性検証技術を実現することを目標に研究を進め,振舞仕様に基づく以下のような技術を開発した. (1)未知ウイルス検知技術:振舞仕様の理論的枠組に基いてプログラムの挙動をモデル化することで,プログラムの安全性(=ウイルスで「あること」ならびに「ないこと」の判定)を論理的に解析し,自動的に検知する枠組を提案し,処理系を作成した.具体的には,Microsoft社のWindows OS上のプログラムを対象として,未知ウィルス検知ソフトウェアを作成し,開発した技術の有効性を示した. (2)振舞仕様に基づく安全性検証技術:システムの安全性(safety)を,よりユーザーやアプリケーションに近いレベルで検証する技術として,システムの要求や仕様を振舞(behavior)レベルで定式化し,それに基づきシステムの安全性をよりユーザに近いレベルで検証し得る技術を研究開発し,それを鉄道信号システム,コンポーネントウェア,並行分散システム,安全プロトコルなどに適用し,その有効性を示した.特に電子商取引プロトコルに付いては,実規模のプロトコルの検証を行った. (3)振舞仕様に基づくモデル検査技術:システムの要求や仕様を振舞(behavior)レベルで定式化し,システムの状態を仕様レベルで自然に抽象化することで,一般には無限状態となるシステムに対しても有効なモデル検査技術を開発し,基本的な並行アルゴリズムにや通信プロトコルについてこの技術の有効性を示した.

種々の量的時間制約を含む並行計算システムに対する形式仕様・形式検証の方法論を線形論理学的手法を用いて与えた。時間制約付き並行計算プロセスを線形論理の証明で記述することにより、論理学的な証明分析手法を実時間並行計算システムの仕様・検証理論に適用した。特に稠密時間の枠組における線形論理的分析法の有効性を示した。又、後半では、種々の具体的な実時間有限状態システムのサンプルに対して我々の仕様・検証の方法論を適応し、方法論の検討・評価を行った。まず実時間システムの具体例(例えば、交通網自動制御システムの形式仕様とその安全性検証、実時間制約つきPhilosopher's Table等)に我々の方法論を適用し、これまでの他の方法論と比較検討した。特に、マルチエージェントの数や時間制約が発展的に変化する並行計算システムの仕様・検証例を用いて、我々の方法論の独自性を考察した。 伝統的な方法論である、時間オートマタ(Timed Automata)によるモデルチェッキングと呼ばれる手法による検証も(PSPACE)決定的であることがこれまでに知られている。これら伝統的モデルチェッキング法との比較も行い、われわれの新しい論理的方法論の特徴を調べた、又、これまでのオートマタを用いたモデル化の段階でしばしば生じるValidationの問題(実時間システムの設計者の最初の意図通にモデル化がなされているかどうかを問う問題)に焦点を当て、われわれの論理的形式仕様の方法論のメリットを分析した。われわれの論理的形式仕様の方法論では、ある形式で記述された仕様から論理的仕様への自動変換が可能である。又自然な表示的意味論(trace semantics)との間で完全性定理が成り立っている。これらの理由により仕様記述の意味が正確に論理的仕様に反映されること、及びこのようなValidationの問題が生じないことを確認した。

特定領域研究「新しい論理学の展開」に向けて、その準備のための企画・調査を行った。現在進みつつある新しい論理学の展開を把握し、論理学の進むべき方向を明らかにしていくには、哲学系論理学者達が中心となり、これに西洋・東洋の論理学史の学者達および認知科学、言語学、人工知能論、情報科学基礎論、数学基礎論を含めて特定領域研究チームを形成する必要がある。このため、本企画・調査研究においても、論理哲学者達だけでなく、これに認知言語学者、論理学史学者、情報科学者に加わってもらった。 岡田は論理哲学(数学基礎論やフッサール後期の論理学も含む)を、飯田は言語分析哲学を、野矢は日常言語と論理との関係を、土屋は認知科学的立場からの論理を、岩田はおもに印度論理を中心に企画調査を行った。また、これらのメンバーの各々は、哲学以外の他の分野との交流も盛んに行ってきた。例えば、土屋は言語学界および認知科学界においても哲学的立場から多くの成果をあげており、また岡田は人工知能論や情報科学や数学との境界領域の研究者たちとの打ち合わせも進めてきた。また、これまでも哲学系の研究代表者岡田と分担者土屋は情報科学系の分担者佐藤と分野を超えて本企画調査のための学術交流を重ねてきた。 これと並行して、岡田が海外における代表的な哲学系論理学の共同研究プロジェクトの視察・調査を行った。また、ソルボンヌ大学哲学科Joinet博士、パリ・エコールノルマールシュープリュールのLongo博士ら欧州の論理学者およびホンコン大学哲学科及び米国テキサス大哲学科Thomason博士らアジア、米国の何人かの分析哲学者や言語行為論の論理研究者らを招いて、本研究企画のためのディスカッションを行い、助言を仰いだ。

第2年次は,申請者がこれまでに確立した,線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する,証明のPSPACE決定可能性と(表示的意味論に対する)完全性という二つの定理を用いて,論理的手法による実時間システムの開発ツールを実装した.われわれのツールは次の特徴を持つ. 1.その第1は,ひとつの実時間システム全体の設計に伴う,システマティックな論理的形式仕様および,われわれの(PSPACE)決定手続きを用いた安全性・信頼性の自動検証が可能である.これは,これまでに得られた上記二つの論理的基本定理を用いることにより直接遂行できた. 2.その第2は,すでに与えられている実時間システムに新たな部分を加えたり,ある部分を変更したりするときに必要となる形式検証の問題や,二つの独立に作られた(安全性がそれぞれに対して保証されている)実時間システムを統合・総合しようとするときに必要となる形式検証の問題である.われわれの論理的な仕様・検証の枠組みは,もともと高度のモジュラー性を有しているので,このような問題に対しても本質的に上記1の方法論を応用することができた. 3.その第3は,一部に危険な状態が生じ得ることが分かっている実時間システムのなかで,ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析する手法の開発である.論理推論体系を(通常,定理自動証明の分野で行われているように)ボトムアップ的に用いると,論理的に証明できない命題に対しては,その反例がシステマティックに生成される.この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると,その反例となるプロセススケジュール(プラン),即ち安全なプロセススケジュール(プラン)の具体例が自動的に生成・枚挙される.この手法を用いて,与えられた実時間システム内での種々のスケジューリングの問題の論理的な方法論が適用できることとなった.このようなことは,これまでの伝統的なモデルチェッキングの手法では不可能なことであった.