--- a/youshiki/5-1.tex	Wed Feb 20 21:17:10 2008 +0900
+++ b/youshiki/5-1.tex	Wed Feb 20 22:56:27 2008 +0900
@@ -63,7 +63,7 @@
 }
 
 \def\論文題目{
-線形時相論理による Continuation based C プログラムの検証
+線形時相論理を用いた Continuation based C プログラムの検証
 }
 \def\題目位置{17.74cm} % タイトルが 1 行のとき
 %\def\題目位置{17.56cm} % タイトルが 2 行のとき
@@ -77,7 +77,7 @@
 まず、非決定性を含むプログラムとして並列プログラムをとりあげ、
 継続を基本とする言語Continuation based C(CbC)で記述し、
 そのプログラムに対してタブロー法と線形時相論理を用いて検証する手法を示している。
-次に、実装したプログラムを他の検証ツールであるSPINと
+非決定性を含むプログラムを検証するために、可能な実行すべてを検
 %家庭用ゲーム機で動作するゲームプログラムの分割の単位として、
 %ゲームプログラムを実行可能に分割すること(Demonstration)を提案している。
 %また、
@@ -90,12 +90,28 @@
 
 %page 2
 \def\審査要旨b{
+査し、プログラムの持つ状態をすべて展開している。
+
+~~次に、実装したプログラムを他のモデル検査ツールであるSPINと
 Java PathFinderの２つと比較している。
-実行時間においては他の検証ツールより遅いという結果になっているが、
+実行時間においては他のモデル検査ツールより遅いという結果になっているが、
 実用に耐え得る速度であることが示されている。
-また、SPINとJava PathFinderはシミュレーションによる検証であるが、
-CbCでは、実際のプログラムを直接実行することによる検証であるため、
-この部分にエラーが入ることはないのがCbCによる検証の利点であることが示された。\\
+
+~~また、Java PathFinderはバイトコードによるシミュレーションであり、
+SPINはPROMELA をコンパイルしたCのコードによるシミュレータにより検証を
+行っている。
+CbCによる検証は、他の二つと異なり実際に実行可能なプログラムを直接実行
+することで行われる。そのため、この部分にエラーが入ることはないのがCbCによる
+検証の利点であることが示された。
+
+~~CbCにおける検証では、検証する性質の記述はCbCそのもので行われる。
+タブロー展開と同時に(限られた)時相論理で記述された性質を
+ほとんどオーバヘッドなくチェックすることが可能であることが示された。
+したがって、上記の論文で掲げていた目的を十分に達成していると考えられる。
+%また、SPINとJava PathFinderはシミュレーションによる検証であるが、
+%CbCでは、実際のプログラムを直接実行することによる検証であるため、
+%この部分にエラーが入ることはないのがCbCによる検証の利点であることが示された。\\
+
 %比較の結果から、
 %CbCが実用的であることを示している。
 %次に、