時相論理には，様々なタイプがある．時間を離散的と捉えるか・連続的と捉えるか．未来のみを扱うか・過去も扱うか．時間の分岐（可能な未来）をモデル化するか否か．
ここでは，要求に関連しそうな基本的なところのみを扱う．また，ここでは，時間軸上の順番のみを問題にする．3msecから 5msecの間といった時間を論理で扱うことは難しい．
ここでは，Manna氏とPnueli氏による教科書 から．
いま，状態の列をσとし，その j 番目が式 φ を満足しているとき，次の様に記述することとする．
(σ, j) ⊧ φ.
「否定」演算子 ¬
(σ, j) ⊧ ¬φ iff (σ, j) ⊭ φ.
j 番目が p でないということは，p であることが正しくない．”iff C” は「もし，C ならば，かつ C の時に限り」という意味である．いわゆる必要十分条件を示す．
「選言」演算子 ∨
(σ, j) ⊧ φ ∨ ψ iff (σ, j) ⊧ φ or (σ, j) ⊧ ψ.
これも問題ないと思う．否定と選言から，∧（連言），→（含意），↔（同等）も導出できる．
↔（equivalence）は始めてかもしれない．次の意味である．A↔B ≡ (A→B) ∧ (B →A)
「次」演算子 ○
ここから，時相論理特有の記号の使い方である．
(σ, j) ⊧ ○ φ iff (σ, j+1) ⊧ φ.
p の次の状態を指す．簡単な例だと次になる．「悲しい」∧ ¬「金銭的に恵まれている」⇒ ○「悲しい」
「⇒」の意味は，後に記述する．
簡単なようで，少し間違えやすい．もう少し複雑な例を考える．(x=0) ∧○(x=1)の真偽がどう変化するかを考えてみる．状態列の番号と x を混同しないように．
「(x=0) ∧○(x=1)」真理値表
| j |
0 |
1 |
2 |
3 |
4 |
5 |
6 |
| x |
0 |
0 |
1 |
1 |
0 |
0 |
1 |
| x = 0 |
T |
T |
F |
F |
T |
T |
F |
| x = 1 |
F |
F |
T |
T |
F |
F |
T |
| ○ (x=1) |
F |
T |
T |
F |
F |
T |
T |
| (x=0) ∧○(x=1) |
F |
T |
F |
F |
F |
T |
F |
横軸が時間の進行を示している．xの値は，適当に与えている．○(x=1) は，x=1 の次の状態であるから，一つ先を見る．x = 1 の真偽を一つ先取りすることになる．
次回は，未来に関する演算子の残りである．
(nil)
要求記述で，様相論理を使うこと場面は少ない．ただ，様相論理の発展形の一つである時相論理が使われるときがある．KAOSは，時相論理を用いる要求分析手法である．
時相論理という言葉は聞かなくても，モデル検証ということばは耳にするかもしれない．ミスリーディングと思うが，ここでのモデルとはふるまいのモデルのみを指す．時相論理は，設計者のものだけではなく，要求分析者が必要とする論理でもある．あるモデルが正しいか否かは，正しいとするプロパティが与えられて始めて確認できる．いくら立派な検証器があっても，プロパティが正しく設定できなければ，何も示していないことになる．アプリケーションに依存したプロパティは，要求定義をおこなう人のみが与えることができる．
時間を気にせずにいえることは少ない．
例えば，「アクセル踏下するならば，踏下量に応じエンジン回転数を上げること」というのは，もちろんエンジンが動作している場合である．OFF状態で，いくら踏下しても，エンジン回転数は増加しない．
これは，単純に前提の問題だともいえる．前提に「エンジンが動作している」をAND結合すれば解決する．しかし，プリクラッシュが作動しているときはどうだろうか．
論理を拡張することによって，時間に関わる問題を解決するというのが，時相論理のねらいの一つである．私はX歳ですという言明は，X歳の時にしか真ではなく，その変化を論理として扱えるようにしようということである．
もともとは，並行プロセスや通信をどう扱うというところから主たる発展があった．ここでは，もう少し要求よりに次回から説明していく．
(nil)
久しぶりにタイトルが変わった．
さて，命題論理は中身は問わずに文の真偽を議論した．述語論理は文の述語を表現することで，表現力が向上した．しかし，それでもいえることは限られている．「人間であれば，いつかは死ぬ」ということばかりを考えているわけではない．
トゥールミンの図式では，最終の結論に至る前に様相限定子というのがでてくる．「必然的に」「明白に」「たぶん」といったものである．日常会話を考えれば分かるが，絶対の真だけを話しているわけではない．なんらかの形で，上記のような括弧付きで話している．推測とその確認が会話の本質であり，かならずなんらかの「様相」を含む．
様相というといかめしいが，英語でモード（mode, modal logic）と呼ばれる．日本語の文法書を見ると，ムードと訳される場合もある．そのままのタイトルの本を見ると，以下のようにある．
ムードは，動詞の示す運動を，話し手が現実と関連づけることに関わる文法的なカテゴリである ．
推量形として，例えば「かれも，これから本をよむだろう．」というのが示されている．この「だろう」は，「本を読む」ということに対する推量となる．
かくのごとく，様相を使わずに話すことは不可能なので，それを論理化したいというのは，自然の欲求である．
そのために，次のような様相演算子が定義された．
□：必然である
◇：可能である
例えば，自然数における通常の演算を認めれば，2×2が４になることは必然であるし，惑星の数が10を超えることは可能である（ ）．
様相演算子を使った規則としては，さまざまなものがある．以下は，その例である．
□φ→φ
φであることが必然であれば，（現在は）φが真である．
□φ→◇φ
φであることが必然であれば，φであることが可能である．
これを違和感なく受け止めるか，規則（正確には，公理）として認めないかで，様々な体系が作られてきた．たった2つの演算子の追加によってである．よく知られているように，可能世界意味論によって，これら様々な体系の意味が与えられたが，未だに議論が収束しているわけではない．
さて，要求文書の多くは規範的な記述が多くを占めるため，様相演算子を必要とする場面は少ないかもしれない．
ただ，別の拡張が必要となることがある．時間軸上のシステム状態変化を記述するためである．
(nil)