hpprc/llmjp-kaken huggingface dataset:
形式手法のための論理の構築と、一階拡張が満たす性質に関する研究

研究成果の概要(和文):対象を形式的に記述することで,それらの対象を自動的に検証できるようになる.しかし,形式的に記述・検証するためには,「論理」という枠組みが必要となる.本研究では,Jacksonモデルを基にした要求管理を目的とした論理やMilk-run物流システムの経路探索を目的とした論理を構築した.また,検証用論理として提案された一階様相μ計算に関する性質として,モデル論的性質や表現力比較に関するいくつかの性質をしめした研究成果の概要(和文):対象を形式的に記述することで,それらの対象を自動的に検証できるようになる.しかし,形式的に記述・検証するためには,「論理」という枠組みが必要となる.本研究では,Jacksonモデルを基にした要求管理を目的とした論理やMilk-run物流システムの経路探索を目的とした論理を構築した.また,検証用論理として提案された一階様相μ計算に関する性質として,モデル論的性質や表現力比較に関するいくつかの性質をしめした1)検証のための新しい論理の構築要求仕様の参照モデルとして有名なJacksonモデルを基にした(要求管理のための)形式手法のためのモデル及び論理を構築し、その成果を国際会議などで発表した。本参照モデルでは、要求とシステム仕様の関係に、ドメイン知識の概念を取り入れ、その三つ組みで要求とシステム仕様の関係を定式化するものである。また、本手法では、形式的議論、及び計算機支援実現のための仕組みとして(形式)論理を用いた。具体的には、要求変更が起きた際の「仕様の最弱条件」という概念を定義し、それを計算機により自動的に導くことにより、要求変更のインパクトを測り、要求変更の管理を支援する技法を開発した。さらに、飛行機の着陸時制御システムの要求管理に本手法を適用し、その有効性を示した。2)一階様相μ計算の理論的性質を明らかにすること2.A)モデル理論:"一般モデルで充足可能な命題様相μ計算の論理式は、標準モデルでも充足可能か?"という問題を解決するために、与えられた一般モデルから、それと論理式の真偽に関して等価な標準モデルを構築する研究を行い、その成果を国内会議にて発表した。現時点では、この主張の完全な証明には至っていないが、有限な一般モデルに対しては、それと等価な標準モデルが構築できることを示した。2.B)表現力:CTL^*の表現力が命題様相μ計算の表現力よりも真に弱いことを示す証明を拡張し、それぞれの一階拡張である、FOCTL^*の表現力が一階様相μ計算の表現力よりも真に弱いことを示し、その成果を国内誌にて発表した。従来のCTL^*及び命題様相μ計算の表現力比較の証明は論理式に関する帰納法を用いている。そこで、一階拡張における証明へ拡張するために、一階拡張に特有の論理式に対応した帰納法による証明を行った。1.検証のための新しい論理の構築:物流システムの分析・検証のための論理の構築を行った.本研究では,配達システムにおける荷物配達要求記述言(DR-SLL:Delivery Requirements Specification Language)を時相論理であるLTLを基に構築した.さらに,この物流システム検証のためのシステムを,既存のLTL処理機を用いて実装するために,DRSLのLTLへの変換規則を考案した.(北村は関連成果で,2011年度山下記念研究賞を受賞)2.A.モデル理論: "一般モデルで充足可能な命題様相μ計算の論理式は,標準モデルでも充足可能か?"という問題を解決することがこの項目の目標である.昨年度の成果である「与えられた有限な一般モデルに対し,それと論理式の真偽に関して等価な標準モデルの構築」に関する研究を継続した.有限という制約を外すことができるか否かは解決できていない.2.B.表現力:昨年度の結果は,1)FOCTL*の表現力がFOM-muの表現力よりも弱いことを,論理式の構成に関する帰納法で証明し,さらに,2)後者の論理式で前者の論理式と等価にならないものを具体的に示すという二段階からなる.2)の方針を他の一階時相論理達の表現力比較にも適用できるよう,具体的な論理式を探すことが必要であり,命題時相論理の表現力比較で用いられる手法を調査し,その結果をまとめた.これらの結果を一階時相論理の表現力比較へ応用することで,一階時相論理達の表現力の差を示すことができると考えられるが,証明は完成していない.一階様相μ計算と似た論理を経由することで命題様相μ計算のモデル検査の効率を上げる研究などがある.一階様相μ計算の部分論理である一階時相論理達の表現力を明らかにすることで,記述能力・計算量の観点から,形式的検証などで利用する際に適切な論理を選択出来るようになる.2.(1)モデル理論:一般モデルと標準モデルの充足性に関しては,モデルが有限であるとうい仮定の下での等価性を過去の共同研究で示した.そこで,無限モデルから有限モデルへの対応をつけるための研究を実施したが,有限という制約を外すことができるか否かは未解決である.(1)本年度以前からの成果を発展させることでスムースな研究展開ができたためと考えられるため.(2.A).命題様相μ計算の完全性証明は困難であり,それと等価な箇所が本年度以降に残ったと考えられるため.

(2.B)昨年度の成果を用いて,他の一階時相論理たちの表現力の大小関係を示すことができると考えられ,本年度の調査結果を用いて,大小関係が真の大小関係となることを証明可能であると考えられるため.24年度が最終年度であるため、記入しない。1.本年度構築した論理のブラッシュアップ及び,提案した論理を用いた検証例の有用性に関する研究を推進する.2. A.Finite Model Propertyの成り立つ条件を精査し,無限モデルから有限モデルへの対応をつけることで,無限モデルと有限モデルのギャップを埋めることができるか否かを検討する.また,従来の完全性定理の証明で用いられているアイディアをモデル理論への移植可能性を検討する.2. B.昨年度に定式化した一階時相論理用に拡張された論理式に関する帰納法を用いて,ある一階時相論理の表現力が別の一階時相論理の表現力より弱いことを示す.また,本年度調査した命題時相論理の表現力比較の手法を拡張し,ある一階時相論理の表現力が別の一階時相論理の表現力より弱くないことを示す.24年度が最終年度であるため、記入しない。
一本鎖DNAとして特殊構造を示すDNA配列とタンパク質の特異的相互作用

