形式仕様記述言語は，何らかの数学的な体系に従って，作られている．このうち，よく使用される形式的仕様記述言語は，（公理的）集合論に基づいているものが多い．原書にある集合論に基づく形式的仕様記述言語の例は，以下である．
Z, VDM, B, Alloy, OCL
実務で使ったことがないとしても，それぞれ名前を聞いたことがあると思う．
集合で考えることの必然性はなく，ただ，そう考えると考えやすい問題があるというだけに過ぎない．例えば，データベース設計をするときのテーブルは，カラムの値からなる集合と考えることができる．
静的表現は集合にできるとして，操作はどうであろうか．出金するという操作は，出金額が，操作前の残高から操作後の残高を引いた額に等しいと考える（場合によっては，手数料分も考慮する）．
組み込みシステムのような反応型（回数に制限なく入力を受け付け出力する）のシステムと違い，トランザクション型のシステムでは，操作の前と後という考えは，なじみやすい．
もう少し考えを進めると，値は何らかの枠にはまっていることが分かる．通常の口座であれば，マイナスになることはないし，小数点を持つことはない．値は自然数と考えて良いことが分かる．
基本は，上記である．次回からは，代表的な Z を用いた原書の例を示すことにする．スキップも考えたが，KAOSの記述を行う上で，必須となる知識なので，まだ，しばらくは亀の歩みとなる．
(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)
ここまでは，線形時間論理（LTL）と呼ばれる時間を線形でモデル化したときの演算子についてであった．分岐で時間をモデル化する場合もある．代表的なものに，CTL（Computation Tree Logic)がある．
時間が分岐するというのは，以前簡単に紹介した様相論理に意味を与える方法である可能世界意味論に基づいている．
CTLではこれまで，使用した様相論理演算子はおおむね次の様に対応する．
○ ： X (neXt)
□ ： G (Global)
◇ ： F (Future)
U, W については基本的には同じ．
但し，これら（パス式演算子）は単独では用いられない．状態式を構成するA（全てのパス）およびE（あるパス）と組み合わせる．前者は全ての分岐したパスで成立する場合，Eは分岐したいずれかのパスで成立する場合である（LTLでは，暗黙的に A が付加されていると考えることもできる）．
従って，分岐型の場合，時相論理演算子は，次の様になる．
AG φ ：全てのパスにおいて，常に φ が成立する．
EF φ ：あるパスにおいて，いつかは φ が成立する．
このLTLとCTLでは，表現能力に一部違いがある．
例えば，上記の EFφ は，LTLでは表現できない．線形であるから当然である．一方で，LTL式の ◇□φ は，CTL式では表現できない．類似の表現：AF AG φ では，必ず φ が成立しなくてはならない．しかし，LTL式では，停止しないシステム（反応型システムの本質的特徴）では，φ が真になることを観察することはない．典型的には，◇□ ABORT を考えれば良い．
この違いが，要求書の記述においては LTL が好まれ，有限時間で結果を出す必要のあるモデル検査においては CTL が好まれる理由となっている ．
(nil)