hpprc/llmjp-kaken huggingface dataset:
タニシの高度不飽和脂肪酸濃縮機構の解明と生物多様性保全への応用

動物の成長や繁殖に欠くことのできない栄養素である必須脂肪酸が,マルタニシやゼブラフィッシュなどの淡水動物のフンから検出されることが明らかとなった.顕微鏡観察によってフンには多くの原生動物が確認されたが,フンに含まれる原生動物密度と必須脂肪酸含有量には有意な正の相関が検出された.フンに原生動物が集まることで,フンに必須脂肪酸が加わったものと考えられた.フンの元となった餌には原生動物が集まらなかったことから,フンとなることで原生動物を惹きつけるようになると考えられた.マルタニシのフンから元となる餌には含まれていない必須脂肪酸が検出されること発見した.今年度は,マルタニシのフンに必須脂肪酸が含まれる機構を解明することを目的として研究を行った.まず,マルタニシのフンを回収し,20:4n6,20:5n3,22:6n3といった必須脂肪酸が餌には含まれていないにもかかわらず,フンに含まれていることを確認し,再現性のある現象であることを確認した.次にフンを顕微鏡で観察したところ,マルタニシのフンには鞭毛虫や繊毛虫などの原生動物が集まっていることが分かった.そこで,マルタニシのフンを排泄直後から7日後まで1日ごとに採集し,フンの脂肪酸組成とフン表面に存在する原生動物の個体数の関係を解析した.その結果,フンに含まれる20:4n6,20:5n3,22:6n3といった必須脂肪酸とフン表面の原生動物の個体数には有意な正の相関があった.既往の研究によれば,原生動物にはこれらの必須脂肪酸が含まれていることが指摘されている.フンから餌に含まれない必須脂肪酸が検出された原因は,これらの必須脂肪酸を含有する原生動物がフンに集まるためと解釈された.実験で利用したマルタニシの餌には原生動物が集まらなかったことから,マルタニシのフンが何かしらの機構で原生動物を引き付けていると考えられる.原生動物は高次の動物にとって餌源であるが,マルタニシのフンに集まることで高密度化すれば,高次の動物にとって,水中にまばらに存在する原生動物を集めながら捕食するよりも,マルタニシのフンを摂食した方が効率的に原生動物を食べることができると考えられる.今後はマルタニシのフンが生態系の食物網に果たす役割いついて検証を進めていくことが必要であると考えられる.動物の成長や繁殖に欠くことのできない栄養素である必須脂肪酸が,マルタニシやゼブラフィッシュなどの淡水動物のフンから検出されることが明らかとなった.顕微鏡観察によってフンには多くの原生動物が確認されたが,フンに含まれる原生動物密度と必須脂肪酸含有量には有意な正の相関が検出された.フンに原生動物が集まることで,フンに必須脂肪酸が加わったものと考えられた.フンの元となった餌には原生動物が集まらなかったことから,フンとなることで原生動物を惹きつけるようになると考えられた.高度不飽和脂肪酸のエイコサペンタエン酸(EPA)は生物膜の構成要素としての役割や,ホルモンの前駆物質としての役割を担っている。淡水生態系においてEPAの生産源は主に珪藻であり,動物は食物連鎖を介して珪藻を直接あるいは間接的に取り込むことでEPAを得ている。EPAが不足すると生残率や繁殖率が低下し,EPAは動物の生存上極めて重要な栄養素として認識されている。ところが高水温になる夏季の水田や富栄養化が進行した湖沼などでは珪藻が優占し難く,動物に対するEPAの供給量が減少してしまう。一方で申請者らは複数の水田において淡水産巻貝タニシのフンが餌として取り入れた底泥よりも多量のEPAを含んでいることを発見した。このことはタニシが珪藻の優占が難しい水田という場において他の水生動物にEPAを供給している可能性を示している。そこで本研究ではまずタニシがEPAを体内で合成し,フンとして排出する機能があるか確認するために,EPAを含まない餌である緑藻クロレラを用いてタニシを飼育し、フンの脂肪酸を分析した。その結果、タニシのフンからはEPAが検出され、タニシにEPAを合成する能力があることが明らかとなった。さらにEPAを合成する機構を解明するために、炭素13でラベルした必須脂肪酸でありEPAの前駆物質であるリノレン酸を含むクロレラを餌としてタニシを飼育し,タニシのフンの各脂肪酸の炭素安定同位体比を測定した。その結果,タニシのフンに含まれるEPAの炭素安定同位体比は,餌のリノレン酸の炭素安定同位体比から期待される値と比較して,大幅に小さかった。すなわち、タニシのフンに含まれるEPAは直近に食べた13Cラベルクロレラに含まれるリノレン酸から合成されているのではなく,過去に一度体内に蓄えたリノレン酸から合成したものであると考えられた。まず水生動物であるタニシにEPAを合成する能力があることを明らかにすることができた。そして当初予定していたタニシのEPAの濃縮機構の解明について,炭素13でラベルした餌を利用することで,直近に摂食した餌の脂肪酸以外の物質からEPAを合成していることが明らかとなった。また,タニシ体内の脂肪酸の炭素安定同位体比の変化についても予定通り明らかにすることができた。しかしながら,他の水生動物との共生実験において,ドジョウなど野生動物の室内飼育下の生残率が悪く,予定して分析をこなすことができなかった。今後はタニシのフンが実際の環境中で他の底生動物に摂食利用され,EPAの供給源として機能しているかを,現場調査によって明らかにする。

そのために,脂肪酸の炭素安定同位体比をトレーサーとした食物網解析手法を考案する。また,飼育実験において,タニシのフンを餌として与えることでドジョウなどを対象として,成長や生存にどのような影響を与えるか検討する。また,タニシのEPA合成機能がタニシ自身による作用か,腸内細菌による作用か分子生物学的な方法を利用しながら明らかにする。次年度使用額は室内共生実験で分析するはずであった動物サンプルが次年度に繰り越されたために発生したものであり,平成25年度請求額とあわせ,平成25年度の研究遂行に使用する予定である。
EDHFによる内膜肥厚の制御に関する探索研究