1)GCGAAAGC配列を含むDNA断片と一本鎖DNA結合タンパク質との相互作用:すでに我々は,異常に安定なヘアピン構造を形成するGCGAAAGC配列が,ファ-ジG4の複製開始領域のヘアピン構造中に存在することを発見している。しかし,従来から考えられているこの領域のヘアピン構造は,GCGAAAGC型のヘアピン構造とは異なっている。そして条件によっては,これら2つのヘアピン構造のどちらかを形成していることがわかった。この2つの構造の平衡がファ-ジG4の複製開始の機構に関わっていると考え,今回は,この複製に開与している一本鎖DNA結合タンパク質(SSB)と,この領域の一本鎖DNAの相互作用を調べた。核酸分解酵素による限定分解を用い,DNAの構造を調べたところ,SSBが存在しないと,従来から考えられているヘアピン構造を,SSBが存在(結合する)するとGCGAAAGC型のヘアピン構造をそれぞれ形成することがわかった。すなわち,このファ-ジの複製開始領域のヘアピン構造はSSBが結合することによって構造が組み変わることがわかった。そして,このGCGAAAGC型からなるヘアピン構造がDNA複製を開始させる酵素であるプライマ-ゼと相互作用することが示唆される。2)GCGAAAGC断片の高次構造の解析:現在,GCGAAAGCをはじめ種々のDNA断片を合成しそれらの構造をNMRスペクトルやX線結晶構造解析等の手法を用いて調べている。NMRは,GCGAAAGCと数種類のDNA断片のNOESYスペクトルより立体構造のモデリングを行なっている。またGCGAAAGC断片の結晶化に成功し,その解析も進行中である。以上のように申請した内容の大半を達成することが出来た。
新興国における最適な為替政策運営に関する研究：移民送金と国際信用収縮の視点

近年移民送金の金額はその他の国際資本フローを上回る規模となっており、これは国際金融における為替政策上の新たなジレンマを生み出している。本研究では、為替変動がこうした国際資本フローを通じて新興国経済に与える仕組みについて明らかにし、「外貨建て移民送金と国際金融市場における投資資金調達という、異なる性質を持つ二つの大きな国際資金フローが生みだすジレンマに直面する新興国経済にとって、望ましい為替政策運営とは何か」という問いに対する政策的示唆を提示する。
絵本の読み聞かせ聴取時における脳反応について

H30年度の研究の目的および方法、結果、考察を以下に示す。【目的】絵本の読み聞かせによって、心の安定や心地よさが生じる可能性があるということに着目し、脳機能イメージングの手法(NIRS)を用い、絵本の読み聞かせ聴取時と、音読時、黙読時の脳の状態を計測し、比較検討する。【方法】対象は、小児(7-12歳)、大学生・大学院生(20-36歳)30名。島津製作所NIRStation近赤外光イメージング装置OMM-3000を使用し、関心領域をBroca野を含む前頭前野を中心に、左右各17chにて計測する。【結果】小児にまで対象を広げ計測を行ったところ、絵本の読み聞かせ聴取時では、全例で前頭前野の広範囲にてoxy-Hb濃度が減少した。音読時には、多くの例で、Broca野にてoxy-Hb濃度の増加が認められたが、一部の例では、Broca野でのoxy-Hb濃度の増加がみられず、前頭前野の正中部にてoxy-Hb濃度の減少がみられた。絵本の読み聞かせ聴取時のoxy-Hb濃度の減少量と質問紙調査でのリラックスの程度との間に相関がみられた。【考察】絵本の読み聞かせ聴取時に、前頭前野にてoxy-Hb濃度が減少したことは、快感情が起こり、リラックスした状態が誘発されたことによるものと推察された。また、前頭前野内側部はDMN(デフォルトモードネットワーク)の構成部位であることより、内省が抑制され、絵本の読み聞かせ聴取に没入することができていると考えられた。音読時・黙読時にみられたBroca野におけるoxy-Hb濃度変化量の差は、読字能力の個人差を反映している可能性があると考えられた。読字が苦手な学生は、音読時・黙読時においては、努力性の読みを反映してBroca野がより強く賦活されたと考えられた。本研究により、絵本の読み聞かせ聴取時には、心の安定や心地よさを感じ、メンタルヘルスに有効であることが示唆された。H28年度の研究の目的および方法、結果、考察を以下に示す。【目的】絵本の読み聞かせによって、心の安定や心地よさが生じる可能性があるということに着目し、脳機能イメージングの手法(NIRS)を用い、絵本の読み聞かせ聴取時と、音読時の脳の状態を計測し、比較検討する。【方法】対象は、大学生・大学院生(20-36歳)20名。【結果】絵本の読み聞かせ聴取時は、全例で前頭前野の広範囲にてoxy-Hb濃度が減少した。音読時にみられたBroca野におけるoxy-Hb濃度変化量の差は、音読能力の個人差を反映している可能性があると考えられた。音読が苦手な学生は、努力性の読みを反映してBroca野がより強く賦活されるのではないかとの仮説が考えられる。大学生20名を対象にNIRS検査を施行することができた。絵本の読み聞かせ時の脳反応をNIRSを用い明らかにすることができた。音読時の脳反応も合わせてNIRSを用いて明らかにすることができた。読みの苦手な学生でBroca野がより強く賦活されることを見出した。H29年度の研究の目的および方法、結果、考察を以下に示す。【方法】対象は、大学生・大学院生(20-36歳)40名。

音読時・黙読時にみられたBroca野におけるoxy-Hb濃度変化量の差は、読字能力の個人差を反映している可能性があると考えられた。読字が苦手な学生は、音読時・黙読時においては、努力性の読みを反映してBroca野がより強く賦活されるのではないかとの仮説が考えられる。大学生40名を対象にNIRS検査を施行することができた。絵本の読み聞かせ時の脳反応をNIRSを用い明らかにすることができた。音読時・黙読時の脳反応も合わせてNIRSを用いて明らかにすることができた。黙読速度とBroca野のoxy-Hb濃度変化量には、負の相関がみられ、読字の苦手な学生でBroca野がより強く賦活されることを見出した。H30年度の研究の目的および方法、結果、考察を以下に示す。【目的】絵本の読み聞かせによって、心の安定や心地よさが生じる可能性があるということに着目し、脳機能イメージングの手法(NIRS)を用い、絵本の読み聞かせ聴取時と、音読時、黙読時の脳の状態を計測し、比較検討する。【方法】対象は、小児(7-12歳)、大学生・大学院生(20-36歳)30名。島津製作所NIRStation近赤外光イメージング装置OMM-3000を使用し、関心領域をBroca野を含む前頭前野を中心に、左右各17chにて計測する。【結果】小児にまで対象を広げ計測を行ったところ、絵本の読み聞かせ聴取時では、全例で前頭前野の広範囲にてoxy-Hb濃度が減少した。音読時には、多くの例で、Broca野にてoxy-Hb濃度の増加が認められたが、一部の例では、Broca野でのoxy-Hb濃度の増加がみられず、前頭前野の正中部にてoxy-Hb濃度の減少がみられた。絵本の読み聞かせ聴取時のoxy-Hb濃度の減少量と質問紙調査でのリラックスの程度との間に相関がみられた。【考察】絵本の読み聞かせ聴取時に、前頭前野にてoxy-Hb濃度が減少したことは、快感情が起こり、リラックスした状態が誘発されたことによるものと推察された。また、前頭前野内側部はDMN(デフォルトモードネットワーク)の構成部位であることより、内省が抑制され、絵本の読み聞かせ聴取に没入することができていると考えられた。読字が苦手な学生は、音読時・黙読時においては、努力性の読みを反映してBroca野がより強く賦活されたと考えられた。本研究により、絵本の読み聞かせ聴取時には、心の安定や心地よさを感じ、メンタルヘルスに有効であることが示唆された。今後さらに被験者数を増やし、小児例を対象にNIRS検査行いたい。そして、小児における音読・黙読時の脳反応、絵本の読み聞かせ聴取時の脳反応の特徴を明らかにしたい。NIRS検査では脳表面の血流しか評価できないため、同じ課題を機能的MRIを用いて施行し、脳全体の血流動態・神経活動評価も行いたい。さらに、課題施行時に心拍変動、唾液中のアミラーゼ・コルチゾールを測定し、絵本の読み聞かせによるリラックス効果を客観的に評価する予定である。また、絵本の読み聞かせの方法を対乳児音声(母親語:Motherese)及び対成人音声を用いてその効果の比較を行う。
粒子法による電子状態計算手法の開発

