risk = nil;

これまでの例で見たように，時相論理により，自然言語に近い形で要求や前提を記述することができることが分かる．一方で，常に自然に記述できるというわけではない．少し複雑な式になると，直感的に意味をとりづらくなる．

対処の方法として，原書では，記述パターン ¹を紹介している．

これは，要求仕様に良く出てくる自然言語表現を，LTL 式や CTL 式に置き換えるためのパターンである．例えば，「先行する」について考える．

常に，「S が P に先行する」のであれば，次の様にパターン化できる（ここでは LTL 式のみを記載する．もとの論文では，よくある時間記述のパターンに対して，CTLと筆者たちが限量正規表現（quantified reqular expression）と呼ぶ方法でも表現している）．

◇ P → (¬P U (S∧¬P))

並びとしては， S, P である．いつかは，P になるが，S になるまでは P は偽でなくてはならない．かつ，Sとなった場合でも，Pは偽でなくてはならない．

一つの置き換えとして妥当であることがわかる．以後もパターンを示すが，特に解説は加えないので，LTLの練習ということで読み取って欲しい．

次は，Rの前では，「S が P に先行する」場合である．

◇R → (¬P U (S  ∨  R))

逆に，Q以後，「S が P に先行する」場合は，次になる．

□¬Q  ∨  ◇ (Q ∧ ◇ (¬P U (S  ∨ □¬P)))

QとRの間で，「S が P に先行する」場合は次になる．

□((Q ∧◇R) → (¬P U (S  ∨  R)))

Q以降，Rまでの間で，「S が P に先行する」場合は，次になる．

□(Q →  ((¬P U (S  ∨  R))  ∨  □¬P))

(nil)