線形時間特性

コンピュータサイエンスの一分野であるモデル検査では、線形時間特性はコンピュータシステムのモデルの要件を記述するために使用される。特性の例には、「自動販売機はお金が投入されるまで飲み物を出さない」（安全性特性）や「コンピュータプログラムは最終的に終了する」（活性特性）などがある。公平性特性は、モデルの非現実的なパスを除外するために使用できる。たとえば、2つの信号機のモデルでは、「両方の信号機が無限に頻繁に青になる」という活性特性は、「各信号機が無限に頻繁に色を変える」という無条件公平性制約の下でのみ真である可能性がある（一方の信号機が他方より「無限に速い」場合を除外するため）。^[1]

形式的には、線形時間プロパティは「原子命題」のべき集合上のω 言語です。つまり、プロパティには命題集合のシーケンスが含まれており、各シーケンスは「単語」と呼ばれます。すべてのプロパティは、何らかの安全性プロパティPと活性プロパティQに対して「 PとQ の両方が発生する」と書き直すことができます。システムの不変条件とは、特定の状態に対して真または偽であるものです。不変プロパティは、モデルの到達可能なすべての状態が満たす必要がある不変条件を記述しますが、永続性プロパティは「最終的には何らかの不変条件が永遠に保持される」という形式です。

線形時相論理などの時相論理は、式を使用して線形時間プロパティの種類を記述します。

この記事は命題的線形時間プロパティに関するもので、プログラム状態に関する述語を扱うことができないため、次のようなプロパティを定義することはできません: y の現在の値によって、終了前に x が 0 と 1 の間を切り替えた回数が決まります。安全性と活性プロパティで使用されるより一般的な形式論では、これを処理できます。

AP を原子命題の集合とする。 ( APの冪集合) 上の単語は、 (原子命題 に対して)のような、命題集合の無限列である。AP 上の線形時間 (LT) プロパティはのサブセット、すなわち単語の集合である。^[2]集合上の LT プロパティの例は、「 a を無限に含む単語の集合」である。単語wはこの集合に含まれる。なぜなら、a はに含まれ、これは無限に出現する。この集合に含まれない単語は であり、a は(最初の集合では) 1 回しか出現しない。 ${\displaystyle 2^{AP}}$${\displaystyle w:=\{a\}\{a,b\}\emptyset \{a,b\}^{\omega }}$${\displaystyle AP=\{a,b\}}$${\displaystyle (2^{AP})^{\オメガ }}$${\displaystyle \{a,b\}}$${\displaystyle \{a,b\}}$${\displaystyle x:=\{a\}(\{b\}\emptyset )^{\omega }}$

LT プロパティはアルファベット上のω 言語です(逆も同様です)。 ${\displaystyle \Sigma =2^{AP}}$

wの有限接頭辞をpref ( w )で表します(つまり、上記の場合)。LT プロパティPの閉包は次のようになります。 ${\displaystyle \{\{a\},\{a\}\{a,b\},\{a\}\{a,b\}\emptyset ,...\}}$

${\displaystyle {\mathit {closure}}(P):=\{\sigma \in (2^{AP})^{\omega }\mid {\mathit {pref}}(\sigma )\subseteq {\mathit {pref}}(P)\}}$

有限状態機械の理論を使用すると、プログラムまたはコンピュータ システムをクリプキ構造でモデル化できます。LT プロパティは、クリプキ構造のトレース (出力) に対する制約を記述します。たとえば、交差点の 2 つの信号がクリプキ構造で表されている場合、原子命題は各信号の可能な色であり、トレースが LT プロパティ「信号が同時に両方青になることはない」を満たすことが望ましい場合があります (車の衝突を避けるため)。^[3]

クリプキ構造TSのすべてのトレースがTS 'のトレースである場合、 TS 'が満たすすべてのLTプロパティはTSによって満たされます。これは抽象化を可能にするモデル検査に役立ちます。システムの簡略化されたモデルがLTプロパティを満たす場合、システムの実際のモデルもそれを満たすことになります。^[4]

