競争的研究費の研究課題 - 岡田　光弘

モデルチェッキング法の限界を超える新しい論理的手法によるダイナミックな実時間システムのための検証ツールの実現

2001年

-

継続中

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 岡田　光弘, 補助金,  研究代表者

　研究概要を見る

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

フランス国立情報科学研究所と共同で申請者の理論の中核部分の実装試作を行ってきた。この試作された論理的検証系FATALIS Systemが来年度の日本側の上記実装研究の基盤として用いられる。

　備考を見る

特定領域研究C

実時間システムに対する論理的仕様・検証言語の国際共同実装計画

2001年

-

2003年

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 岡田　光弘, 補助金,  研究代表者

　研究概要を見る

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

　備考を見る

基盤研究(B)

発展的実時間システムの自動検証を可能にする新しい論理的検証理論

2001年

-

2002年

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 岡田　光弘, 補助金,  研究代表者

　研究概要を見る

本年度は、第1年次に開発した論理的理論を基にした仕様、検証の有効性を確かめ、仕様、検証の新しい論理的方法論を開発した。とくに、まず実時間システムの研究分野でベンチマークとして使われている代表的な実時間システムの具体例を発展的システムの例に変形し、これに我々の方法論を適用し、われわれの論理的な方法論とこれまでの他の方法論とを比較した。(例えば、今までの静的な交通網モデルを、新たに交通網が複雑化したり、電車の本数が変化したり、列車ダイヤの改定や時間制約の変化が起こったりする進化的モデルに作り変えて検討した。)

とくに、これまでのPVS言語やTLA言語などで代表されるような、伝統的な述語論理に基づいた論理的手法では、述語論理の表現力を用いて形式仕様が可能であるが、これらPVS言語やTLA言語の(および、その他の述語論理に基づく)枠組では、一般に証明可能性問題が非決定的であるため、形式的検証を体系的に遂行することができなかった。そこで彼らは、この言語使用者の責任において、与えられた形式仕様に特有な種々のInvariant Propertiesを見つけだし、それをもとに多重の数学的帰納法を適用して、検証の論理的証明を構成する、というアドホックな方法を採用していた。しかし現実の問題として、少し規模が大きな実時間システムを設計しようとすると、このような適当なInvariant Propertiesを一般の設計者自身が自分の責任で見いだすことは不可能であるのが実情である。これに対して、我々の線形論理に基づいた論理体系の枠組みは(PSPACE)決定可能であるので、仕様された実時間システムの安全性検証の証明構成(または危険性の証明構成)が自動的に遂行できる。この違いを具体的な例を用いて分析した。

　備考を見る

萌芽的研究→萌芽研究

国際共同研究及び特定領域研究「新しい論理学の展開」のための企画研究

2000年

-

継続中

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 岡田　光弘, 補助金,  研究代表者

　研究概要を見る

特定領域研究「新しい論理学の展開」及びそれと並行して行う国際共同研究に向けて,その準備のための企画・調査を行った.現在進みつつある新しい論理学の展開を把握し,論理学の進むべき方向を明らかにしていくには,哲学系論理学者達が中心となり,これに西洋・東洋の論理学史の学者達および認知科学,言語学,人工知能論,情報科学基礎論,数学基礎論を含めて特定領域研究チームを形成する必要がある.このため,本企画・調査研究においても,論理哲学者だけでなく,これに認知言語学者,論理学史者,情報科学者に加わってもらった.

昨年度に引続き,岡田は論理哲学(数学基礎論やフッサール後期の論理学も含む)を,飯田は言語分析哲学を,野矢は日常言語と論理との関係を,土屋は認知科学的立場からの論理を,岩田はおもに印度論理を中心に企画調査を行った.また,これらのメンバーの各々は,哲学以外の他の分野との交流も盛んに行ってきた.例えば,土屋は言語学界および認知科学界においても哲学的立場から多くの成果をあげており,また 岡田及び佐藤は人工知能論や情報科学や数学との境界領域の研究者達との打ち合わせも進めてきた.また,これまでも哲学系の研究代表者岡田と分担者土屋は情報科学系の分担者佐藤と分野を超えて本企画調査のための学術交流を重ねてきた.

これと並行して,岡田が海外における代表的な哲学系論理学の共同研究プロジェクトの視察・調査を行った.特に4月にソルボンヌ大(パリ大学第1校)哲学科において欧州側共同研究者達と共同研究企画のための会合を行ったのに続いて,7月末のヨーロッパ論理学会の折には米国側の共同研究者達も含めて上記課題の国際共同研究の企画会議を行った.