内膜肥厚は動脈硬化の主要な発生要因である.動脈では内皮細胞が内皮由来血管弛緩因子(一酸化窒素,EDNO)に加え,内皮由来膜過分極因子(EDHF)を遊離させることにより内膜肥厚を抑制すると考えられている.しかし,動脈グラフトにおける異常血流と内膜肥厚の関係,内膜肥厚とEDHFの機能変化との関係は不明である.動脈グラフトにおける内膜肥厚と異常血流の関係を検討するため,ウサギ動脈グラフトモデルを考案した(Tabata K et al., 2017).現在,この動物モデルを用いて,異常血流と内膜肥厚との関連を検討している.自家動脈グラフトは,麻酔下でウサギの右総頸動脈を採取し,その後,摘出した動脈を再び端々吻合することにより作成した(無結紮群).poor-runoff群は右内頸動脈を結紮するとともに,3本の右外頸動脈の分枝のうち1本,または2本を結紮することにより作成した(2分枝結紮グループ,3分枝結紮グループ).術後4週間経過した動物で,平均血圧,心拍数と右総頚動脈の血流を測定した.平均血圧と心拍数は3グループ(無結紮群,2分枝結紮群,3分枝結紮グループ)で変化が認められなかった.一方,右総頚動脈の血流は無結紮群>2分枝結紮群≧3分枝結紮グループであった.動脈血管のパラフィン固定標本を用いて,血管内腔の直径と血管壁の厚さを測定した.血管内腔の直径は,無結紮群≧2分枝結紮群>3分枝結紮グループであり,血管壁の厚さは,無結紮群>2分枝結紮群>3分枝結紮グループであった.本年研究より,動脈グラフトでの異常血流は,血管内腔の大きさを減少させ,血管壁を肥厚させることが明らかになった.現在,これらの結果を確認するための追加実験を行うとともに,摘出グラフトを用いて,異常血流と内皮由来弛緩因子の機能変化を検討するための研究に着手したところである.本研究は,自家動脈グラフトにおける異常血流と内膜肥厚,異常血流とEDHFの機能変化との関係を明らかにし,内膜肥厚を抑制するための有効な治療法を探索することを目的としたものである.本年度の結果は,動脈グラフトの異常血流が血管内腔の直径を減少させるとともに,血管壁を肥厚させること示唆した.研究は,現在のところ,おおむね順調に進行していると考えられる.本年度の研結果を確認するための追加実験を行うとともに,総頚動脈グラフトが正常血流および異常血流であるウサギより得た摘出標本を用いて,アセチルコリン(血管内皮刺激薬)による内皮依存性弛緩反応(内皮由来弛緩因子であるNOとEDHFの機能)変化と異常血流との関係を明らかにする.具体的には,正常血流および異常血流動物より得た動脈グラフトの摘出標本での内皮依存性血管弛緩反応を,NO合成阻害薬L-NNA(内皮細胞でのNO合成阻害⇒内皮由来NO依存性弛緩反応阻害)やKCa channel阻害薬(内皮細胞のKCa channel阻害⇒内皮細胞の過分極抑制⇒血管平滑筋細胞の過分極(EDHFの機能)阻害⇒血管弛緩反応抑制)存在下で検討することにより,異常血流とEDHFの機能変化との関係を明らかにする.内膜肥厚は動脈硬化の主要な発生要因である.動脈では内皮細胞が内皮由来血管弛緩因子(一酸化窒素,EDNO)に加え,内皮由来膜過分極因子(EDHF)を遊離させることにより内膜肥厚を抑制すると考えられている.しかし,動脈グラフトにおける異常血流と内膜肥厚の関係,内膜肥厚とEDHFの機能変化との関係は不明である.動脈グラフトにおける内膜肥厚と異常血流の関係を検討するため,ウサギ動脈グラフトモデルを考案した(Tabata K et al., 2017).現在,この動物モデルを用いて,異常血流と内膜肥厚との関連を検討している.自家動脈グラフトは,麻酔下でウサギの右総頸動脈を採取し,その後,摘出した動脈を再び端々吻合することにより作成した(無結紮群).poor-runoff群は右内頸動脈を結紮するとともに,3本の右外頸動脈の分枝のうち1本,または2本を結紮することにより作成した(2分枝結紮グループ,3分枝結紮グループ).術後4週間経過した動物で,平均血圧,心拍数と右総頚動脈の血流を測定した.平均血圧と心拍数は3グループ(無結紮群,2分枝結紮群,3分枝結紮グループ)で変化が認められなかった.一方,右総頚動脈の血流は無結紮群>2分枝結紮群≧3分枝結紮グループであった.動脈血管のパラフィン固定標本を用いて,血管内腔の直径と血管壁の厚さを測定した.血管内腔の直径は,無結紮群≧2分枝結紮群>3分枝結紮グループであり,血管壁の厚さは,無結紮群>2分枝結紮群>3分枝結紮グループであった.

本年研究より,動脈グラフトでの異常血流は,血管内腔の大きさを減少させ,血管壁を肥厚させることが明らかになった.現在,これらの結果を確認するための追加実験を行うとともに,摘出グラフトを用いて,異常血流と内皮由来弛緩因子の機能変化を検討するための研究に着手したところである.本研究は,自家動脈グラフトにおける異常血流と内膜肥厚,異常血流とEDHFの機能変化との関係を明らかにし,内膜肥厚を抑制するための有効な治療法を探索することを目的としたものである.本年度の結果は,動脈グラフトの異常血流が血管内腔の直径を減少させるとともに,血管壁を肥厚させること示唆した.研究は,現在のところ,おおむね順調に進行していると考えられる.本年度の研結果を確認するための追加実験を行うとともに,総頚動脈グラフトが正常血流および異常血流であるウサギより得た摘出標本を用いて,アセチルコリン(血管内皮刺激薬)による内皮依存性弛緩反応(内皮由来弛緩因子であるNOとEDHFの機能)変化と異常血流との関係を明らかにする.具体的には,正常血流および異常血流動物より得た動脈グラフトの摘出標本での内皮依存性血管弛緩反応を,NO合成阻害薬L-NNA(内皮細胞でのNO合成阻害⇒内皮由来NO依存性弛緩反応阻害)やKCa channel阻害薬(内皮細胞のKCa channel阻害⇒内皮細胞の過分極抑制⇒血管平滑筋細胞の過分極(EDHFの機能)阻害⇒血管弛緩反応抑制)存在下で検討することにより,異常血流とEDHFの機能変化との関係を明らかにする.<理由>今年度は,ウサギ動脈グラフトのpoor-runoffモデルを作成(モデルにおける血流変化と血管壁肥厚に関する実験系を確立)するために,多くの時間と経費(顕微鏡用デジタルカメラの購入など)をかけた.そのため,ウサギpoor-runoff動脈グラフトを使用した血管内皮由来弛緩因子(NOとEDHF)の機能変化に関する研究に十分な時間と経費を割くことができなかった.<使用計画>本年度の実験の追加実験をおこなうとおもに,次年度の研究計画に従い,poor-runoff動脈グラフトでの内皮機能変化(EDHFの機能変化)に関する研究を行う.この実験を遂行するための試薬やその他の消耗品の購入には,本年度未使用額と次年度の経費を充てる予定である.また,次年度の経費は,論文作成や関連する学会に出席するための旅費などにも使用する予定でる.
新規の超階層構造をもつポリオルガノホスファゼンの合成とその電子材料への応用