安全性プロパティは、非公式には「悪いことは起こらない」という形をとる。^[5]たとえば、システムが自動現金預け払い機(ATM) をモデル化する場合、そのようなプロパティは「PIN が入力されない限り、お金は払い出されない」というものである。^[6]正式には、安全性プロパティは LT プロパティであり、そのプロパティに違反する単語は「悪い接頭辞」を持ち、その接頭辞を持つ単語はプロパティを満たさない。つまり、^[7]

${\displaystyle \forall \sigma \in (2^{AP})^{\omega }\setminus P\ \exists {\text{ 有限の接頭辞}}\ {\hat {\sigma }}:P\cap \{\sigma '\mid {\hat {\sigma }}\ {\text{ の接頭辞}}\ \sigma '\}=\emptyset }$

ATMの例では、最小の悪いプレフィックスとは、最後のステップでお金が払い出され、どのステップでもPINが入力されない、実行される有限のステップセットです。安全性を検証するには、クリプキ構造の有限のトレースのみを考慮し、そのようなトレースが悪いプレフィックスであるかどうかを確認するだけで十分です。^[8]

LTプロパティPが安全プロパティである場合、かつその場合のみ。^[9]${\displaystyle {\mathit {閉包}}(P)=P}$

不変プロパティは、条件が現在の状態のみを参照するタイプの安全性プロパティです。^[10]たとえば、ATM の例は不変ではありません。現在の状態が「お金を出す」であることを見ても、プロパティに違反しているかどうかはわかりません。現在の状態が「お金を出す」であり、以前の状態が「PIN を読み取る」ではなかったことだけを見ても、プロパティに違反しているかどうかはわかりません。不変の例としては、上記の信号機の条件「信号機が同時に両方青になることはない」があります。別の例としては、コンピュータ プログラムのモデルにおける 「変数xが負になることはない」があります。

正式には、不変式は次の形式になります。

${\displaystyle P=\{A_{0}A_{1}....\in (2^{AP})^{\omega }\mid \forall j\in \mathbb {N} :A_{j}\ {\text{satisfies}}\ \Phi \}}$

ある命題論理式の場合。^[10]${\displaystyle \Phi }$

クリプキ構造は、すべての到達可能な状態が不変条件を満たす場合にのみ不変条件を満たし、これは幅優先探索または深さ優先探索によって確認できます。^[11]安全性は不変条件を使用して帰納的に検証できます。^[12]

活性特性は非公式には「結局何か良いことが起こる」という形をとる。^[5]正式には、P は、つまり任意の有限文字列が有効なトレースまで継続できる場合、活性特性である。 ^{[13] [7]活性特性の例としては、前述の LT 特性「無限に}a を含む単語の集合」がある。単語の有限接頭辞は、単語がこの特性を満たさないことを証明できない。なぜなら、単語は無限にaを持ち続けることができるからである。 ${\displaystyle {\mathit {pref}}(P)=(2^{AP})^{*}}$

コンピュータプログラムの観点から見ると、有用な活性特性には「プログラムは最終的に終了する」ことや、並行コンピューティングにおいては「すべてのプロセスは最終的に処理されなければならない」ことなどがある。^[14]

永続性プロパティは、「最終的には永遠に」という形式の生存性プロパティです。つまり、次の形式の性質です。^[15]${\displaystyle \Phi }$

${\displaystyle P=\{A_{0}A_{1}...\in (2^{AP})^{\omega }\mid \exists N\in \mathbb {N} :\forall n\geq N:A_{n}\ {\text{satisfies}}\ \Phi \}}$

（ 上のすべての単語の集合）以外のLTプロパティは、安全性と活性の両方の特性を持ちません。^{[16]すべてのプロパティが安全性または活性の特性であるわけではありませんが（「}は正確に1回発生する」を考えてみましょう）、すべてのプロパティは安全性と活性の特性の共通部分です。^[5]${\displaystyle (2^{AP})^{\omega }}$${\displaystyle 2^{AP}}$