粒子法を用いると計算点(粒子)の配置に制約がない。この点に注目して電子状態計算に適用することが研究課題の特徴である。特に粒子法の特徴を生かすよう電子状態の動的な変化の算出が可能な形にしなければならないため、粒子の配置の決定法について精度を維持しつつ、有効に算出できる手法の検討を行うことがこの研究の主目的である。研究遂行中は粒子の配置とその精度および効果について見極めを中心に行った。我々が目指している電子状態の時間的な変化をとらえるために、時間依存の波動方程式を、Bohm形式を用いて解くこととした。これは波束の動的な特性を軌跡データの解析から求める手法として知られており、我々が用いている粒子法との相性が非常に良い。一方、Bohm形式では数値的に不安定であることと、粒子法では計算点である粒子の配置が精度を決めるため、計算点が過度に集中する場合あるいは疎になる場合、精度が低下してしまうという欠点があった。そこでこれらの課題を解決するために我々は次のような手法を開発した。まず大きな節のない基底状態と節のある励起状態の線形結合を作り時間発展を進める手法である.これにより数値的な不安定さを解消することができた。次に計算点の粗密による課題に対しては、計算点の動的な追加および削除を行うことにより、計算精度を目指す範囲内に抑えることが可能となった。これらの開発された手法について、基本的な動作例として、電界効果トランジスタ半導体デバイスの電子状態計算での動作特性の解析をはじめ、二重スリットを通過する電子波束の干渉について動的な解析を計算例として確認することができた。計算点間隔が広い場合や極めて狭い場合に新しい計算点の追加や計算点の消去を行うものであり電子状態解析の特徴が出るものである。粒子法を用いると計算点間の配置には制約はない。その分自由度は増すが、常に精度の確認が必要となる。また粒子法の特徴が生かせるように電子状態の動的な変化の算出が可能な形にしなければならない。このために粒子の配置の決定法について精度を維持しつつ、有効に算出できる手法の検討を行うことが、この研究の主目的である。このため初年度では、粒子法(特にSSPH)を電界効果トランジスタ(FET)の1次元の解析が可能な半導体デバイスの電子状態計算に適用することで、その精度への影響を見極めることに注力した。その結果、差分法と遜色がないことを示すことができた。特に、電子密度が電子移動度とゲートに印加された電圧によって決まる高移動度トランジスタ(HEMT)を対象とした。電流とゲート印加電圧の関係が1次元の計算によって単純に求めることができるからである。このデバイスの量子準位等を評価するために、特に粒子法の中で精度が高いと言われているSSPHを用いた。解析ではデバイスの典型的な特徴としてI-V特性および増幅率に注目した。HEMTの電子状態の解析にはSSPHだけでなく比較のため有限差分(FD)も用いた。得られた結果はFDの結果とよく一致しており、SSPHの精度がFDと遜色がないことが判明した。次年度以降では、粒子の配置と精度の関係を見極めつつ、計算点である粒子の動的な変化をさせる最適な配置を見つけることができるような解析を行う予定である。粒子法の特徴である計算領域に計算点(粒子)を均等に配置する必要はなく、電子状態に合わせ高精度な計算が必要な領域へ集中的に粒子を配置することで効率的な計算を行うことが期待できるからである。計画に従い初年度計画にそって、小規模サイズでの基本アイデアの試行と計算精度の見極め、基本アイデアを生かすためのプログラムの設計、更に計算精度の確認をしつつ基本的なプログラムを作成することができたためである。比較のため、SSPHではsmoothing lengthを均一にし、その長さを0.2, 0.3Åと変えて対応するFDの結果と比べたが精度に差は生じていないことから、基本的な計算手法として問題ないことが確認できた。またsmoothing lengthを精度が必要になるHEMTの占有量子準位が分布しているチャネル層付近で倍近くまで増加させたが、結果は変わらずSSPHの有効性がある程度確認できた。同様に結果が比較できるようにFDでも非等間隔の差分を取って両者の結果を比較したところ精度に差はみられなかった。粒子法を用いると計算点の配置に制約がない。特に粒子法の特徴を生かすよう電子状態の動的な変化の算出が可能な形にしなければならない。粒子の配置の決定法について精度を維持しつつ、有効に算出できる手法の検討を行うことがこの研究の主目的である。このため2017年度までに、1次元の解析が可能なHEMTデバイスの解析成果から得られた知見を用い、電子状態解析の特徴がでる二重スリットを通過する電子波束の干渉について動的な解析を実施した。この解析に粒子法を用い、計算点(粒子)の配置とその精度および効果について見極めを中心に行った。粒子法では計算点である粒子の配置が精度を決めるため、計算点が過度に集中する場合あるいは疎になる場合、精度が低下してしまうという欠点がある。