　備考を見る

基盤研究(C)

振舞仕様に基づく安全性検証の研究

2000年

-

2003年

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 仁木　厚吉, 補助金,  研究分担者

　研究概要を見る

一貫した論理体系に基づき,適応性と汎用性に優れ,かつ自動化の容易な安全性検証技術を実現することを目標に研究を進め,振舞仕様に基づく以下のような技術を開発した.

(1)未知ウイルス検知技術:振舞仕様の理論的枠組に基いてプログラムの挙動をモデル化することで,プログラムの安全性(=ウイルスで「あること」ならびに「ないこと」の判定)を論理的に解析し,自動的に検知する枠組を提案し,処理系を作成した.具体的には,Microsoft社のWindows OS上のプログラムを対象として,未知ウィルス検知ソフトウェアを作成し,開発した技術の有効性を示した.

(2)振舞仕様に基づく安全性検証技術:システムの安全性(safety)を,よりユーザーやアプリケーションに近いレベルで検証する技術として,システムの要求や仕様を振舞(behavior)レベルで定式化し,それに基づきシステムの安全性をよりユーザに近いレベルで検証し得る技術を研究開発し,それを鉄道信号システム,コンポーネントウェア,並行分散システム,安全プロトコルなどに適用し,その有効性を示した.特に電子商取引プロトコルに付いては,実規模のプロトコルの検証を行った.

(3)振舞仕様に基づくモデル検査技術:システムの要求や仕様を振舞(behavior)レベルで定式化し,システムの状態を仕様レベルで自然に抽象化することで,一般には無限状態となるシステムに対しても有効なモデル検査技術を開発し,基本的な並行アルゴリズムにや通信プロトコルについてこの技術の有効性を示した.

　備考を見る

特定領域研究(B)→特定領域研究

線形論理を用いた並行計算システム及び実時間システムの形式仕様・形式検証の理論

2000年

-

2002年

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 岡田　光弘, 補助金,  研究代表者

　研究概要を見る