現在のところ,予備的に行った実験ではフェノキシ基をもつポリ(ビスフェノキシボスファゼン)[PN(0C_6H_5)_2]_n(PBPP)を新規カチオン重合により合成したところ,数平均分子量で3万程度となり,分子量分布は1.08程度でリビング的に反応が進行した。カチオン重合は次のようにして行った。1)オキシ塩化リンとフェノールを出発物質として,クロロベンゼン中,塩化マグネシウムを加え,室温で6時間反応させジフェニルリン酸クロリドを得る。2)得られたジフェニルリン酸クロリドにアンモニアとt-BMEを加えて-20°Cで1.5時間反応させ,ジフェニルリン酸アミンを得る。3)これに五塩化リン,ジクロロベンゼンを加え,室温で6時間反応させ,モノマーのトリクロロ-N-(ジフェノキシボスホリル)モノホスファゼンを得る。得られた化合物に触媒として塩化第一錫を加え60mmHg,150°Cで120時間反応させてPBPPを得た。4)このようにし耳得られたポリホスファゼンは従来のラジカル重合の溶液法に比べて,分子量も高くかつ分子量分布も狭い。また原料のPOCl_3も回収され,リサイクル可能である。PBPPの広角X線回折の結果,T(1)以上の140°Cにおいては,11.7Aの鋭いピークと4.6Aのブロードなピークが見出された。前者はおよそ主鎖長に対応し,後者は主鎖の繰り返し単位に対応する。従って,中間相において,主鎖は乱れ,側鎖は規則的に並ぶモデルが考えられる。X線回折の結果から室温相においても側鎖の規則性の予兆が現れている。PBPPの100Hzから100kHzにわたる複素誘電率(ε')及び誘電損失(ε'')の温度変化を,Fig3(a)及びFig.3(b)に示す。100Kから270Kにわたってε'はほぼ一定の3.5であるが,温度が上昇すると,主鎖のミクロブラウン運動が励起され,ε'は分散を示しながら上昇し,310Kで3.9に達する。ε''はそれとともに極大を示す。ε''は370K付近にはT(1)に起因する折れがみられる。さらに温度が上昇して,中間相になると温度上昇とともに,周波数の逆数に依存する電気伝導の増大により,ε',ε''はいずれも増大する。
アポトーシスシグナルの細胞内クロストークを基盤とした癌治療の基礎研究

1:細胞周期を制御するcdk2,cdk4の細胞生物学的意義を調べるために3T3細胞に優性抑制的cdk2(cdk2dn),cdk4(cdk4dn)の安定高発現細胞株を樹立した。細胞株のCdk2,cdk4活性はそれぞれ抑制された。血清除去によりG0/G1に細胞周期を止め、血清添加により細胞周期を動かすと両者とも親株に比べ2時間ほどS期への進行が遅延した。cdk2dn細胞ではcdk4キナーゼ活性は親株と同じに上昇したがcdk4dn細胞ではcdk4,cdk2ともに活性上昇が抑制された。血清除去によるアポトーシス誘導ではcdk2dn細胞は親株と違いがなかったがcdk4dn細胞ではアポトーシスが強く誘導された。以上よりcdk2,cdk4は細胞周期を同じように正に制御するが単にredundancyに働くのでなく、cdk4は血清因子に依存するサバイバルシグナルに関与すると考えられた。一方,cdk4とredundantに働くとされるcdk6について検討を加えたところ優性抑制性cdk6を高発現させた3T3細胞では細胞局期や細胞死に全く影響が認められなかった。このことはcdk4,cdk6は少なくとも3T3細胞においては生物学的に異なる機能を担う可能性が示された。2:野生型p53を発現するメラノーマ細胞(A2058)を用い,アロ抗原特異的細胞傷害生T細胞(CTL)を作製した。CTLはIL2依存性細胞株であり,cold target inhibition法にて特異性について確認した。細胞傷害活性については^<51>Cr放出法および細胞増殖指数によって検討した。標的細胞を今までに作製した遺伝子導入細胞(dominant negative変異型p53,dominant negative変異型IkBα,野生型IkBα過剰発現)を用い,細胞傷害に与える影響について検討した。細胞傷害の程度については,いずれの変異細胞もコントロール細胞と有意な相違は見られなかった。CTLから分泌されるgranulysin値を測定した場合,いずれの場合にも培養上清中に放出されるgranulysin値に有意な差を認めなかった。以上の事からCTLによるアロ抗原の認識とそれに引き続くCTLからの細胞傷害シグナルは同等である事,そしてCTLからの細胞傷害シグナルを受けた後の標的細胞の細胞障害(死)のシグナル伝達についてはNFkBやp53の経路は関与していない可能性が示された。悪性黒色腫から樹立したA2085細胞株は野生型p53を発現している。機能萌に野生型であることはp53依存性の遺伝子p21、BaxがUV,IR刺激にて誘導されること、また変異型p53を導入することにより抑制されることから示された。A2085細胞に野生型IkBα、優性抑制的に働くN端(1-36)除去のδN-IkBαの安定発現性細胞株を樹立した。3つの細胞をTNFαで刺激するとIkBα導入株では細胞死が促進された。

細胞をUV-Cで刺激すると野生型IkBα高発現細胞は細胞死が促進されたがδN-IkBα発現細胞では細胞死は促進されなかった。NFkBの活性化は2つの遺伝子導入細胞で著明に抑制されていることからUV-Cに対する反応性の違いはNFkBの抑制に依存しないことが予測された。UV-C刺激後のp53依存性に発現が調節されるアポトーシス促進因子であるBaxの発現を検討したところIkBα細胞ではBaxの発現が増強していた。p53の発現に相違は認められないことからIkBα細胞ではp53の転写活性が増強されていることが示唆された。無刺激の状態ではp53の転写活性に相違が認められないことからUV-C刺激後にp53あるいはIkBαが何らかの修飾を受けることが必要であることが示唆された。p53のリン酸化状態をリン酸化特異的抗体を使用して現在検討している。細胞周期を制御するcdk2, cdk4の細胞生物学的意義を調べるために3T3細胞に優性抑制的cdk2(cdk2dn), dk4(cdk4dn)の安定高発現性細胞を樹立した6細胞株のCdk2, cdk4活性はそれぞれ抑制された。血清除去によりGO/Glに細胞周期を止め、血清添加により細胞周期を動かすと両者とも親株に比べ2時間ほどS期への進行が遅延した。cdk2dn細胞ではcdk4キナゼ活性は親株と同じに上昇したがcdk4dn細胞ではcdk4, cdk2ともに活性上昇が抑制された。血清除去によるアポトーシス誘導ではcdk2dn細胞は親株と違いがなかったがcdk4dn細胞ではアポトーシスが強く誘導された。以上よりcdk2, cdk4は細胞周期を同じように正に制御するが単にredundancyに働くのでなく、cdk4は血清因子に依存するサバイバルシグナルに関与すると考えられた。年度の計画として細胞免疫を介した抗腫瘍効果の細胞生物学的解析を進める準備としてCTLの系を作成することを目標にしたが、その過程で今回CTLやNK細胞に発現し標的細胞を殺す際に分泌される蛋白質granulysinに関して研究を行なった。この蛋白には蛋白分解により15Kと9Kのアイソフォームがあることが知られていたが共同研究者らとともにこの分泌型蛋白質を認識するモノクローナル抗体を作成しELISA測定法を開発して検討を行なった。フローサイトメトリ法で解析するとgranulysinは一部のT細胞と殆どのNK細胞内に存在することが確認された。T細胞をIL2刺激で活性化しLAK細胞とすると細胞内のgranulysin陽性細胞は増加し、発現は亢進した。細胞培養液中の蛋白を測定すると15Kは検出されるが9Kは殆ど検出されなかった。健常人の血清を測定したところやはり15Kは検出されたが9Kは検出されなかった。NK細胞を標的細胞であるK562細胞と共培養するとkilling活性に比例して培養液中の15Kは増加したが9Kはごくわずか検出されるのみであった。NK細胞に分泌阻害剤を作用させると培養液中の15Kは減少することが示された。リコンビナント9K蛋白に細胞傷害活性があるという他施設の報告を考慮すると、CTL・NX細胞から15K蛋白は恒常的に分泌されているが標的細胞に作用すると15K、9K蛋白質が分泌されるが9Kは血清中の半減期が短く測定されにくいと推察される。
アクチナイド化合物の探索と結晶育成

本研究は、4f電子の異常な電子相関によって現われる重い電子状態や超伝導等の異常な磁性の発生機構を総合的に研究する重点領域研究「アクチナイド化合物の物性」(代表者:東北大学理学部教授糟谷忠雄)の分担グループとして、超高純度の試料を作成する東北大学金研片平、大洗両研究施設をセンターとする鈴木(謙)班を中心に、全国の10大学の約40名の研究者が利用できる既存の施設を拠点とするサテライト研究班を組織して、アクチナイド化合物の物質探索と純良単結晶の育成を目的として、系統的に研究を行った。研究期間が3年に短縮したため、国際規制物質として厳しい取り扱い規制を受けるアクチナイド化合物の中で、ウラン化合物を中心に研究目的を絞った。今年度は3年継続研究の2年度であるが、予算的にも多少恵まれ、東北大学、広島大学、筑波大学を中心に結晶育成装置も整備され、ウランプニクタイトやウラン3元系化合物(UaTbXc)の新しい物質の探索が系統的に行えるようになり、物理学会での発表の数も年間55編と急激に増加した。主な研究成果は、既知の結晶構造のウラン3元系化合物(UaTbXc)の物性開発に対する研究に各班が集中している感があるが、広島大学の藤井グループが(111)、(112)化合物の異常磁性の研究に、北大の都グループはURu_2Si_2系の超伝導の発生機構に関わる研究に、筑波大学の大貫グループはdHvA効果を目的としたウラン化合物の開発に、また東北大学の小松原グループはUーPtーSi系の物質探索に、鈴木グループはウランプニクタイトの物質探索に、それぞれ成果を挙げた。今年度の後半に結晶育成装置がセンターを中心に整備され、我が国のウラン化合物の研究の著しい後進的状況を回復しつつあるので、最終年度への継続による研究成果の発展が充分に期待される実績を挙げた。
ブタ始原生殖細胞の体外培養およびブタEG細胞株の作出

マウス胚性幹(ES)細胞や始原生殖(PGC)細胞由来のEG細胞のように多能性を維持し、さらに次世代の子孫が得られる細胞株は、ブタをはじめ家畜では得られていない。そこで本研究では、妊娠2233日齢のブタ胎仔よりPGC細胞を採取し、EG細胞株を樹立するために体外培養を試みた。本研究の結果から以下の知見が得られた。1)胎仔の生殖隆起をコラーゲナーゼ・ディスパーゼ液で解離後、抗体磁気ビーズを用いて選択的にPGC細胞を単離・精製する手法につい検討した。その結果、高い回収率、高い純度でPGC細胞が得られることが明らかとなった。しかしながら、得られたPGC細胞の生存率は低く、胎仔採取から細胞の分離までの処理方法についてさらに検討する必要があることが示唆された。2)膜結合型SCF(幹細胞成長因子)を発現するフィーダー細胞(S14-m220細胞)を用いて、PGC細胞の培養を試みた。その結果、S14-m220細胞をフィーダー細胞に用いることによりPGC細胞数がSTO細胞に比べ多くなることが明らかとなった。3)PGC細胞の培養における成長因子の影響について検討した。その結果、PGC細胞をLIF(白血病成長因子)、SCF、bFGF(塩基性線維芽細胞成長因子)の成長因子を添加した培養液中で培養した場合、PGC細胞の増殖は促進されなかった。しかし、これらの因子の他にFK(フォリスコリン)を添加した培養液中で培養した場合、ALP活性の高い細胞が著しく多く増殖することが明らかとなった。Buffalo Rat Liver(BRL)細胞の培養上清液およびアセチルシステインについても検討したが、これらには著しい促進効果は認めれれなかった。以上の培養条件下で継代培養を試みたが、アルカリフォスファターゼ(ALP)活性およびSSEA-1抗体陽性のES細胞様の細胞株は得られなかった。そこで本研究では、ブタ妊娠胎仔よりPGC細胞を採取し、EG細胞株を樹立するために体外培養を試みた。また、EG細胞株が得られた場合に、同細胞のキメラ形成能を確認するためにレシピエント胚が必須であることから、ブタ卵胞卵子の体外成熟・受精および体外培養系について検討した。1)妊娠26日齢の生殖隆起をトリプシン液やコラ-ゲナーゼ液で処理してPGC細胞を採取した場合、PGC細胞以外の体細胞の増殖が著しく、細胞懸濁液からPGC細胞のみを精製する必要があることが明らかとなった。また、PBS-EDTA液中で採取した場合、体細胞の混入は少なくなるものの、採取細胞数が減少することが明らかとなった。現在、PGC細胞の精製方法について引き続き検討中である。2)採取されたPGC細胞をLIF(白血病成長因子)、SCF(幹細胞成長因子)、bFGF(塩基性線維芽細胞成長因子)、TNF(腫瘍壊死因子)等の成長因子を添加した培養液中で培養した場合、PGC細胞の増殖は促進されず、また、アルカリフォスファターゼ(ALP)活性およびSSEA-1抗体陽性のES細胞様コロニーは得られなかった。現在、用いるフィーダー細胞について株化細胞およびマウスおよびブタ体細胞を用いて検討している。3)ブタ卵胞卵子の体外受精は用いる種雄ブタにより著しく影響したが、胚盤胞期まで発生させる培養系を確立することができた。また、受精卵子の体外培養における気相について検討した結果、低酸素状態で培養することにより胚盤胞期への発生率が高くなることが明らかとなった。

