SPIN にはNext-0Step 演算子 (X) はない？
SPIN では，Next Step Operator (X) は使えないらしい．以下はそのSPIN開発者らによる言及．
Spin Run-Time Optionsによれば，
Spin Run-Time Optionsによれば，SPINには，Next Step Operator (X) がないらしい．なんでも， partial order reduction と互換性を保つためであるとか．原文では以下の通り：
The LTL operators are written: [] (always), <> (eventually), and U (strong until). There is no X (next) operator, to secure compatibility with the partial order reduction rules that are applied during the verification process.
The spin model checker: primer and reference manual によれば
The spin model checker: primer and reference manual P.515
In the syntax that SPIN accepts for the specification LTL formulae, the standard LTL operator "next", written X, is not allowed. The restriction secures that all LTL properties that can not be expressed are necessarily compatible with SPIN's partial order reduction strategy. Technically, it means that the behaviour expressed by these formulae is stutter invariant. Quite apart from this desirable closure property, one can also make a strong distributed system execution preclude the use of the next operator. (There is no real notion of a unique next step in a concurrent system.) The conversion algorithm for LTL forumlae, though, can easily handle the next operator if the above concerns are not application. Furthermore, it is also possible to write LTL formulae that do include the next operator and that are still stutter invariant, but this is generally hard to determine.
つまり，SPIN の LTL 式が標準の LTL がもつ Next 演算子を持たない理由は以下の二つ：
- SPIN'sの半順序簡約（partial order reduction）と互換性を保証するため
- （並行システムにおいては唯一の次ステップという真の概念が存在しないため，）分散システムの実行は，Next 演算子の使用を排除する．
ちなみに，この2つ目の理由は個人的にはよくわからなかった．確かに並行システムのインタリービングな意味モデルでは次ステップとしてくるものは，非決定的に決まり，真の次ステップと言うものはないのだが，「次ステップでおきる可能性」という意味では，Next 演算子の使用は有効だと思うが．そもそもモデル検査ってそういうものだったのでは？
→ LTL の Kripke モデルによる解釈では，全てのパスでというのが定義として定められている．つまり，Next-Step 演算子でも，全ての次ステップでPが成り立つと言う意味理解になってしまうため，インタリービングモデルでは意味を成さなくなってしまう．（なぜなら，上述の通りインタリービングモデルでは次ステップは非決定的に決まるため）
SPIN のLTL構文
NAME
LTL - linear-time temporal logic formulae, for specifying correctness requirements.SYNTAX
Grammar:
ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
Unary Operators (unop):
[] (the temporal operator always),
<> (the temporal operator eventually),
! (the boolean operator for negation)
Binary Operators (binop):
U (the temporal operator strong until)
V (the dual of U): (p V q) == !(!p U !q)
&& (the boolean operator for logical and)
|| (the boolean operator for logical or)
-> (the boolean operator for logical implication)
<-> (the boolean operator for logical equivalence)
Operands (opd):
Predefined: true, false
User-defined: names starting with a lowercase letter.
疑問
- stutter invaritant ってなんだろう？？→あとで調べる
- NuSMV のLTL構文にはNext-step 演算子（X）があったが，あれはどういう理解になっているんだろう？
