# HG changeset patch
# User atsuki
# Date 1203264924 -32400
# Node ID 0ba2de3295b84a891b4cae9f98a103eeed3e4709
# Parent  39242aece5fc98f162f2fbdb4a3ea0043599831e
*** empty log message ***

diff -r 39242aece5fc -r 0ba2de3295b8 paper/chapter1.tex
--- a/paper/chapter1.tex	Sun Feb 17 14:24:23 2008 +0900
+++ b/paper/chapter1.tex	Mon Feb 18 01:15:24 2008 +0900
@@ -20,9 +20,9 @@
 による実装とその実装に対する検証手法を提案している。
 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
-また、CbCで記述されたプログラムは非決定性状態遷移記述と近い構造になるという性質がある。
+また、CbCで記述されたプログラムは決定性状態遷移記述と近い構造になるという性質がある。
 
-本研究は、CbCが非決定性状態遷移記述と相性の良い言語であることに着目し、
+本研究は、CbCが決定性状態遷移記述と相性の良い言語であることに着目し、
 非決定性状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
 状態を展開する際に、線形時相論理も同時に展開することにより検証を行うことを目的としている。
 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用される。