Buffalo Rat Liver(BRL)細胞の培養上清液およびアセチルシステインについても検討したが、これらには著しい促進効果は認めれれなかった。以上の培養条件下で継代培養を試みたが、アルカリフォスファターゼ(ALP)活性およびSSEA-1抗体陽性のES細胞様の細胞株は得られなかった。
化学兵器由来と考えられるジフェニルアルシン酸中毒の臨床学的研究と治療法の開発

平成15年(2003年)3月飲用井戸水に混入したジフェニルアルシン酸(DPAA)による健康被害が茨城県で発覚し、中毒症状として、運動失調,ミオクローヌス,振戦などの小脳・脳幹症状を中心に後頭葉、側頭葉の症状が確認された。小児では精神運動発達遅滞もみられた。151名がDPAA暴露者と認定されて、健康診査を定期的に施行している。脳血流シンチグラフの定量的画像統計解析法にて小脳・脳幹と後頭葉の有意な血流低下が示された。ポジトロン・エミッション・トモグラフ(PET)でも同様の脳部位に糖代謝低下が認められ、神経症状と画像変化脳部位が一致した。DPAA暴露の臨床マーカー(客観的生体指標)として活用できると考えられる。DPAA曝露者の生体試料(尿、毛髪、爪、血清、血球、髄液等)から抽出分離を行い、LC-ICP/MS, LC/MS/MSでDPAAと生体内代謝物と考えられるフェニルアルソン酸、フェニルメチルアルシン酸を新たに同定、定量した。モデル動物実験ではラットにDPAA(5mg/kg/day)の28日間連続経口投与を実施し、ヒトと同様な症状発現に成功した。さらに各臓器におけるDPAAとその代謝物を定量し、体内分布を調べた。DPAAは大脳、小脳、脊髄などの中枢神経系に移行はし難いが、一度、移行すると中枢からの排泄は遅い傾向がみられ、投与中止14日後でも中枢神経ではDPAAおよび生体内代謝物の残留傾向がみられた。特に小脳・脳幹に有意に蓄積しやすいことが判明した。ジフェニルアルシン酸の排泄経路として尿から約50%糞便中から約50%排泄されることが明らかになった。糞便中の排泄量を経時グラフにするとDPAAは腸肝循環していることが判り、この腸肝循環を断ち切る吸着剤が体外排泄を促進させ、DPAAの急性期治療として利用できると考えられた。今後、候補物質による体外排泄促進実験を実施したい。茨城県神栖町飲用井戸水汚染によるDPAA中毒は、世界で最初の報告である。DPAA中毒の症状は、ミオクローヌス、振戦、小脳失調などの小脳-脳幹由来の症状と視覚異常、睡眠障害、記銘力障害などの後頭葉、側頭葉由来の症状であった。これら各症状は入院後(飲水中止後)12週間で徐々に軽快し、退院後(飲水開始後)12ヶ月で症状が増悪するという特徴を示していた。加えて小児では精神運動発達遅滞がみられた。高濃度汚染地域(A地区)と比較的高濃度汚染地域(B地区)が明らかになっているが、汚染濃度はA地区にてDPAA約15mg/L、B地区ではA地区の1/10程度の汚染であった。平成17年度末の曝露認定者135名の生活因子、臨床所見、検査所見、生体試料中DPAA濃度をデータベース化し、様々の解析を試みた。既述の各症状・症候の出現頻度をA地区(34名)、B地区(67名)で比較したところ、A地区で各症状出現が有意に高かった。(_X2検定:p<0.01)脳血流シンチグラフィの解析では(1)側頭・後頭部、(2)小脳、(3)側頭葉内側部(海馬付近)の血流低下がみられ、急性期の症状責任部位に一致していた。

