モデル検査
Definition [Positive Normal Form (release PNF)]For a ∈ AP, LTL formulae in release positive normal form (release PNF, or simply PNF) are given by ϕ ::= true | false | a | ¬a | ϕ ∧ ϕ | ϕ ∨ ϕ | ○ϕ | ϕ U ϕ | ϕ R ϕ
Definition [Positive Normal Form (release PNF)]For a ∈ AP, LTL formulae in release positive normal form (release PNF, or simply PNF) are given by ϕ ::= true | false | a | ¬a | ϕ ∧ ϕ | ϕ ∨ ϕ | ○ϕ | ϕ U ϕ | ϕ R ϕ