Research projects

我々の研究の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築等の形式仕様・形式検証に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。 我々の方法論がダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して有効であることを示した。また、神戸大学田村研究室グループからの協力も得て、我々の理論の実装を論理型プログラム言語上で進めた。これまでの理論的研究と実装的研究の統合も行った。 論理的形式検証の方法論を認証プロトコルの安全性検証にも応用してきた。認証プロトコルの論理的検証においても、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らが秋に来日し今後の共同研究の企画立案を行った。特にソフトウェア及びネットワークコミュニケーションの安全性検証のための共同研究の方法論を検討した。我々のソフトウェア検証の論理的方法についての日米共同研究は欧州やカナダ等の研究グループの研究とも深く関連するため、これらの研究グループとも打合せをして我々の研究企画に役立てた。

Linear logical proof theory and semantics theory have been developed and the researches have reached a matured stage to integrate proof theory and semantics theory. In this project we developed a method of integrating proof theory and semantics of linear logic and related logics. We specially developed a method to study proof theoretic properties using this integrated framework, by using a phase semantic techniques, including the relation between "simple logic" and linear logic, uniform and abstract characterizations of cut-eliminations and logical computation models. We also applied the linear logical syntax and semantics to formal verification techniques on real-time system designs and correctness proof techniques on security protocols as well as to computational complexity theory and type-inference theories for programming languages.

特定領域研究及び国際共同研究「新しい論理学の展開」に向けた企画・調査を行った。本企画・調査研究班は、論理哲学者達だけでなく、これに認知言語学者、論理学史学者、情報科学者等も含めて形成されている。特に本年度は国際共同研究の基礎となるネットワーク作りを発展させた。 (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が来年度の日本側の上記実装研究の基盤として用いられる。

We developed and designed a formal specification and verification tool for dynamic real-time systems in the collaboration with the French partner group (Jean-Pierre Jouannaud's group), based on linear logic. By dynamic real-time systems we mean a multi-agent systems in which the number of participating agents may be changed and the time constraints may be changed dynamically We gave an automated transformation procedure to transform a natural specification on the user-level into a linear logical specification. We also gave an elimination procedure to eliminate the dense time notions from a linear logical specification. Then, various kinds of verifications are performed in terms of the proof-search mechanism of a fragment of linear logic. The dense time elimination procedure is given by a program extraction method known in constructive logic. We also developed a logical framework for the security protocol correctness proofs, applying the same concept. We also studied some related logical research on our linear logic, which is the logical framework of our verification tool.

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

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

The following results have been gotten by doing research for developing the verification technology which is highly applicable and flexible, and is amenable for automation. (1)Inspection Technology for Unknown Viruses : Based on the logics of behavioral specifications, a technology for modeling behavior s of programs and automatically inspecting their safety is developed. A virus inspection program is developed for Windows OS, and the effectiveness of developed technology has been proved. (2) Safety Verification Technology based on Behavior Specification : By formalizing requirements and/or specifications in behavior level, a verification technology is developed which can verify the safety properties of systems in the level which is more honest to users or application logics. The technology has been applied to railway signal systems, software components, concurrent and distributed systems, and secure protocols, and is proved to be effective. In particular, verifications of several practical e-commerce protocols have been done using the technology. (3) Model Checking Technology based on Behavioral Specification : Based on behavioral specifications, a model checking technology which is effective for software with infinite states is developed.

We gave a logical method for formal specification and formal verification of concurrent systems, in particular real-time concurrent systems, which contains quantified time constraints in the dense-time setting. In the first half of the project we gave a concrete algorithm for verification of the basic safety and other related properties (the membership property, the appointment property, the liveness property, etc.) in the dense real-time setting. We also gave a theory of automated transformation from a specification (written in the framework of natural description language) into a linear logical specification. Then in the second half of the project we extended our theories to dynamic real-time systems where the number of agents/participants and the form of time-constraints are dynamically changed. We also compared our linear logical method with the traditional model checking and the timed automata method.

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

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