症状の改善に伴い脳血流低下が改善していることから、これら脳血流シンチグラフィは有機ヒ素中毒におけるバイオマーカーになる可能性が考えられた。また、複数の曝露者の尿中DPAA及び爪、毛髪中DPAAを測定したところ、曝露中止後約300日で尿中DPAAは検出されなくなった。爪からは曝露中止後3年以上経てもDPAAが検出された。これらの知見は、新たにDPAA中毒が発生した場合に有用な情報になると考えられた。DPAA中毒が発覚して約2年経過したが、後遺障害と考えられる症状も認められることから、住民健診を継続して行っていく必要がある。今後、DPAAの体内動態や中枢神経系への蓄積の有無、DPAAの神経細胞障害性など、本研究を通して明らかにする予定である。平成15年(2003年)3月飲用井戸水に混入したDPAAによる健康被害が茨城県で発覚し、現在までに高濃度暴露者(12mg/kgの暴露;A地区)と比較的高濃度暴露者(0.1mg/kg以下の暴露;B地区)併せて135名が暴露者と認定され、定期的に健康診査を実施されている。本中毒の臨床症状は多彩で小脳-脳幹症状と思われる運動失調、ミオクローヌス、振戦に加え、睡眠障害、記銘力障害、視覚異常などである。これら症状は、一過性であり暴露中止後により数週間でほぼ消失するが、小児では精神運動発達遅滞をみとめる例もある。さらに多動傾向、学習障害などADHD様の症状を示す児や自律神経障害を示す児もみられ、DPAAとの関連が疑われている。小児の一部に肝機能障害、脳波異常や軽度の脳萎縮が認められた。脳血流シンチグラフの定性的視覚的解析では(1)側頭・後頭部、(2)小脳、(3)側頭葉内側部(海馬付近)の血流低下傾向がみられ、この脳血流低下部位は、急性期の症状責任部位に一致していた。また慢性期のA地区暴露者や症状がないB地区暴露者でも高率に同部位の脳血流低下が認められた。DPAA暴露におけるこれら特定脳部位の血流低下の意義を明らかにするため、暴露者のFDG-PET解析、若年健常者の脳血流データベース作成、モデル動物におけるPETを行っている。生体試料からのDPAA検出は暴露の指標である。量の測定、解析において、暴露中止後も血清からは約200日、尿からは約300日経てもDPAAが検出される。爪は3年以上経てもDPAAが検出された。髄液からもDPAA検出は可能で、髄液中DPAA濃度は血清中の3-5%の濃度であった。本中毒の臨床マーカー候補として、生体試料の血液、尿、爪、毛髪および脳血流シンチグラフが挙げられるが、特に脳血流シンチグラフはDPAAの生体影響を測る臨床マーカーとして有用と考える。慢性期症状を有する健康被害者や、小児では精神運動発達遅滞なども認められることから、今後も厳重な追跡調査が必要と思われる。平成15年(2003年)3月飲用井戸水に混入したジフェニルアルシン酸(DPAA)による健康被害が茨城県で発覚し、中毒症状として、運動失調,ミオクローヌス,振戦などの小脳・脳幹症状を中心に後頭葉、側頭葉の症状が確認されている。さらに小児では精神運動発達遅滞もみとめられる。現在までに151名が暴露者と認定されて、健康診査を定期的に施行している。脳血流シンチグラフで小脳・脳幹と後頭葉の血流低下が明らかになり、定量的画像統計解析法にて有意に血流低下していることが示された。ポジトロン・エミッション・トモグラフ(PET)でも同様の脳部位に糖代謝低下が見られたことから、DPAA暴露の臨床マーカー(客観的生体指標)として活用できると考えられる。
大分県大野川流域における旧石器時代の研究