位相幾何学では、すべての単語の集合にメトリックを備えることができます。 ${\displaystyle (2^{AP})^{\omega }}$

${\displaystyle d(w,x):=\inf\{2^{-|s|}\mid s\in {\mathit {pref}}(w)\cap {\mathit {pref}}(x)\}}$

すると安全性は閉集合となり、活性性は稠密集合となる。^[17]

公平性の特性は、非現実的なトレースを排除するためにシステムに課せられる前提条件です。 ^{[18] [19]}無条件の公平性は、「すべてのプロセスは無限に頻繁に順番が回ってくる」という形式です。強い公平性は、「すべてのプロセスは、無限に頻繁に有効化されれば、無限に頻繁に順番が回ってくる」という形式です。弱い公平性は、「すべてのプロセスは、特定の時点から継続的に有効化されれば、無限に頻繁に順番が回ってくる」という形式です。^[20]

いくつかのシステムでは、公平性制約は状態の集合によって定義され、「公平なパス」とは、公平性制約内のいずれかの状態を無限に通過するパスのことである。複数の公平性制約がある場合、公平なパスは、制約ごとに 1 つの状態を無限に通過する必要がある。^[21]プログラムは、すべてのパスについて、パスが公平性条件に違反するか、パスがP を満たす場合、公平性条件の集合に関してLT プロパティPを「公平に満たす」 。つまり、プロパティP はすべての公平なパスで満たされる。^[22]

クリプキ構造において公平性は、すべての到達可能な状態がその状態から始まる公平な経路を持つ場合に実現可能である。公平性条件の集合が実現可能である限り、それらは安全性とは無関係である。^[23]

計算木論理（CTL）などの時相論理は、いくつかのLTプロパティを指定するために使用できます。^[24]すべての線形時相論理（LTL）式はLTプロパティです。計数議論により、各式が有限文字列である論理は、すべてのLTプロパティを表すことができないことがわかります。これは、式は可算数個あるはずですが、LTプロパティは不可算数個あるためです。

• Alpern, B.; Schneider, FB (1987). 「安全性と活性の認識」.分散コンピューティング. 2 (3): 117. CiteSeerX  10.1.1.20.5470 . doi :10.1007/BF01782772. S2CID  9717112.
• クリステル・バイアー;加藤園、ヨースト・ピーター(2008)。モデル検査の原則。 MITプレス。ISBN 9780262026499。
• Clarke, Edmund M. ; Grumberg, Orna ; Kroening, Daniel (2018).モデル検査。MIT プレス。ISBN 9780262038836。
• D'Silva, Vijay; Kroening, Daniel ; Weissenbacher, Georg (2008). 「形式的ソフトウェア検証のための自動化技術の調査」。IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems . 27 (7): 1165–1178. doi :10.1109/TCAD.2008.923410. S2CID  8921624.
• Finkbeiner, Bernd; Torfah, Hazem (2017)。「線形時間特性の密度」。コンピュータサイエンスの講義ノート。検証と分析のための自動化技術。第 10482 巻。Springer。
• Kern, Christoph; Greenstreet, Mark R. (1999). 「ハードウェア設計における形式検証: 概観」。ACM Transactions on Design Automation of Electronic Systems . 4 (2). Association for Computing Machinery. doi :10.1145/307988.307989. ISSN  1084-4309. S2CID  13994730.

• エマーソン、E. アレン(1990)。「時間的および様相的論理」。理論計算機科学ハンドブック。B 。
• Pnueli, Amir (1986)。「リアクティブ システムの仕様と検証への時相論理の応用: 現在の傾向の調査」。JW Bakker、W.-P. Roever、G. Rozenberg (編)。同時実行の現在の傾向。コンピュータ サイエンスの講義ノート。第 224 巻。Springer。pp. 510–584。doi : 10.1007/ BFb0027047。ISBN 978-3-540-16488-3。