種々の量的時間制約を含む並行計算システムに対する形式仕様・形式検証の方法論を線形論理学的手法を用いて与えた。時間制約付き並行計算プロセスを線形論理の証明で記述することにより、論理学的な証明分析手法を実時間並行計算システムの仕様・検証理論に適用した。特に稠密時間の枠組における線形論理的分析法の有効性を示した。又、後半では、種々の具体的な実時間有限状態システムのサンプルに対して我々の仕様・検証の方法論を適応し、方法論の検討・評価を行った。まず実時間システムの具体例(例えば、交通網自動制御システムの形式仕様とその安全性検証、実時間制約つきPhilosopher's Table等)に我々の方法論を適用し、これまでの他の方法論と比較検討した。特に、マルチエージェントの数や時間制約が発展的に変化する並行計算システムの仕様・検証例を用いて、我々の方法論の独自性を考察した。

伝統的な方法論である、時間オートマタ(Timed Automata)によるモデルチェッキングと呼ばれる手法による検証も(PSPACE)決定的であることがこれまでに知られている。これら伝統的モデルチェッキング法との比較も行い、われわれの新しい論理的方法論の特徴を調べた、又、これまでのオートマタを用いたモデル化の段階でしばしば生じるValidationの問題(実時間システムの設計者の最初の意図通にモデル化がなされているかどうかを問う問題)に焦点を当て、われわれの論理的形式仕様の方法論のメリットを分析した。われわれの論理的形式仕様の方法論では、ある形式で記述された仕様から論理的仕様への自動変換が可能である。又自然な表示的意味論(trace semantics)との間で完全性定理が成り立っている。これらの理由により仕様記述の意味が正確に論理的仕様に反映されること、及びこのようなValidationの問題が生じないことを確認した。

　備考を見る

基盤研究(B)

特定領域研究「新しい論理学の展開」のための企画研究

1999年

-

継続中

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 岡田　光弘, 補助金,  研究代表者

　研究概要を見る

特定領域研究「新しい論理学の展開」に向けて、その準備のための企画・調査を行った。現在進みつつある新しい論理学の展開を把握し、論理学の進むべき方向を明らかにしていくには、哲学系論理学者達が中心となり、これに西洋・東洋の論理学史の学者達および認知科学、言語学、人工知能論、情報科学基礎論、数学基礎論を含めて特定領域研究チームを形成する必要がある。このため、本企画・調査研究においても、論理哲学者達だけでなく、これに認知言語学者、論理学史学者、情報科学者に加わってもらった。

岡田は論理哲学(数学基礎論やフッサール後期の論理学も含む)を、飯田は言語分析哲学を、野矢は日常言語と論理との関係を、土屋は認知科学的立場からの論理を、岩田はおもに印度論理を中心に企画調査を行った。また、これらのメンバーの各々は、哲学以外の他の分野との交流も盛んに行ってきた。例えば、土屋は言語学界および認知科学界においても哲学的立場から多くの成果をあげており、また岡田は人工知能論や情報科学や数学との境界領域の研究者たちとの打ち合わせも進めてきた。また、これまでも哲学系の研究代表者岡田と分担者土屋は情報科学系の分担者佐藤と分野を超えて本企画調査のための学術交流を重ねてきた。

これと並行して、岡田が海外における代表的な哲学系論理学の共同研究プロジェクトの視察・調査を行った。また、ソルボンヌ大学哲学科Joinet博士、パリ・エコールノルマールシュープリュールのLongo博士ら欧州の論理学者およびホンコン大学哲学科及び米国テキサス大哲学科Thomason博士らアジア、米国の何人かの分析哲学者や言語行為論の論理研究者らを招いて、本研究企画のためのディスカッションを行い、助言を仰いだ。

　備考を見る

基盤研究(C)

実時間システムの形式仕様・検証のための新しい論理的方法論

1999年

-

2000年

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 岡田　光弘, 補助金,  研究代表者

　研究概要を見る

第2年次は,申請者がこれまでに確立した,線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する,証明のPSPACE決定可能性と(表示的意味論に対する)完全性という二つの定理を用いて,論理的手法による実時間システムの開発ツールを実装した.われわれのツールは次の特徴を持つ.

1.その第1は,ひとつの実時間システム全体の設計に伴う,システマティックな論理的形式仕様および,われわれの(PSPACE)決定手続きを用いた安全性・信頼性の自動検証が可能である.これは,これまでに得られた上記二つの論理的基本定理を用いることにより直接遂行できた.

2.その第2は,すでに与えられている実時間システムに新たな部分を加えたり,ある部分を変更したりするときに必要となる形式検証の問題や,二つの独立に作られた(安全性がそれぞれに対して保証されている)実時間システムを統合・総合しようとするときに必要となる形式検証の問題である.われわれの論理的な仕様・検証の枠組みは,もともと高度のモジュラー性を有しているので,このような問題に対しても本質的に上記1の方法論を応用することができた.

3.その第3は,一部に危険な状態が生じ得ることが分かっている実時間システムのなかで,ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析する手法の開発である.論理推論体系を(通常,定理自動証明の分野で行われているように)ボトムアップ的に用いると,論理的に証明できない命題に対しては,その反例がシステマティックに生成される.この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると,その反例となるプロセススケジュール(プラン),即ち安全なプロセススケジュール(プラン)の具体例が自動的に生成・枚挙される.この手法を用いて,与えられた実時間システム内での種々のスケジューリングの問題の論理的な方法論が適用できることとなった.このようなことは,これまでの伝統的なモデルチェッキングの手法では不可能なことであった.

　備考を見る

萌芽的研究

知識発見の論理に関する研究

1998年

-

2000年

日本学術振興会, 科学研究費補助金(文部科学省・日本学術振興会）, 佐藤　雅彦, 補助金,  研究分担者

　研究概要を見る

本研究課題では，知識発見の論理の基礎付けおよび知識発見の計算モデルに関する研究を行なった．

知識発見の論理の基礎付けに関する研究では，哲学における論理および数理論理学の両面から，知識発見の論理の基礎付けを図ることを目的とし，科学哲学における「発見の文脈」，特に，論理的アルゴリズムに還元できない「発見」について，哲学的視点から考察した．さらに発見の論理の演繹的側面を記号論理学，形式論理学の立場から考察した．さらに，発見における知識および概念の獲得過程を論理の立場から分析し，信念更新の理論に基づいて定式化した．また，数学における理想概念の導入と発見の関連を考察し，同時に概念と判断を組織的に記述できる体系を導入し，概念発見の考察のための基礎を与えた．

知識発見の計算モデルに関する研究では，知識発見の論理に対応する計算モデルについて検討し，適切な計算モデルを実現するシステムを計算機上に実現した．具体的には，分散計算空間における求解計算モデル，モデル検査法に基づくアルゴリズムの発見，古典論理の証明からのアルゴリズム発見手続について考察し成果を挙げた．

　備考を見る

特定領域研究(A)