59年度および61年度に発掘調査を実施した大分県大野町の宮地前遺跡と大野郡犬飼町の松山遺跡の資料整理・分析と報告書作成を主として行った.その他,両遺跡の資料整理・分析に関連する遺跡の資料収集調査を,宮崎県児湯郡周辺と京都文化財団において実施した.また,松山遺跡については周辺の表面採集と土層観察のための調査を実施して, 61年度の発掘調査の補強を行い,ローム層の堆積と遺物包含層の関係を確かめた.宮地前遺跡については,細石器文化層の上部に文化層が認められた弥生時代中期を主体とする土器,縄文時代晩期の土器・石器の実測・トレースが終了し,現在,図版および観察表の作成にかかっている.細石器時代の石器についても実測・トレースが終了し,平面・垂直分布と個体別資料化の分析を進めている.報告書用の原稿・図版・写真については, 4月上旬完成を目指して,最終段階に入っている.先年行われた平安博物館の宮地前遺跡の調査では不明であった弥生中期の城ノ越式土器や縄文晩期の石包丁形石器について新たな知見を得た.また,細石器文化についても,資料数は必ずしも多くないが,石器群と包含層,さらに生活面の実態を把握することができた.いっぽう,松山遺跡は資料整理のための基礎作業である洗い・ナンバリング・台帳づけを完了し,さらに,平面・垂直分布図の作成,接合資料および個体別資料化の作業もほぼ終わり,石器の実測を現在進めている.松山遺跡では, 12組53点の接合ができ,特に18点の細石核ブランクの接合資料は「船野型細石核」の製作過程を考察する上で,重要視される.また,これらの接合資料・個体別資料はこれから行う遺跡構造の分析で大いに利用できるものと考えられる.なお,松山遺跡については, 63年1月に「大野郡松山遺跡の調査速報」として, 8ページの印刷物で,石器群のブロックなど研究実績の一端を,発表した.61年度の具体的な調査は、大分県大野郡大野町の宮地前遺跡の発掘調査とその整理に重点をおいて進めることを心がけた。宮地前遺跡の発掘調査は、61年12月の中旬から下旬にかけての14日間実施した。14層までは客土層および攪乱層で、弥生時代前期中期の土器片、縄文時代晩期の土器・石器が混在し、しかも細片の状態で出土した。5層は縄文時代晩期の包含層で土器片・偏平打製石斧が出土。さらに、堅穴住居跡と考えられる遺構の一部が検出された。7層はソフトローム層への漸移層。この層から8層のソフトローム層の上部にかけてが旧石器時代の遺物包含層。細石刃・剥片それに台石などが出土したが、石器群の数は必ずしも多くなかった。包含層までの深さが3メートルを越え、縄文時代晩期の包含層が厚く堆積し、さらに遺構の一部がかかっており、石器群の集中が予測される地域までは発掘出来なかった。大野川流域の旧石器時代の遺跡(大野郡犬飼町の松山遺跡)が、破壊されるということで、62年2月に2週間表面調査および発掘調査を緊急に実施した。ローム層への漸移層およびローム層の上部まで削平され、流紋岩製の石器・石片などが多量に露出していた。3月に予定されている耕作・作付けによって、破壊される地点の約90ヘーベの発掘調査とその周辺の表面調査を行った。細石刃・細石核、ナイフ形石器、剥片・砕片など、流紋岩製の石器類約600点が漸移層からローム層上部にかけて、良好な状態で出土した。表面調査でも、削器・ナイフ形石器・剥片など多数発見され、予想以上の成果をあげることができた。今後、松山遺跡は大野川中流域における細石器文化の重要な遺跡として注目されるものと確信している。資料の収集(記録化)は、松山遺跡の緊急調査のため宮崎平野周辺出土の細石器関係資料の一部だけにとどまった。59年度および61年度に発掘調査を実施した大分県大野町の宮地前遺跡と大野郡犬飼町の松山遺跡の資料整理・分析と報告書作成を主として行った.その他,両遺跡の資料整理・分析に関連する遺跡の資料収集調査を,宮崎県児湯郡周辺と京都文化財団において実施した.また,松山遺跡については周辺の表面採集と土層観察のための調査を実施して, 61年度の発掘調査の補強を行い,ローム層の堆積と遺物包含層の関係を確かめた.宮地前遺跡については,細石器文化層の上部に文化層が認められた弥生時代中期を主体とする土器,縄文時代晩期の土器・石器の実測・トレースが終了し,現在,図版および観察表の作成にかかっている.細石器時代の石器についても実測・トレースが終了し,平面・垂直分布と個体別資料化の分析を進めている.報告書用の原稿・図版・写真については, 4月上旬完成を目指して,最終段階に入っている.先年行われた平安博物館の宮地前遺跡の調査では不明であった弥生中期の城ノ越式土器や縄文晩期の石包丁形石器について新たな知見を得た.また,細石器文化についても,資料数は必ずしも多くないが,石器群と包含層,さらに生活面の実態を把握することができた.

いっぽう,松山遺跡は資料整理のための基礎作業である洗い・ナンバリング・台帳づけを完了し,さらに,平面・垂直分布図の作成,接合資料および個体別資料化の作業もほぼ終わり,石器の実測を現在進めている.松山遺跡では, 12組53点の接合ができ,特に18点の細石核ブランクの接合資料は「船野型細石核」の製作過程を考察する上で,重要視される.また,これらの接合資料・個体別資料はこれから行う遺跡構造の分析で大いに利用できるものと考えられる.なお,松山遺跡については, 63年1月に「大野郡松山遺跡の調査速報」として, 8ページの印刷物で,石器群のブロックなど研究実績の一端を,発表した.
曲面の写像類群とモジュライ空間の幾何学

