Proving What's Possible

形式手法コンサルタントとして、システムの特性を数学的に表現する際に使用する「常に真」(A)と「最終的に真」(E)という2つの時間演算子に加えて、第三のクラスとして「可能性」(P)特性を紹介。P(x)は「モデル内でxが発生し得るか」を表し、仕様の妥当性チェックなどに有用だが、AlloyやTLA+などの主要形式手法ではネイティブサポートされていない。