--- a/paper/chapter/01-introduction.tex	Tue Feb 16 14:33:25 2021 +0900
+++ b/paper/chapter/01-introduction.tex	Tue Feb 16 14:52:49 2021 +0900
@@ -45,7 +45,7 @@
 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
 範囲が限られているため、有限時間でモデル検査などで検証することが可能である。
-この為にはOSの処理を証明しやすくする表現で実装する必要がある。\cite{hyperkernel}
+この為にはOSの処理を証明しやすくする表現で実装する必要がある\cite{hyperkernel}。
 証明しやすい表現の例として、 状態遷移ベースでの実装がある。
 
 
@@ -102,4 +102,4 @@
 これらのメタレベルの計算はコンパイル時に決定するために、自動化を行いたい。
 
 本研究ではGearsOSの信頼性と拡張性の保証につながる、メタ計算に関するAPIについて考察する。
-GearsOSがメタ計算を自動生成しているPerlトランスパイラで従来のGearsOSのシステムよりさらに拡張性の充実と、信頼性の保証を図る。
\ No newline at end of file
+GearsOSがメタ計算を自動生成しているPerlトランスパイラで従来のGearsOSのシステムよりさらに拡張性の充実と、信頼性の保証を図る。