model-checking - LTL フォーミュラのサイズは?

Question

LTL 数式のサイズ |p| は一般的に、複雑さに関して何を意味しますか? 原子命題の数、深さ、または何か？

前もって感謝します！！

Answer 1

複雑さという点では、式で使用されるXおよびU演算子の数を数えることは理にかなっています。F、G、R、Wなどの演算子は、 Uを使用するシンタックス シュガーと見なすことができることに注意してください( LTL の構文を参照)。

正当化: システムをモデル チェックするときは、システムの各状態について考えられる未来をそれぞれ考慮する必要があります。したがって、 X ... または ... U ...の形式の部分式が true または false である可能性があることを考慮する必要があります。したがって、各状態には 2^n の可能性があります。ここで、n はXおよびU演算子の数です。

より正確には、リキテンシュタインとプニューリのアルゴリズムなどを使用して式を検証する場合、s を状態数として、サイズ <= s*2^n のグラフで強連結成分 (SCC) を検索します。

LTL 構文で過去の演算子も使用できる場合は、演算子YとSを同様に追加できます。