本研究では,曲面の写像類群とリーマン面のモジュライ空間の構造の解明を中心課題とし,それに密接に関連する種々の問題についての研究を行った.具体的には,写像類群のコホモロジー群の研究,Floerホモトピー型の理論の展開,3次元多様体のゲージ理論に基づく位相不変量の研究,写像類群の調和的Magnus展開の理論の建設,Grothendieck-Teichm\"uller群の構造の研究,3次元多様体論における体積予想の研究,3・4次元における非可換幾何学の展開,写像類群の有限部分群と特性類の関係に関する研究,写像類群のJohes表現の研究,写像類群と4次元多様体論との関連,等である.このように代表者および各分担者はそれぞれのテーマを追究する一方で,相互啓発により一段高い観点からの研究を目指した.その中から,例えば写像類群の幾何学とシンプレティック幾何学との結びつきや,写像類群と自由群の外部自己同型群の構造の類似点および相違点の解明等の新しい研究の方向も見えてきた.本研究では,曲面の写像類群とリーマン面のモジュライ空間の構造の解明を中心課題とし,それに密接に関連する種々の問題についての研究を行った.具体的には,写像類群のコホモロジー群の研究,Floerホモトピー型の理論の展開,3次元多様体のゲージ理論に基づく位相不変量の研究,写像類群の調和的Magnus展開の理論の建設,Grothendieck-Teichm\"uller群の構造の研究,3次元多様体論における体積予想の研究,3・4次元における非可換幾何学の展開,写像類群の有限部分群と特性類の関係に関する研究,写像類群のJohes表現の研究,写像類群と4次元多様体論との関連,等である.このように代表者および各分担者はそれぞれのテーマを追究する一方で,相互啓発により一段高い観点からの研究を目指した.その中から,例えば写像類群の幾何学とシンプレティック幾何学との結びつきや,写像類群と自由群の外部自己同型群の構造の類似点および相違点の解明等の新しい研究の方向も見えてきた.曲面の写像類群の構造と,リーマン面のモジュライ空間の幾何学について,主として位相幾何学の観点からの研究を行った.本年度に得られた結果を具体的に記すと,つぎのようになる.1.研究代表者は,8月にStanford大学で開催された,「Topology of Moduli Spaces」と題する国際研究集会に参加し,これまでの成果を発表すると共に,多くの研究者と研究討論を行った.その結果,Getzler氏との討論でつぎのことが分かった.すなわち,シンプレクティック群の表現論とtrivalentグラフの不変量を用いてリーマン面のモジュライ空間のtautological代数を記述する,代表者と分担者の河澄氏との仕事を,puncturesが二個以上の場合に一般化すれば,Getzler氏が種数2で得ていた関係式を一般化するような関係式を得る可能性が大きい.現在,この方向で研究を続行中である.2.分担者の古田は,研究協力者とともにゲージ理論を用いた3次元および4次元多様体の研究を進め,新しく導入した不変量の性質を詳しく調べた.3.代表者とMillerによる,Mumford-Morita類の代数的独立性に関する定理について,曲面の有限位数の自己同型の幾何学的性質のみを用いた新しい証明が得られた(秋田-河澄-植村).4.分担者の廣瀬は,スピン写像類群の表示と,その4次元トポロジーヘの興味深い応用を得た.曲面の写像類群の構造と,リーマン面のモジュライ空間の幾何学について,引き続き位相幾何学の観点からの研究を行った.本年度に得られた結果を具体的に記すと,つぎのようになる.2.研究代表者は,D.Kotschick氏と共同で,任意の種数$g\geq 3$に対して,曲面上の種数$g$の葉層曲面バンドルで,全ホロノミー群が曲面の面積保存微分同相群に入り,かつ符号数が消えないものが豊富に存在することを証明した.これは,写像類群の幾何学とシンプレクティック幾何学との結びつきを示唆するもので,新しい研究の方向が得られた.3.分担者の古田は,研究協力者とともにSeiberg-Witten理論のホモトピー版を用いた3次元および4次元多様体の研究を引き続いて進め,いくつかの新しい結果を得た.4.分担者の河澄は,超楕円写像類群上のMumford-Morita類と,Weierstrass点との間の興味深い関連を発見した.5.分担者の廣瀬は,把手体の写像類群に関する研究を,4次元多様体の中に埋め込まれた曲面の幾何学に応用した.曲面の写像類群およびリーマン面のモジュライ空間の幾何学について,引き続き位相幾何学の観点からの研究を行った.本年度に得られた結果を具体的に記すと,つぎのようになる.1.研究代表者は,9月に京都の竜谷大学で開催された,「Geometry of Foliations 2003」と題する国際研究集会に参加し,これまでの成果を発表すると共に,多くの研究者と研究討論を行った.2.研究代表者はD.Kotschick氏と共同で,前年度の結果を使うことにより,面積保存微分同相群に全ホロノミー群が入る葉層曲面束の特性類を定義し,それらが非自明であることを証明した.これは,写像類群の幾何学とシンプレクティック幾何学とのさらに深い結びつきを示すものである.

3.分担者の古田は,Seiberg-Witten理論に対応するFloerホモトピー理論を展開するために,パラメータつきFredholmユニヴァースの概念を定義し,いくつかの新しい結果を得た.4.分担者の河澄は,拡大Johnson準同型の考え方を用いた森田Mumford類の微分形式表示をし調べ,それらの背景にあるMagnus展開を群コホモロジーと複素解析の両面から研究した.5.分担者の中村は,絶対Galois群のTeichmullerモジュラー群への作用,とくにDehn twist生成元への作用を具体的に記述する方法を解明した.
無限構造を扱うプログラム推論を用いたソフトウェア検証方法の確立