この対策として、計算点間隔が広い場合や極めて狭い場合に新しい計算点の追加や計算点の消去を行うという手法を考案した。計算領域に計算点を均等に配置する必要はなく、電子状態に合わせ高精度な計算が必要な領域へ集中的に粒子を配置することで効率的な計算を行うことができるという粒子法の特徴を活かしている。また、基底状態も虚数時間を使う時間発展の手法を用いることで効率的に計算可能であることがわかり、上記手法と組合せ効率的な解析の推進が大いに期待できる。初年度計画にそって、小規模サイズでの基本アイデアの試行と計算精度の見極め、基本アイデアを生かすためのプログラムの設計、更に計算精度の確認をしつつ基本的なプログラムを作成することができたが、本来の目的である実時間実空間の時間依存密度汎関数法へ粒子法を適用したコードに仕上げるには、必要な変更箇所が非常に多いことと各変更箇所での動作確認に予想以上に時間がかかることが判明し、その結果、当初計画と比較して若干の遅れが発生しているためである。今後、動的双極子モーメントの計算とそれに合致した動的な粒子配置の検討を進めていく必要がある。また光学スペクトルへの対応は2018年度の課題となる。一方、粒子法に基づいて重要な波動関数の勾配の計算やラプラシアンの計算については、2016年度smoothing lengthに関する検討を十分に行ったため、任意配置でもある程度の精度を維持しつつ、算出できることが分かっている。これは1次元、2次元および3次元にて確認済みであり、研究の進展は順調に推移すると期待できる。粒子法を用いると計算点(粒子)の配置に制約がない。この点に注目して電子状態計算に適用することが研究課題の特徴である。特に粒子法の特徴を生かすよう電子状態の動的な変化の算出が可能な形にしなければならないため、粒子の配置の決定法について精度を維持しつつ、有効に算出できる手法の検討を行うことがこの研究の主目的である。研究遂行中は粒子の配置とその精度および効果について見極めを中心に行った。我々が目指している電子状態の時間的な変化をとらえるために、時間依存の波動方程式を、Bohm形式を用いて解くこととした。これは波束の動的な特性を軌跡データの解析から求める手法として知られており、我々が用いている粒子法との相性が非常に良い。一方、Bohm形式では数値的に不安定であることと、粒子法では計算点である粒子の配置が精度を決めるため、計算点が過度に集中する場合あるいは疎になる場合、精度が低下してしまうという欠点があった。そこでこれらの課題を解決するために我々は次のような手法を開発した。まず大きな節のない基底状態と節のある励起状態の線形結合を作り時間発展を進める手法である.これにより数値的な不安定さを解消することができた。次に計算点の粗密による課題に対しては、計算点の動的な追加および削除を行うことにより、計算精度を目指す範囲内に抑えることが可能となった。これらの開発された手法について、基本的な動作例として、電界効果トランジスタ半導体デバイスの電子状態計算での動作特性の解析をはじめ、二重スリットを通過する電子波束の干渉について動的な解析を計算例として確認することができた。
剪断波超音波パルスによるSNOM探針接触の検出

1.SNOM装置の試作SNOMとしての基本性能を確かめるために音叉型水晶振動子の電極を分離し,片方に光ファイバーを取り付け,他方で信号検出した。約40kHZと130kHzとに共振点が現れ,それぞれ1次,2次のモードに対応している。2次のモードの共振特性を利用することによりいわゆるACモードでの探針制御により試料の凹凸像を得ることができた。試料にはスライドガラス上の金蒸着膜を2μm角の市松模様状にエッチングしたものを用いた。2.剪断変形によるパルスエコー従来の超音波探針顕微鏡では,タングステン探針の根本に伸縮変形する圧電体を貼り付け探針先端を伸縮変形させて反射波の位相変化を検出していた。伸縮変形では試料表面を塑性変形させる恐れがあり,他の方法で凹凸を制御したうえで音響インピーダンスの情報を取り出す必要がある。5MHzで共振する勢断変形圧電体を直径0.5mmφのタングステン探針の根本に貼り良好な剪断変形パルスエコーを得ることに世界で初めて成功した。しかしながら,探針の深さ方向へ距離変化に対して剪断変形による接触による信号変化は伸縮変形を利用した場合のように単調ではなく,従来のパルス重畳法を用いての凹凸像検出は不可能であった。複合材料ネフマックの表面を研磨後,金を蒸着しSTMとして探針を制御しながら勢断変形による信号を映像化することはできたが,その映像の解釈はできていない。3.送り装置とアクチュエータの開発SPMとして粗動機構に空中レトラクト方式を考案していたが審査請求し許可を取得した。また,送り装置に円筒型圧電体を用いる方式を発明し,共同出願した。1.SNOM装置の試作剪断波超音波パルスを伝搬させる前に,従来のSNOMを製作した。まず,光ファイバーの根本に伸縮変形する圧電対を貼り付け共振特性を測定した。2次のモードの共振特性の方が単一ピークで共振振幅も大きくその共振を利用することによりいわゆるACモードでの探針制御により試料の凹凸像を得ることができた。2.剪断変形によるバルスエコー従来の超音波探針顕微鏡では,タングステン探針の根本に伸縮変形する圧電対を貼り付け探針先端を伸縮変形させて反射波の位相変化を検出していた。しかしながら、伸縮変形では試料表面を組成変形させるおそれがあり,他の方法で凹凸を制御したうえで音響インピーダンスの情報を取り出す必要がある。5MHzで共振する剪断変形圧電体を直径0.5mmφのタングステン探針の根本に貼り良好な剪断変形パルスエコーを得ることに世界で初めて成功した。従来のパルス重畳法を用いて凹凸増が検出可能であることを確認しつつある。3.光ファイバーに取り付けた剪断変形版によるパルスエコー光ファイバーの先端から約10mm上部に0.5mm厚の伸縮変形及び剪断変形の圧電体を4層積層して切断した側面を貼り付け超音波パルスを送り込む実験を行った。しかしながら,現在の段階では,良好なパルスエコーを得るに至っていない。側面を利用するために,光ファイバーの太さに対して圧電体の大きさが相対的に大きすぎることが考えられる。現在圧電体を薄くスライスして使用する方法を検討中である。1.剪断変形によるパルスエコー超音波探針顕微鏡では,タングステン探針の根本に伸縮変形する圧電対を貼り付け探針先端を伸縮変形させて反射波の位相変化を検出する。

導電体試料でない場合には試料表面の凹凸を他の方法で制御し音響インピーダンスの情報を取り出す必要がある。伸縮変形の代わりに剪断変形を利用するため,昨年度は5MHzで共振する剪断変形圧電体を直径0.5mmφのタングステン探針の根本に貼り良好な剪断変形パルスエコーを得ることに世界で初めて成功した。さらに今年度は10MHzの圧電体を使用しても良好なパルスエコーを得ることができた。しかしながら,パルス重畳法を用いた位相検波出力は探針試料間距離に対して線形の変化をする条件がまだ決まっていない。振幅を小さくすると位相検波出力が得られないためである。2.伸縮変形による接触の検出従来の伸縮変形で振動振幅を減少させることにより試料に塑性変形を与えることなく情報を取り出す可能性を探った。直径68μmのカーボンファイバーを埋め込んだ複合試料の断面をSTM及び超音波信号により映像化することに成功した。3.光ファイバーに取り付けた剪断変形版によるパルスエコー光ファイバーの先端から約10mm上部に0.5mm厚の伸縮変形あるいは剪断変形の圧電体を4層積層して切断した側面を貼り付け超音波パルスを送り込む実験を引き続き行ったが,良好なパルスエコーが得られていない。探針全体に圧電体膜を形成してトランスデューサにすることを検討している段階である。
子どもの姿勢調査および筋量、筋力、身体活動量との関係

