risk = 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)