本研究は,リアクティブ・システムなど無限に継続する状態を扱うソフトウェアの正当性検証に向けた方法論の確立を目的とする.そのために,計算論理に基づくプログラム推論技術を中核に用いる点に特徴がある.次のような3つの研究成果を得た.(1)推論に用いる余論理プログラム(co-logic programs)とホーンμ-計算(Horn μ-calculus)に関する諸性質やその応用を示した.(2)検証に必要な仕様を実行ログから導出する仕様発見アルゴリズムを提案した.(3)仕様表現に必要とされる時間等の量的制約も含むパターン発見アルゴリズムの設計と効率的な実装を行った.本研究では,リアクティブ・システムなどのソフトウェアの正当性を検証する検証システムのための方法論を構築することを目的とする.そのために,計算論理に基づく形式的手法である論理プログラムに対するプログラム推論技術を用いるアプローチをとる.研究提案者は,先行研究で余論理(co-logic)プログラムに対するプログラム推論の枠組みを提案した.余論理プログラムは,リアクティブ・システムの記述に必要な無限項を自然に扱える特長を持つことに着目し,確定余論理プログラムに対するプログラム推論方法を与えた.研究計画1年目は,この結果を拡張するためにホーンμ-計算(Horn μ-calculus)に着目した.述語の否定を計算する双対(dual)プログラムを導出する否定除去技法を利用し,ホーンμ-計算の枠組みで双対プログラムを定式化した.そして,従来の主要なプログラムの意味論である有礎モデル(well-founded model)や解集合(answer set)について,ホーンμ-プログラムとの関係を示した.特に,有礎モデルの双対プログラムの不動点による特徴付けを示した.また,プログラムの検証では,プログラムが与えられた仕様を満たしているかを調べることが前提であるが,その仕様を与えること自体が難しい課題である.この仕様を自動的に導出するためのパターン発見アルゴリズムについて検討した.その基礎となるパターン発見アルゴリズムの設計と効率的な実現についての見通しを得ることができた.これまでの結果から,モデル検査などのシステム検証問題に対して余論理プログラムを用いた推論方法によるアプローチが有効で効率的な実装につながることが分かった.これにより,プログラム推論に基づくシステムの検証方法の開発に貢献する点で意義がある.本研究では計算論理技術に基づくシステム検証の方法論を構築するために,プログラム推論技術の理論的枠組みの構築と,検証システム実現のための余論理プログラミング技術の蓄積,そしてその有効性・妥当性の実証という研究サイクルを遂行するための課題を設定している.その中で,研究計画の1年目は特に以下のようなタスクについて研究を行った.プログラム推論の理論的基盤については,研究提案者は先行研究で余論理プログラムに対するプログラム変換の枠組みを提案した.この枠組みを拡張しより広い対象を扱うために,ホーンμ-計算に着目し,ホーンμ-計算の枠組みで双対プログラムを定式化した.これにより,より広いクラスの余論理プログラムにも適用可能になった.この点ではほぼ予定通り順調に進行している.また,検証システムにおいて必要となるプログラムの仕様について,その仕様を自動的に導出するパターン発見アルゴリズムの検討に着手した.その基礎となるパターン発見アルゴリズムの設計と効率的な実現についての見通しを得ることができ,概ね予定通りに進行している.更に,変換による検証のアプローチの有効性を確認するための実験については,検証システム実現のための余論理プログラミング技術について,時制論理式などいくつかの例題を通してその有効性を確認した.以上から,研究計画に従ってほぼ予定通り順調に進行している.本研究の目的は,リアクティブ・システムなどのソフトウェアの正当性を検証する検証システムを構築するための方法論を確立することにある.そのために,計算論理に基づく形式的手法である論理プログラムに対するプログラム推論技術を採用している.本研究では,リアクティブ・システムの記述に必要な無限構造を自然に扱える余論理(co-logic)プログラムとそのプログラム推論方法を基礎としている.研究計画1年目では,ホーンμ-計算(Horn μ-calculus)に着目し,その性質と応用可能性を調べた.余論理プログラムを拡張してその双対プログラムを考えて,その定式化をホーンμ-計算を用いて行った.また,主要なプログラムの意味論である有礎モデルや解集合について,ホーンμ-プログラムとの関係を示した.研究計画2年目は,これらの結果を拡張し理論的解析を行った.ホーンμ-計算が余論理プログラムの真の拡張であり余論理プログラムに課される構文的制約を必要としない枠組みであることを示した.さらにそのためのプログラム推論の規則や拡張された双対プログラムを示した.また,プログラム検証に必要になる仕様をログから自動的に導出する仕様発見については,プログラム実行のログを格納した系列データから再現(recurrent)ルールというパターンを発見する方法による仕様発見アルゴリズムについて検討を進めた.また,その基礎となる時間等の量的制約を表現する区間パターン発見アルゴリズムの設計と効率的な実現に基本検討を行った.これまでの研究結果から,モデル検査などのシステム検証問題に対して余論理プログラムやホーンμ-計算を用いた推論方法が有効であるという知見が得られた.このことは,プログラム推論に基づくシステムの検証方法の開発に貢献する意義がある.本研究では計算論理技術に基づくシステム検証の方法論を構築するために,プログラム推論技術の理論的枠組みの構築と,検証システム実現のための余論理プログラミング技術の蓄積,そしてその有効性・妥当性の実証という研究サイクルを遂行するための課題を設定して行っている.研究計画2年目は,特に以下のようなタスクについて研究を行った.プログラム推論の理論的枠組みについては,これまでの枠組みを拡張しより広い対象を扱うためにホーンμ-計算について,その性質と応用可能性を引き続き検討した.

ホーンμ-計算にプログラム推論の規則や拡張された双対プログラムを定式化した.これにより,余論理プログラムにもとづく推論方式の適用可能性をより広げることができた.この点ではほぼ予定通り順調に進行している.また,プログラム検証に必要な仕様をログから自動的に導出する仕様発見については,ログ系列データから再現ルール発見アルゴリズムの検討を続け,その実現に着手した.それを改良して効率的な実現についての見通しを得て,概ね予定通りに進行している.変換による検証のアプローチの有効性を確認するための実験については,再現ルールから発見される時制論理式を対象にして,それを検証するためのシステム実現に向けて,余論理プログラミング技術に基づく方法の有効性を確認した.以上から,研究計画に従ってほぼ予定通り順調に進行している.本研究では,リアクティブ・システムなどの状態が無限に継続する対象を扱うソフトウェアの正当性を検証する検証システム構築のための方法論を確立することを目的としている.そのために,計算論理に基づく論理プログラムに対するプログラム推論技術を中核に用いる点が特徴である.本研究で対象とする論理プログラムは,リアクティブ・システムの記述に必要な無限構造を自然に扱える余論理(co-logic)プログラムを基礎としている.その余論理プログラムとホーンμ-計算(Horn μ-calculus)との関連性に着目し,その性質とプログラム推論方法についての検討を行った.そのなかで,ホーンμ-計算が余論理プログラムをその一クラスとして扱えるより一般的な枠組みであることを示した.また,論理プログラムにおける主要な意味論である有礎モデルと解集合を取り上げ,ホーンμ-プログラムとの関係を調べた.また,プログラム検証に必要な仕様をユーザがあらかじめ正確に与えることは難しい問題である.そのために,実行ログから自動的に導出する仕様発見のアプローチを採用した.プログラム実行のログを格納した系列データから再現(recurrent)ルールというパターンを発見する仕様発見アルゴリズムについて,効率の良いアルゴリズムの検討と実装を行った.また,仕様表現に必要とされる時間等の量的制約を表現する区間パターン発見アルゴリズムの設計と効率的な実現も行った.本研究の結果から,モデル検査などのシステム検証問題に対して余論理プログラムやホーンμ-計算を用いた計算論理に基づく推論方法の有効性を示す知見を得た.このことは,仕様発見機能を備えたプログラム推論に基づくシステムの検証方法の実現に貢献する意義がある.本研究は,リアクティブ・システムなど無限に継続する状態を扱うソフトウェアの正当性検証に向けた方法論の確立を目的とする.