本研究は、姿勢と筋力、骨格筋量、身体活動量との関係を明らかにすることを目的とした。小中学生410人を対象に行った調査で、姿勢が悪いと感じることがある人は72.8%で、姿勢の悪さを感じていない群と比べると、体育以外の運動実施回数がやや少ない傾向が見られた。中学生33名を対象にした測定で、体幹や下肢筋量が少ないと、頭部が前方に出たり、背中の彎曲が大きい傾向がみられた。しかし、姿勢の良し悪しで身体活動量に差はないことが示された。以上の結果から、運動実施状況や身体活動量は姿勢に大きな影響を与えないものの、体幹や下肢の筋量が姿勢に関与している可能性が示唆された。本研究の目的は、授業中の児童・生徒の姿勢データを取得し、生活習慣・運動習慣との関係を検討すること、姿勢と筋力、骨格筋量、身体活動量との関係を明らかにすることである。そこで、静岡県内の小学校および中学校で授業の様子をビデオ撮影するとともに、400人の児童・生徒に対し、姿勢と運動習慣に関する調査用紙を配布し、回答を得た。教育現場で子どもに接している教員の多くが、姿勢が悪い子どもの増加を実感しているものの、実際に姿勢が悪い子どもがどの程度いるのかは明らかになっていない。したがって、このビデオ画像を分析することにより、実態の一部が明らかになるものと考えられる。また、調査用紙から、小学生では、授業中に足を後ろに曲げたり、頬杖をつくことが多いと回答する児童が目立ち、中学生では足を前に伸ばしたり、机に伏せることが増える傾向にあることがわかった。また70%を超える児童・生徒が、姿勢が悪いと感じている(よく感じている・時々感じている)ことが明らかになった。さらに、静岡県内の中学校で23人の生徒を対象に、立位姿勢、足圧分布(重心の前後・左右の偏り)、体幹筋力(背筋力、上体起こし)、身体組成に関する測定を実施した。その結果、重心の前後の偏りと、体幹の筋力の間に有意な相関関係は認められなかったが、重心の左右の偏りが大きいと下肢筋量の左右差が大きくなる傾向が見られた(r = -0.431、p = 0.051)。しかしながら、必ずしも、利き足でより多くの体重を保持している訳ではない可能性も伺え、より詳細な検討が必要であると考えられた。また、この中学校の養護教諭と姿勢に関する意見を交換した。その際に、脊柱彎曲などの問題がある生徒が授業中の姿勢が悪いと評価されている訳ではないことが示された。石川県内の小学校に通う児童65人(6年生・1112歳)を対象に姿勢に関する測定を実施した。姿勢の測定は前額面方向の立位姿勢を撮影した写真を分析する方法、および重心動揺装置を用い前後左右方向の重心の位置を測る方法を用いた。立位姿勢画像は、画像分析ソフト(Image J)を用いて分析し、左右の肩の高さで結んだラインと水平面との成す角度を求めた。その結果、1.8±1.4度(平均±標準偏差)の傾きが確認された。また、3度以上の傾きがある児童は20人(30.1%)、うち5度以上の傾きがある児童が2名(0.3%)存在した。一方、重心動揺装置を用いた測定では、左右それぞれ50%ずつ体重がかかっている場合を基準として、左右それぞれにかかる体重の差(重心の偏り)が12.3±8.5%あることが確認された。また、69:31と片方の脚に過度に体重をかけている児童も存在した。しかし画像から確認された身体の傾きと重心動揺装置を用いた重心の偏りの間には相関関係は認められなかった。また、一部の児童を対象に超音波診断装置を用いて腹部および大腿前部の左右の筋厚の測定を実施した。しかしながら、身体の傾きや重心の偏りが確認された児童であっても、筋厚の左右差は確認されなかった。これは、児童の筋厚が成人に対して薄いことで、左右差があったとしても、測定誤差に埋もれてしまうためと考えられた。幼児を対象とした測定も実施した。この測定では、重心動揺計を用いて、体重の偏りを測定するとともに、身体活動量や体力に関する測定も実施した。これについては、現在、データの分析中である。本研究の目的は、児童・生徒の姿勢と生活習慣・運動習慣との関係を検討すること、さらに、立位姿勢と筋力、骨格筋量、身体活動量との関係を明らかにすることである。

最終年度の成果:女子中学生10名を対象に、立位姿勢、足圧分布(重心の前後・左右の偏り)、体幹筋力(背筋力、上体起こし)、骨格筋量、身体活動量の測定を行った。立位姿勢から、姿勢が良い群と悪い群に分け、測定値を比較した。その結果、足圧分布、体幹筋力、骨格筋量、身体活動量のいずれにおいても、両群間で有意な差は確認されなかった。期間を通した成果:400人の児童・生徒を対象に姿勢と運動習慣に関する調査を行った結果、小学生では、授業中に足を後ろに曲げたり、頬杖をつくことが多いと回答する児童が目立ち、中学生では足を前に伸ばしたり、机に伏せることが増える傾向が見られた。また、調査対象者の70%以上が、姿勢が悪いと感じている(よく感じている・時々感じている)ことが明らかになった。また。中学生のおよそ45%以上が、普段良い姿勢でいることを意識していないことも明らかになった。静岡県内の中学校で、授業中のビデオ映像から、姿勢の良い生徒11人、悪い生徒12人をそれぞれ選出し、前述の調査結果を比較したところ、自身の姿勢への意識は、姿勢が良いと判断された群で高い傾向を示した。しかしながら、1週間当たりの運動実施回数や時間は両群に差は見られなかった。さらに、立位姿勢、足圧分布、体幹筋力、骨格筋量の測定を実施したところ、授業中の姿勢と立位姿勢は必ずしも一致しないことが示された。一方、重心の左右の偏りが大きいと下肢筋量の左右差が大きくなる傾向が見られた。これらの結果から、自身の姿勢に対して意識を高める必要性があることが伺えた。また、運動実施状況や身体活動量は姿勢に大きな影響を与えないものの、体幹や下肢の筋量が姿勢に関与している可能性が示唆された。応用健康科学本研究の目的は、授業中の児童・生徒の姿勢データを取得し、生活習慣・運動習慣との関係を検討すること、姿勢と筋力、骨格筋量、身体活動量との関係を明らかにすることである。平成24年度は、第1段階として、姿勢の観察・評価と生活習慣・運動量の調査を実施し、第2段階として、第1段階で姿勢が良い/悪いと評価された児童・生徒を対象とした測定を実施する計画であったが、平成24年度終了時では、計画がやや遅れていた。そこで、平成25年度の前半は、姿勢の観察・評価と生活習慣・運動量の調査に重点を置くこととし、静岡県内の小学校・中学校で、小学4年生から中学3年生まで、授業中の姿勢観察を行った。机の配列に応じ、最大3方向から、異なる科目で複数時間のビデオ撮影を行った。また、対象となった学年の全児童・全生徒を対象に姿勢と運動習慣に関する調査を行った。本研究で取得したビデオ画像を分析することで、授業中に姿勢が悪い子どもがどの程度いるのかを示すことができると考えられる。ビデオ画像から、客観的な姿勢評価基準を作成することも可能ではないかという期待もあったが、姿勢そのものが悪いのか、授業に集中していないだけなのかの判別ができないケースが多かったため、基準の作成には一層の工夫・調査が必要なことが伺えた。平成25年度の後半には、第2段階である姿勢が良い/悪いと評価された生徒を対象とした測定を行い、立位姿勢、足圧分布、体幹筋力、身体組成のデータを取得した。その成果の一部を昨年度開催された国内学会にて発表した。身体活動量の測定については、装置を1週間装着することに関して、協力校との調整ができず、実施することが出来なかったことから、今年度、再度交渉・実施をする方針である。本研究の目的は、子どもの姿勢と筋力や筋量、身体活動量との関係を検討すること、および身体活動量を増やすことにより、姿勢を改善できるか検討することである。平成24年度は、第1段階として、姿勢の観察・評価と生活習慣・運動量の調査を実施し、第2段階として、第1段階で姿勢が良い/悪いと評価された児童・生徒を対象とした測定を実施する計画であった。
近代ロシア・ナショナリズムの形成―ロシア帝国西部地域諸民族との相互関係のなかで

