線形時間特性

コンピュータサイエンスの一分野であるモデル検査では、線形時間特性を用いてコンピュータシステムのモデルの要件を記述する。例えば、「自動販売機はお金が投入されるまで飲み物を出さない」（安全性特性）や「コンピュータプログラムは最終的に終了する」（活性特性）といった特性がある。公平性特性は、モデルの非現実的な経路を除外するために用いることができる。例えば、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特性「 q は無限に頻繁に発生する」は満たさない。すべての可能な経路がまたは に無限に頻繁に入るため、 「 pは無限に頻繁に発生する」は満たす。${\displaystyle \{p,q\}}$ ${\displaystyle s_{1}s_{2}s_{3}^{\omega}}$ ${\displaystyle s_{1}}$ ${\displaystyle s_{3}}$

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

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

線形時間特性の分類

安全性

安全性プロパティは、非公式には「悪いことは起こらない」という形をとる。^{[ 5 ]}例えば、システムが自動現金預け払い機（ATM）をモデル化している場合、そのようなプロパティは「暗証番号が入力されない限り、お金は払い出されるべきではない」となる。^{[ 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{を満たす}}\ \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})^{\オメガ }}$ ${\displaystyle 2^{AP}}$

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

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

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

公平性の特性

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

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

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

時相論理

計算木論理（CTL）などの時相論理は、いくつかの線形時相論理特性を指定するために用いることができる。 ^{[ 24 ]}すべての線形時相論理（LTL）式はLT特性である。計数論的議論によれば、各式が有限の文字列である論理は、すべてのLT特性を表現することはできない。なぜなら、式は可算数個存在するはずであるが、LT特性は非可算数個存在するからである。

注記

1. バイエル＆カトーエン (2008)、p. 126.
2. Baier & Kataen (2008)、97–98 ページ。
3. Baier & Kataen (2008)、97–99 ページ。
4. バイエル＆カトーエン (2008)、p. 102.
5. アルパーン&シュナイダー (1987)。
6. バイエル＆カトーエン (2008)、p. 109.
7. フィンクバイナー & トルファ (2017)、p. 4.
8. Baier & Kataen (2008)、p. 112.
9. バイエル＆カトーエン (2008)、p. 113.
10. Baier & Kataen (2008)、p. 105.
11. Baier & Kataen (2008)、105–106 ページ。
12. カーン＆グリーンストリート（1999）、135ページ。
13. バイエル＆カトーエン (2008)、p. 119.
14. D'Silva、Kroening、Weissenbacher（2008）、5ページ。
15. バイエル＆カトーエン (2008)、p. 197.
16. バイエル＆カトーエン (2008)、p. 121.
17. Baier & Kataen (2008)、123–124 ページ。
18. バイエル＆カトーエン (2008)、p. 124.
19. カーン＆グリーンストリート（1999）、131-132頁。
20. Baier & Kataen (2008)、126–127 ページ。
21. Clarke、Grumberg、Kroening（2018）、32～33ページ。
22. Baier & Kataen (2008)、p. 132.
23. Baier & Kataen (2008)、137–139 ページ。
24. カーン＆グリーンストリート（1999）、127ページ。

参考文献

• Alpern, B.; Schneider, FB (1987). 「安全性と活性の認識」.分散コンピューティング. 2 (3): 117. CiteSeerX  10.1.1.20.5470 . doi : 10.1007/BF01782772 . S2CID  9717112 .
• クリステル・バイアー;かとえん、ヨースト・ピーター(2008)。モデル検査の原則。 MITプレス。ISBN 9780262026499。
• クラーク、エドマンド・M、グルンバーグ、オルナ、クローニング、ダニエル(2018).モデル検査. MIT Press. 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。