Loading article…
コンピュータ科学の一分野であるモデル検査では、線形時間特性を用いてコンピュータシステムのモデルの要件を記述します。特性の例としては、「自動販売機はお金が投入されるまで飲み物を出さない」（安全性特性）や「コンピュータプログラムは最終的に終了する」（活性特性）などがあります。公平性特性は、モデルの非現実的な経路を排除するために使用できます。たとえば、2つの信号機のモデルでは、「両方の信号機が無限に青になる」という活性特性は、「各信号機が無限に色を変える」という無条件の公平性制約の下でのみ真となる可能性があります（一方の信号機が他方よりも「無限に速い」場合を排除するため）。[ 1 ]
形式的には、線形時間特性は「原子命題」の冪集合上のω言語です。つまり、特性は命題の集合のシーケンスを含み、各シーケンスは「単語」と呼ばれます。すべての特性は、ある安全特性Pと活性特性Qに対して「 PとQの両方が発生する」と書き換えることができます。システムの不変条件とは、特定の状態に対して真または偽となるものです。不変特性は、モデルの到達可能なすべての状態が満たさなければならない不変条件を記述し、一方、永続性特性は「最終的に永久に何らかの不変条件が成り立つ」という形式をとります。
線形時相論理などの時相論理は、数式を用いて線形時間特性の種類を記述する。
この記事は命題線形時間特性に関するものであり、プログラムの状態に関する述語を扱うことはできないため、次のような特性を定義することはできません。yの現在の値によって、終了前に x が 0 と 1 の間で切り替わる回数が決まる。安全性と活性特性で使用されるより一般的な形式論では、このような特性を扱うことができます。
AP を原子命題の集合とする。（APの冪集合）は、次のような命題の集合の無限列です。（原子命題の場合）) AP上の線形時間 (LT) 特性は、つまり、単語の集合。[ 2 ]集合に対するLTプロパティの例は「無限回a を含む単語の集合」です。単語wはこの集合に含まれています。なぜならa はに含まれているからです。これは無限に頻繁に出現します。このセットに含まれない単語は、aは(最初のセットで) 1 回しか出現しない。
LT特性とは、アルファベット上のω言語のことである。（そしてその逆もまた然り）。
pref ( w ) はwの有限接頭辞を表します(つまり上記の場合）。LTプロパティPの閉包は次のようになります。
有限状態機械の理論を用いると、プログラムやコンピュータシステムはクリプキ構造でモデル化できる。LT特性は、クリプキ構造のトレース（出力）に対する制約を記述する。例えば、交差点にある2つの信号機がクリプキ構造で表される場合、原子命題は各信号機の可能な色であり、トレースが「信号機は両方とも同時に青にならない」というLT特性を満たすことが望ましい（車の衝突を避けるため）。[ 3 ]
クリプキ構造TSのすべてのトレースがTS 'のトレースである場合、 TS 'が満たすすべてのLTプロパティはTSによって満たされます。これは、モデル検査において抽象化を可能にするのに役立ちます。システムの単純化されたモデルがLTプロパティを満たす場合、システムの実際のモデルもそれを満たします。[ 4 ]
安全特性は非公式には「悪いことは起こらない」という形をとります。[ 5 ]例えば、システムが自動預け払い機（ATM）をモデル化する場合、そのような特性は「PINが入力されない限りお金は払い出されない」です。[ 6 ]正式には、安全特性はLT特性であり、その特性に違反する単語には「悪い接頭辞」があり、その接頭辞を持つ単語ではその特性を満たしません。つまり、[ 7 ]
ATMの例では、最小限の不正なプレフィックスとは、最後のステップで現金が払い出され、どのステップでもPINが入力されない有限のステップの集合です。安全性を検証するには、クリプキ構造の有限のトレースのみを考慮し、そのようなトレースのいずれかが不正なプレフィックスであるかどうかをチェックするだけで十分です。[ 8 ]
LTプロパティPが安全プロパティであるのは、以下の条件を満たす場合に限る。[ 9 ]
不変条件とは、現在の状態のみを参照する安全条件の一種です。[ 10 ]例えば、ATM の例は不変条件ではありません。現在の状態が「お金を出す」であること、そして以前の状態が「PIN を読み取る」でなかったことだけを見て、その条件が破られているかどうかを判断できるからです。不変条件の例としては、上記の信号機の条件「信号機が両方とも同時に青になることはない」があります。また、コンピュータ プログラムのモデルにおける「変数xは決して負にならない」も不変条件の例です。
形式的には、不変量は次の形式をとります。
クリプキ構造が不変条件を満たすのは、到達可能なすべての状態が不変条件を満たす場合のみであり、これは幅優先探索または深さ優先探索によって確認できます。[ 11 ]安全性の特性は、不変条件を使用して帰納的に検証できます。[ 12 ]
活性特性は非公式には「最終的に何か良いことが起こる」という形をとる。[ 5 ]正式には、Pが活性特性であるのは、つまり、任意の有限文字列は有効なトレースに継続できる。[ 13 ] [ 7 ]活性特性の一例として、前述のLT特性「無限回含まれる単語の集合」がある。単語の有限接頭辞では、その単語がこの特性を満たさないことを証明することはできない。なぜなら、その単語は無限に多くのsを持つように継続できるからである。
コンピュータプログラムに関して言えば、有用な活性特性には「プログラムは最終的に終了する」こと、そして並行コンピューティングにおいては「すべてのプロセスは最終的に処理されなければならない」ことが含まれる。[ 14 ]
永続性プロパティは、「最終的に永久に」という形式の生存性プロパティです。つまり、次の形式の性質です。[ 15 ]
LTプロパティ以外（すべての単語の集合））は安全性と活性の両方の性質を持つ。[ 16 ]すべての性質が安全性または活性の性質であるわけではないが（「aがちょうど1回発生する」を考えてみよう）、すべての性質は安全性と活性の性質の交差である。[ 5 ]
位相幾何学において、すべての単語の集合メトリックを装備できます:
公平性の特性は、非現実的なトレースを排除するためにシステムに課される前提条件です。 [ 18 ] [ 19 ]無条件の公平性は、「すべてのプロセスが無限に順番を得る」という形式です。強い公平性は、「すべてのプロセスが無限に有効にされている場合、無限に順番を得る」という形式です。弱い公平性は、「すべてのプロセスが特定の時点から継続的に有効にされている場合、無限に順番を得る」という形式です。[ 20 ]
一部のシステムでは、公平性制約は状態の集合によって定義され、「公平なパス」とは、公平性制約内のいずれかの状態を無限回通過するパスのことです。公平性制約が複数ある場合、公平なパスは制約ごとに 1 つの状態を無限回通過する必要があります。[ 21 ]プログラムは、すべてのパスについて、公平性条件を満たさないか、またはPを満たす場合、公平性条件の集合に関してLT 特性Pを「公平に満たす」ことになります。つまり、すべての公平なパスについて特性Pが満たされます。 [ 22 ]
クリプキ構造において公平性特性が実現可能であるとは、到達可能なすべての状態から始まる公平な経路が存在する場合をいう。公平性条件の集合が実現可能である限り、それらは安全性特性とは無関係である。[ 23 ]
計算木論理(CTL)などの時間論理は、いくつかの LT 特性を指定するために使用できます。[ 24 ]すべての線形時間論理(LTL) 式は LT 特性です。数え上げの議論により、各式が有限文字列である論理では、すべての LT 特性を表すことはできないことがわかります。なぜなら、式の数は可算個でなければなりませんが、LT 特性は非可算個あるからです。