ロシア帝国西部境界地域におけるロシア・ナショナリズムの形成プロセスを、諸民族のアイデンティティの勃興、それとの接触と衝突、相互影響などから明らかにした。特に、社会史的な分析に力を入れ、個別の具体的な事例を入念に分析することを心掛けた。研究の推移とともに、研究分担者の範囲を超えて、多様な国家の研究者がプロジェクトに参加することになり、そのことで、多角的な視点から議論を深めることができた。宗教に焦点を当てたことで、ロシア・ナショナリズムの形成も含め、前近代からの諸民族のアイデンティティの変容のプロセスを、統治システムや社会制度の変化のなかで明らかにすることができたと考える。2015年度は、ロシア帝国西部地域におけるナショナリズムの多層性について社会史的な分析を進め、世界的な学者と意見を交換し、その研究内容を深めた。ICCEES(国際中欧・東欧研究協議会)第九回世界大会(幕張)にてパネルを組織し(「Tangled nation-building competition in Ziemiezabrane (eastern region of Poland)or Zapadnyi Krai (western region of Russia)」)、そこで研究報告をした際に、世界的な学者と交流を深め、当研究課題に関しても、次の成果につながる意見を得た。さらに、幕張での国際学会の後に、パネリストを神戸に招聘し、神戸でワークショップ(“Empires, religions, and nationalisms in Central and Eastern Europe and Russia")を開催した。そこでは、別の財源で招聘されたポール・ワース氏、コンスタンチン・ヨルダッキ氏に中・東欧・ロシアの帝国的統治・宗教・ナショナリズムについての報告をしてもらった。そのさい同時に、当研究プロジェクトの海外協同研究者であるオルガ・マスチャニツァの報告原稿を研究代表者が報告し、協同研究者の福嶋千穂、東方ユダヤ人の専門家である高尾千鶴子氏にディスカッサントを務めてもらい、さらに、ロシア帝国の仏教徒の専門家である井上岳彦氏を招き、フロアから議論に参加してもらうことで、当研究課題を進展させる学術的議論を行った。当ワークショップには、関西全域から研究者・院生含め30名程度が参加した。こうした議論は、その後の発表された青島陽子「ロシア帝国の「宗派工学」にみる帝国統治のパラダイム」や福嶋千穂『ブレスト合同』に生かされることになった。当初、幕張国際学会と神戸のワークショップに、海外協同研究者のオルガ・マスチャニツァが参加する予定であったが、急な重病のために来日することがかなわなかった。この点は予期しないハプニングであった。しかし、国際学会・ワークショップ双方のために、当人が発表原稿を送付してくれたために、両会議共に実現された。とくに神戸のワークショップでは、その後の研究打ち合わせも含め、海外からのゲストやフロアから十分な時間をかけて意見をもらい、当研究課題を深めることができた。こうしたことからも、2015年度に予定されていた研究活動として十分な進展が見られたと言える。さらに、こうした活動を通じて得られた意見を加えて、論考や出版物も発表された。この研究成果の発表を通じて、さらに国内の研究者のコメントも得ることが出来たことで、さらに2016年度の研究の進展が望める状態であると言える。本研究の目的は、ロシアのナショナル・アイデンティティの形成を、ヨーロッパ北東部に位置するロシア帝国西部地域諸民族の相互影響関係の分析を通じて明らかにすることである。平成28年度の研究実績は、第一に、平成28年8月22日・23日にリトアニアのヴィリニュスにて、リトアニア歴史研究所との共同でシンポジウム「Entangled interactions between religions and national identities in the space of the former Polish-Lithuanian Commonwealth」を開催したことである。このシンポジウムでは、ロシア帝国の西部国境地域とその周辺の諸民族形成過程をより詳細に分析するために、宗教というファクターに着目した。当該地域の民族形成の歴史分析では、伝統的に言語に注目が集まってきた。それに対して、近年ではロシア帝国論を中心に宗教的ファクターに着目した研究が発展してきた。そこで、ナショナリズムと宗教をテーマとしながら、前近代との連続性と断絶、ネイション構築における社会変容の実態、ナショナル・ナラティヴの構築における過去の参照方法、宗派国家たる帝国とネイションの関係性など、新しい観点から当該地域の複雑なネイション形成とそれら相互の影響関係を討論した。当シンポジウムには、8カ国から13名が集まり、それぞれにテーマに沿った研究報告を行った。その他、国内での学会や研究会などの機会を利用しながら、共同研究者との研究打ち合わせを行い、シンポジウムの成果の発表も含めた研究の深化を試みた。予定していたシンポジウムが、当初の予定以上の規模となった。その理由としては、当科研費以外に、民間の財団からもご支援を頂くことができたため、セッションを増加して参加人数全体を増やすことが可能となったことが大きい。それに対して、リトアニア歴史学研究所が真摯に協力をしてくれたため、世界各国から第一線の研究者を集めて討論をする場を作ることができた。さらに、このシンポジウムを成果として、リトアニア歴史学研究所が国内の競争的資金を獲得することができた。その資金と当科研費を併せて、2017年度には、11月にアメリカ最大のスラヴ・ユーラシア研究学会の大会で共同で報告をし、さらに、2018年2月には東京で新たな国際会議を企画している。現在、これらの企画を進めているが、すべて実現すれば、当初の計画で予定していた以上の大きな成果を得ることになる。

2017年度の代表的な研究実績は、まず11月12日にアメリカのスラヴ東欧ユーラシア研究協会年次大会にて、本研究テーマに関わる先端的研究者でアメリカ在住のミハイル・ドルビーロフ、ポール・ワースを討論者と司会者に招き、共同研究者のリトアニア歴史学研究所のダリウス・スタリューナスらと共にパネル"Difficult Alliance: Imperial Government and Russian Nationalism on the Western Provinces of the Russian Empire, 1905-1915"を組んで研究報告を行ったことである。このアメリカでの国際会議では、研究代表者が代表して研究報告し、さらにリトアニア側と研究打ち合わせを行った。続いて、この研究打ち合わせを受けて、2018年2月10・11日に東京大学本郷キャンパスにて、リトアニア歴史学研究所との共同企画で、国際シンポジウム“Protecting the Empire: Imperial Government and Russian Nationalist Alliance in the Western Borderlands during the Late Imperial Period"を開催した。ここには、リトアニアから、リーダーのダリウス・スタリューナス他、若手の研究者3名が出席し、さらにアメリカ、イスラエル、フランス、ウクライナから最先端の研究者を招き、総勢6か国21名で二日にわたって集中的な討論を行った。本研究課題の研究分担者である福嶋千穂、梶さやかも研究報告を行った。さらに、研究代表者は、研究成果の一部を『歴史学研究』(「農民を臣民に鋳直すー帝政期ロシアの農村教師養成のポリティクスー」)に掲載した。ロシア帝国西部境界地域におけるロシア・ナショナリズムの形成プロセスを、諸民族のアイデンティティの勃興、それとの接触と衝突、相互影響などから明らかにした。特に、社会史的な分析に力を入れ、個別の具体的な事例を入念に分析することを心掛けた。研究の推移とともに、研究分担者の範囲を超えて、多様な国家の研究者がプロジェクトに参加することになり、そのことで、多角的な視点から議論を深めることができた。宗教に焦点を当てたことで、ロシア・ナショナリズムの形成も含め、前近代からの諸民族のアイデンティティの変容のプロセスを、統治システムや社会制度の変化のなかで明らかにすることができたと考える。2016年度は、2015年度の国際学会・ワークショップでの意見交換を踏まえながら、リトアニアの首都ヴィリニュスで、海外協同研究者の所属機関であるリトアニア歴史学研究所で国際シンポジウムを企画している(8月22日・23日:
ファージライブラリー法を用いた感染阻害剤の開発

感染は多くの場合に糖鎖が関与していることが知られでいる。本研究ではファージ提示ペプチドライブラリーの手法を用いて糖鎖結合性ペプチドあるいは糖鎖レプリカペプチドをセレクションして、感染阻害剤の作製を行った。特に本研究では分子進化工学の手法を用いて阻害活性に優れたペプチド配列の探索を行った。糖脂質はウイルスや毒素の感染において受容体として関与していることから、糖脂質結合性ペプチドは感染阻害剤として利用できることが考えられる。そこで、インフルエンザウイルスやその受容体である糖脂質に結合するペプチドをファージライブラリーによりセレクションしたペプチド配列を得る事に成功した。これらのペプチドは標的分子であるインフルエンザウイルスのヘマグルチニンや糖脂質に結合した。さらに、インフルエンザウイルスの細胞への感染を阻害する事を見出した。次に、ファージ提示ペプチドライブラリーからセレクションされていたインフルエンザウイルスのヘマグルチニンに結合できる糖鎖レプリカペプチドの構造の最適を行った。具体的にはヘマグルチニンへの結合性を見出している初代配列にランダムな変異を導入してサブライブラリーを構築した。そのサブライブラリーを用いて新たにバイオパニングを実施して結合活性に優れた配列をセレクションした。得られたペプチド配列は、異なる亜型のインフルエンザウイルスのヘマグルチニンに結合し、細胞へのウイルスの感染を阻害することが示された。その阻害活性はもとの配列に対して顕著に向上する事が見出された。(1)糖脂質結合性ペプチドの作成と機能GM1結合性ヘプタペプチドのセレクションにファージディスプレイ法を用いた。ライブラリーとしては繊維状ファージ外殻タンパク質PIIIのN末端に7アミノ酸残基のランダムヘプタペプチドを線状に提示させたものを用いた。異なる溶出法により18種類のファージクローンを得た。中でも活性の高かったのは酸溶出で得られたファージクローンで、その7アミノ酸配列を化学合成したペプチドはシアル酸を有する糖脂質に選択的に結合した。また、コレラトキシンの最大結合量を50%阻害する時のペプチド濃度IC_<50>は20μMであった。その変異ペプチドを用いた結合活性の解析及び阻害実験を行った結果、ペプチド配列中に含まれるArgはGM1のシアル酸と静電的相互作用し、Pheがガラクトースとスタッキングすることにより結合しているということが示唆された。(2)糖鎖レプリカペプチド脂質の作成とその機能糖鎖の認識はペプチドで置き換えることができる。インフルエンザウイルスのヘマグルチニン(HA)は、宿主細胞の細胞膜のGM3やシアル化ルイスX等の糖脂質を受容体としている。HAは遺伝子交雑による抗原性の変化に伴う亜型が生じるために、亜型間にまたがる広域薬剤の開発が望まれている。多種のオリゴ糖鎖の活性を検討することは糖鎖の供給の問題で現実的に難しい。そこでヘマグルチニンに結合できる糖鎖レプリカペプチドを15アミノ酸のランダム配列を有するファージライブラリーから検索した。得られたペプチドは亜型の異なるヘマグルチニンに結合する能力を有していた。得られたHAに結合性を有するペプチドをリポソーム表面に固定化したところ、両亜型のインフルエンザウイルスのMDCK細胞への感染をin vitroで阻害することが見いだされた。感染は多くの場合に糖鎖が関与していることが知られている。まず、糖脂質はウイルスや毒素の感染において受容体として関与していることから、糖脂質結合性ペプチドは感染阻害剤として利用できることが考えられる。そこで、インフルエンザウイルスや毒素が結合する糖脂質に結合するペプチドをファージライブラリーによりセレクションして、ペプチドへの結合性および感染阻害活性について検討した。糖脂質に結合するペプチド配列のモチーフの同定も行った。また、インフルエンザウイルスのヘマグルチニンに結合できる糖鎖レプリカペプチドをファージ提示ペプチドライブラリーから検索した。ヘマグルチニンに結合したファージを溶出する糖鎖の種類により、数種類のペプチド配列を得ることが出来た。

さらには、動物実験において鼻粘膜よりより投与することによって、インフルエンザウイルスの増殖を抑制することにも成功した。さらには、ペプチド配列の最適化し、より高いターゲット結合性ペプチドを得るために、高次構造を有するペプチドを提示したファージライブラリーの作製、およびインフルエンザウイルス結合性のファージのペプチド配列を分子進化させたファージライブラリーの構築を目指した。これにより数種類の新たなファージライブラリーの構築に成功した。感染は多くの場合に糖鎖が関与していることが知られている。本研究ではファージ提示ペプチドライブラリーの手法を用いて糖鎖結合性ペプチドあるいは糖鎖レプリカペプチドをセレクションして、感染阻害剤の作製を行った。特に本年度は分子進化工学の手法を用いて阻害活性に優れたペプチド配列の探索を行った。糖脂質はウイルスや毒素の感染において受容体として関与していることから、糖脂質結合性ペプチドは感染阻害剤として利用できることが考えられる。そこで、インフルエンザウイルスや毒素が結合する糖脂質に結合するペプチドをファージライブラリーによりセレクションしたペプチド配列の最適化を行うために、サブライブラリーを作製してバイオパニングを実施し、更に結合活性に優れたペプチド配列を見出した。また、ファージ提示ペプチドライブラリーからセレクションされていたインフルエンザウイルスのヘマグルチニンに結合できる糖鎖レプリカペプチドの構造の最適を行った。具体的には過去にヘマグルチニンへの結合性を見出している配列にランダムな変異を導入してサブライブラリーを構築した。そのサブライブラリーを用いて新たにバイオパニングを実施して結合活性に優れた配列をセレクションした。得られたペプチド配列は、異なる亜型のインフルエンザウイルスのヘマグルチニンに結合し、細胞へのウイルスの感染を阻害することが示された。その阻害活性はもとの配列に対して顕著に向上する事が見出された。
高階関数型言語のためのソフトウェアモデル検査

高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張に関する研究を進め、その成果を論文として投稿した。検証の枠組みの拡張として、既存の高階関数型言語のための自動検証手法では扱えなかった関数の等価性や単調性などの関数の性質を扱えるようにした。具体的には、このような関数の性質に関する検証問題を既存の検証手法で扱える問題に帰着する方法を提案した。既存の高階関数型プログラムの自動検証手法のほとんどは、量化子を含まない一階の述語を用いてプログラムを抽象化することによって検証を行っている。しかし、量化子を含まない一階の述語という制限のため、関数の等価性など、全称や関数を用いないと表すことができない性質を扱えなかった。例えば、次のように定義された二つの関数sum、sum2が等しいということが検証できない。ここで、sumは1からnまでの整数の和を求める関数であり、sum2はそれを累積変数を用いて求めるものである。本研究では、このような全称および関数を用いないと表せない性質の検証問題を、既存の一階の述語のみを扱う検証問題に帰着する方法を提案した。この拡張した検証の枠祖みを基に、関数型言語OCamlのサブセットで書かれたプログラムを対象とする検証器のプロトタイプを実装した。実装した検証器をさまざまなプログラムに適用し、本手法の有効性を確かめた。ここまでに得られた成果を国内会議の場で発表し、同時に他の研究者との意見交換を行った。(抄録なし)高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張、高速化に関する研究を進め、その成果を論文として発表した。検証の枠組みの拡張として、既存の高階関数型言語のためのソフトウェアモデル検査器では扱えなかったリストや木構造などの再帰的データ構造、例外処理などを扱えるようにした。例えば,再帰的データ構造を扱えるようにするために、再帰的データ構造に対しても関数によるエンコード法を提案した。これによって再帰的データ構造を用いるプログラムから再帰的データ構造を用いない同じ意味のプログラムへと変換することができる。検証の枠組みの高速化として、既存の検証の枠組みで用いていた継続渡し形式変換の改良である選択的継続渡し形式変換を提案した。素朴な継続渡し形式変換では、変換後のプログラムが不必要に複雑になり、これによって変換後のプログラムに対して行われる高階モデル検査の計算量が不必要に増えてしまうという問題があった。これを回避するため、なるべく高階モデル検査の計算量が増えないような継続渡し形式変換を提案した。この改良によって高階モデル検査の計算量を抑えることができ、全体の検証時間を短縮することができる。また、別の高速化として、既存の検証の枠組みで用いていた述語抽象化の改良である選択的述語抽象化を提案した。この改良によって、抽象化の精度を上げることができ、全体の検証時間を短縮することができる。また、この拡張子した検証の枠組みを基に、関数型言語OCamlのサブセットで書かれたプログラムを対象とする検証器を実装した。さらに、検証速度を向上させるためのチューニング等を行った。ここまでに得られた成果を国際会議の場で発表し、同時に国外の研究者との意見交換を行った。当初の計画通り、高階モデル検査を用いた関数型言語のためのソフトウェアモデル検査器に関するテーマについて研究を進め、それを実用レベルに近づけるために様々な最適化や拡張を提案することができた.現時点でのソフトウェアモデル検査器では,検証に時間がかかりすぎて実用的なソフトウェアの検証には適用できない。そこで、検証時間のほとんどを占める述語抽象化、および、高階再帰スキームに対するモデル検査のアルゴリズムの改良、高速化を行う。改良したアルゴリズムを用いて、前年度に実装した検証器の改良を行う。その実装を用いて、様々なプログラムに対して複数の性質を検証し、この実装が実用的なものであることを確かめる。(抄録なし)
液晶反応場による分子認識:新コンセプトに基づく特異的反応制御手法への展開

液晶類似の規則性と液体としての流動性を合わせ持つ液晶を反応媒体として使用し、その高い異方性、配向性により、多岐にわたる有機反応を高度に制御し、酸素類に匹敵する高選択的高効率反応場(系)の構築を行い、新しいコンセプトに基づく反応制御系の確立と液晶制御の要因解明を目的とした。特に、従来成果の乏しい熱反応系に焦点を絞り研究を展開した。その結果、トランス-4-シクロヘキシルシクロヘキシルデカトリエンカルボン酸エステルを反応基質として、分子内熱環化反応を140°Cで行ったところ、スメクチック液晶bis(4-pentyloxypheny1)trans-1,4-cyclohexanedi-carboxylate(BPCD)中では、構造類似の等方性媒体4-pentyloxypheny1 cyclohexanecarboxylate(PCC)やメシチレン中とは明らかに異なる高いジアステレオ選択性と化学収率で進行した。立体選択性と化学収率の両面で液晶媒体の有用性を示すことができたが、これらは基質構造に大きく依存することが明らかになった。本知見は、規則性高い分子配列を持つ液晶独自の構造に起因しているものと思われ、魅力ある液晶反応場の可能性を示唆している。本研究による萌芽的成果により、所期の目的に適った急速な進展が期待できるようになった。