安全性-活性分解定理とその関連研究 - チェシャ猫の消滅定理

こんにちは、チェシャ猫です。先日行われた第 7 回 Web System Architecture 研究会で形式手法について発表してきました。

普段、形式手法について登壇する際は具体例な検証例を出すことが多いですが、今回は理論側に寄せたサーベイになっています。

はじめに

本セッションでは、安全性-活性分解 (safety-liveness decomposition) と呼ばれる一連の結果について解説する。安全性-活性分解は、システムの仕様が与えられた時、それを安全性 (safety) および活性 (liveness) と呼ばれる、よりシンプルな特徴付けを持つクラスに分解して扱うための方法論である。さらにセッションの後半では、安全性と活性の組み合わせ以外にも提案されている派生的な特徴付けについても述べる。

Web アプリケーションと形式手法

システムやプログラムの性質を何らかの数学的な対象を通して表現、検証する方法論を形式手法 (formal methods) と呼ぶ。

期待される入力と出力を人間が具体的に与える従来のテストと比較し、形式手法では理論的な背景に基づいた抜けや漏れのない検証が可能であり、また並行性のようなコントロールが困難な性質についても網羅的な検証を行うことができる。また、実装に依存せず設計段階でその意図を表現・検証できるというメリットもある。一方、形式手法を扱えるプログラマは多くなく、また一般には記述コストが通常のテストに比べて高くなるというデメリットも存在する。

伝統的には形式手法は、例えば航空宇宙関連の組み込みプログラムのような、高コストを支払ってでもそれを上回る信頼性が必要となる分野で用いられてきた。しかし近年では分散システムが身近になったことに起因し、Web アプリケーション開発において形式手法が採用される事例も見られる。一例としてここでは Amazon Web Service による S3 および DynamoDB のレプリケーションを検証した事例 [CRZ15]、および CockroachDB の分散トランザクションの最適化を検証した事例 [TSM20] を挙げておく。

安全性と活性

システムやプログラムの仕様を表現するにあたって、安全性と活性の二種類の仕様があることは古くから経験的に知られてきた。非形式的な表現で述べるなら、安全性とは「何か悪いことが決して起こらない性質」であり、活性とは「何か良いことがいつかは起こる性質」である。

シンプルな例として排他制御を考える。二つのプロセスが並行して動作し、各々が実行中にクリティカルセクションに入る必要があるとする。直感的にイメージされる性質は「二つのプロセスが同時にクリティカルセクションに入ることがない」であり、これは安全性に属する性質である。

しかし実はこの記述には不足があり、システムとして要求される性質を完全には表現していない。各プロセスが一度もクリティカルセッションに入らないようなシステムであってもこの安全性を満たすからである。したがって「各プロセスが実行中にいずれクリティカルプロセスに入る」という条件が必要であり、これが活性に相当する。

このことからもわかる通り、システムに要求される性質を記述する上では、安全性だけでなく活性を与えることが本質的に必要である。

分解定理

システムを検証するに当たって、前提としてその動作や期待する性質を何らかの形で記述する必要がある。停止するプログラムであれば入力-出力の関係としてその性質を記述することも考えられるが、システムサーバのような動き続けるシステムを記述するにはこの形式は不向きである。

このような場合、システムの状態を要素とする無限列を考えることが一般的である。例えば、システムに関与する各プロセスのプログラムカウンタの位置と各変数に代入された値の組はそのシステムの状態とみなすことができる。状態の無限列をパス (path) あるいは振る舞い (behaviour)と呼び、パス全体がなす集合の部分集合を性質 (property) と呼ぶ。

ここで、パスの定義は「実際にそのシステムが動作中に実現しうるもの」に限られない点に注意されたい。最終的な目標となる「システムが要求された性質を満たすことの検証」とはすなわち、「パスのうちシステムが実現しうるもの集合が要求したい性質の集合に含まれていること」に他ならない。

二つのパスに対して「最初 n 個目までの状態までが一致する」という関係はパス間の距離を定義する。したがって、パス全体の集合に対して、この距離が誘導する位相構造を考えることができる。

Alpern と Schneider [AS85] はこの位相構造を用いて、安全性と活性にエレガントな定義を与えている。特に活性については、これが最初の理論的な定義である。

定義：閉な部分集合を安全性 (safety property)、稠密な部分集合を活性 (liveness property) と呼ぶ

非形式的な表現に直すなら、安全性とは「要求に違反する無限列があったとしたら最初の有限個の状態ですでに違反している」性質であり、活性とは「最初の有限個がどんな状態であっても、その後続をうまく取れば全体としては要求を満たすことができる」性質である。これは前項で述べた安全性および活性の直感的な理解とよく一致する。

ところで、一般に位相空間において、任意の集合は閉集合と稠密集合の共通部分として表現することができる。このことから以下の定理が従うことがわかる [AS85]。

定理：任意の性質 $P$ に対して、安全性 $S$ と活性 $L$ が存在して $P = S \cap L$

言い換えれば、システムに要求される任意の性質は、安全性に属する部分と活性に属する部分に分解できることがわかる。この定理は分解定理あるいは Alpern-Schneider 型定理と呼ばれ、以降に述べるような様々な派生的な研究のきっかけとなっている。

f:id:y_taka_23:20201114205820p:plain — 安全性-活性分解の直感的証明

サブクラスに対する分解

上に示した分解定理は、任意の性質 $P$ に対して成立するという意味では適用範囲が広いが、具体的に性質を記述したり判定を行ったりする目的には向かない。実用上はより具体的な記述の形式や分解の手続きが必要である。さらに、分解した結果を効率的に運用するためには、あるクラスに属する性質を分解した結果もそのクラスに閉じていること望ましい。ここでは知られている例として、Büchi オートマトンに対する結果および線形時相論理式に対する結果を取り上げる。

Büchi オートマトンに対する分解

Büchi オートマトンは有限状態オートマトンのある意味での拡張である。有限状態オートマトンが正規言語に対応するように、Büchi オートマトンは ω-正則言語と呼ばれる記号列のクラスに対応する。有限状態オートマトンを用いて記号の有限列が条件にマッチするかどうかを定義できるのと同様、Büchi オートマトンは与えられた記号の無限列が条件にマッチするかどうかを定義する。

非形式的な表現で述べれば、有限の記号列がある有限状態オートマトンに受理されるとは、記号に応じてオートマトンの遷移を辿っていった際、最終状態が受理状態であることを指す。これに対して無限の記号列がある Büchi オートマトンに受理されるとは、記号に応じてオートマトンの遷移を辿っていった際、受理状態を無限回通過することを指す。

今、考えているシステムのパスとは状態の無限列のことであり、システムの性質とはパス全体がなす集合の部分集合であった。つまり記号の集合として状態の集合を考えると、Büchi オートマトン $m$ に対して $m$ が受理するパスの集合 $L(m)$ が定まり、これは何らかの性質を定義しているとみなすことができる。

Alpern と Schneider は先ほどの抽象的な分解に加えて、与えられた Büchi オートマトン $m$ から二つの Büchi オートマトン $Safe(m)$ と $Live(m)$ を構成する手続きを示した [AS87]。

定理：任意の既約 Büchi オートマトン $m$ に対して、 $L(Safe(m))$ および $L(Live(m))$ はそれぞれ安全性と活性となる。さらに $L(m) = L(Safe(m)) \cap L(Live(m))$ が成り立つ

この定理は先に述べた位相を利用して得られる定理と同様、性質を安全性と活性とに分解する記述を与えている。ただしその分解の対象は性質の中でも特に Büchi オートマトンにより定義できるものに限られ、その代わり分解のための具体的な手続きを提供する。

線形時相論理式に対する分解

線形時相論理 (linear temporal logic, LTL) は、時相論理と呼ばれる時間的な広がりを持った条件を記述することができる諸体系の一部である。時相論理には複数のクラスがあり、LTL の他にも計算木論理 (computational tree logic, CTL) や、LTL と CTL の両者を内包する CTL* などの体系が知られている。木構造の分岐を扱うことができる CTL に対して、時間発展を直線的なモデル、すなわち状態列として扱うのが LTL の特徴である。

一般に時相論理おける論理式は、単一の状態に対する通常の命題論理に時相論理用の演算子を追加して記述される。どの記号がどの位置に出現することを許すかによって時相論理の中でも上記のバリエーションが生まれるが、LTL として妥当な演算子とその非形式的な意味は以下の二つである。

$\bigcirc \phi$ ：次の状態で $\phi$ が成立する

$\phi \mathbf{U} \psi$ ：今後いつかは $\psi$ が成立し、かつそれまでの間は $\phi$ が成立する

実用上の文脈では、これらの演算子を用いてさらに定義される

$\Diamond \phi = true \mathbf{U} \phi$

$\Box \phi = \neg \Diamond \neg \phi$

が使用されることが多い。非形式的には $\Diamond \phi$ は「今後、いつかは $\phi$ が成立する」、 $\Box \phi$ は「今後、常に $\phi$ が成立する」といったような意味になる。

LTL 論理式は無限列に対してその真偽が判定できるため、やはり何らかの性質を表現しているとみなすことができる。Maretić らはこの LTL で表される性質のクラスに対する結果として以下を示した [MDB14]。前述の Büchi オートマトンに関する結果と同じく、与えられた性質を安全性と活性に分解する形式になっている。

定理：任意の LTL 論理式 $\phi$ に対して、安全性を表現する LTL 論理式 $\sigma$ と活性を表現する LTL 論理式 $\lambda$ が存在して $\phi = \sigma \land \lambda$

なお、LTL 論理式で表現できる性質は Büchi オートマトンでも表現できるが、逆は成り立たない。LTL 論理式の表現力は Büchi オートマトンの中でも特に counter-free と呼ばれるクラスに属しているものに等しく [DG08]、これは Büchi オートマトン全体より真に狭い [W83]。つまり LTL 論理式に対する上記の定理は、LTL 論理式が分解について閉じていることを意味している。

性質に対する分類の拡張

ここまでに述べてきた結果は、対象とする性質のクラスに差はあるが、いずれも Alpern-Schneider により定式化された安全性と活性という分類に基づいたものであった。やや方向性が異なる研究として、従来とは異なる新たな分類手法を提案した文献を二つ取り上げる。

束論を用いた特徴付け

束 $\langle L, \leq \rangle$ に対して、以下の条件を満たす作用素 $cl: L \rightarrow L$ を閉包作用素と呼ぶ。

$a \leq cl(a)$
$cl(a) = cl(cl(a))$
$a \leq b$ ならば $cl(a) \leq cl(b)$

ある集合が与えられた時、その部分集合の全体に包含関係で順序を入れたものは束になり、位相の意味での閉包を取る操作は閉包作用素の条件を満たす。このため、位相を用いて定義された安全性と活性の概念は、束を用いて再定義することができる。

Manolios と Trefler はこの着想に基づき、束上で定義される安全性と活性の類似物について論じている [MR03]。具体的には以下のような定義である。

定義：可補モジュラー束 $\langle L, \land, \lor, 0, 1 \rangle$ 上の閉包演算子 $cl: L \rightarrow L$ が与えられたとする。 $a = cl(a)$ を満たすような元 $a$ を $cl$ -安全性 ( $cl$ -safety)、 $cl(a) = 1$ を満たすような元 $a$ を $cl$ -活性 (cl-live) と呼ぶ

$cl$ として位相的な閉包を取る操作を考えると、これらの定義は先に挙げたものの一般化になっている。さらにこの方針の面白い性質は、分解された各部分を特徴づける際に共通の $cl$ を用いる必要がないという事実である。以下の定理からわかるように、特定の条件下さえ満たされれば、安全性と活性の定義に異なる $cl$ を使用することができる。

定理： $cl1$ と $cl2$ を可補モジュラー束 $\langle L, \land, \lor, 0, 1 \rangle$ 上の閉包作用素とし、任意の $x \in L$ に対して $cl1(x) \leq cl2(x)$ が成り立つとする。このとき $cl1$ -安全性 $y \in L$ と $cl1$ -活性 $z \in L$ が存在して $x = y \land z$ が成り立つ

この一般化を利用して論文中では、分岐時間的 (branching-time) な性質、すなわちここまで見てきたような状態の直線的な無限列ではなく、状態をノードとするような木構造に対して定義された性質についても、従来と類似の分解定理が成立することが示されている。

定理：任意の分岐時間的な性質は、existentially safe な性質と existentially live な性質の共通部分、universally safe な性質と universally live の共通部分、existentially safe な性質と universally live な性質の共通部分、のすべてのパターンに分解可能である

ここで existentially および universally の具体的な定義は省略するが、それぞれ別の閉包作用素を通じて定義される性質である。非形式的な表現でいえば、状態がなす木構造において、existentially safe は「うまいルートの辿り方をすれば悪いことが起こらない」性質、universally safe は「どんなルートを辿ったとしても悪いことが起こらない」性質といった意味になる。

分岐時間的な分解定理は先に挙げた束上の分解定理の直接的な系であり $cl1$ が existentially、 $cl2$ が universally に対応している。universally safe と existentially live の組み合わせだけが抜けているのは条件 $cl1(x) \leq cl2(x)$ が満たされないためであり、実際にこの組み合わせでは分解できない反例が存在する。

またこの分岐時間の例は、束論による定義が位相による定義の真の拡張になっていることを示す例でもある。実際、universally を定義する閉包作用素は位相的な意味でも閉包を与えるが、existantially を定義する閉包作用素は位相的な意味では閉包にはならない。

階層的な特徴付け

また別の観点からの定式化を用いたシステムの性質の分類として、Chang らによる研究が知られている [CMP93]。従来の Alpern-Schneider 型の研究では性質を安全性と活性に二分していたが、Chang らは階層的なモデルを提案している。

既に述べた通り、Alpern と Schneider による分類は閉集合を安全性、稠密集合を活性とするものであった。Chang らの論文中では複数の視点から同値な定義が与えられているが、対応がわかりやすいように位相による定義を用いて彼らの分類を述べると以下のようになる。

定義：閉集合、開集合、加算個の閉集合の和、加算個の開集合の共通部分として特徴付けられるクラスをそれぞれ Safety、Guarantee、Response、Persistence と呼ぶ

さらに、副次的なクラスとして Safety と Guarantee の両方に属するクラスを Obligation、Response と Persistence の両方に属するクラスを Reactivity として定義している。

面白いのは、理論的に自然な階層として定義されたこれらの性質と、システムに求められる要件の階層がよく対応しているように見えることである。例えば Persistence を定義する「加算個の開集合の共通部分」というクラスは、 $F_{\sigma}$ とも表され集合論では古くからよく知られた研究対象であるが、これは非形式的な表現では「いつかは成立し、かつ一度成立するとその後は成立したままになる」という状況に対応している。

なお、Chang らによる Safety の定義は Alpern-Schendier 型の安全性と共通しているが、他のクラスは活性とは直行する概念である。実際、Guarantee、Obligation、Response、Persistence、Reactivity のいずれかを $\kappa$ で表すと、以下の分解定理が成立する。

定理：クラス $\kappa$ に属する任意の性質 $\Pi$ に対して、Safety に属する $\Pi_{S}$ と $\kappa$ かつ活性に属する $\Pi_{L}$ が存在して $\Pi=\Pi_{S} \cap \Pi_{L}$

参考文献

[AS85] B. Alpern, and F. B. Schneider. 1985. “Defining Liveness.” Information Processing Letters 21 (4): 181–85.

[AS87] B. Alpern, and F. B. Schneider. 1987. “Recognizing Safety and Liveness.” Distributed Computing 2 (3): 117–26.

[CMP93] E. Chang, Z. Manna, and A. Pnueli. 1993. “The Safety-Progress Classification.” In Logic and Algebra of Specification, 143–202. Springer Berlin Heidelberg.

[CRZ15] N. Chris, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff. 2015. “How Amazon Web Services Uses Formal Methods.” Communications of the ACM 58 (4): 66–73.

[DG08] V. Diekert, and P. Gastin. 2008. “First-Order Definable Languages.” Logic and Automata 2: 261–306.

[MR03] P. Manolios, and R. Trefler. 2003. “A Lattice-Theoretic Characterization of Safety and Liveness.” In Proceedings of the Twenty-Second Annual Symposium on Principles of Distributed Computing, 325–33. PODC ’03. New York, NY, USA: Association for Computing Machinery.

[MDB14] G. P. Maretić, M. T. Dashti, and D. Basin. 2014. “LTL Is Closed under Topological Closure.” Information Processing Letters 114 (8): 408–13.

[TSM20] R. Taft, I. Sharif, A. Matei, N. VanBenschoten, J. Lewis, T. Grieger, K. Niemi, et al. 2020. “CockroachDB: The Resilient Geo-Distributed SQL Database.” In Proceedings of the 2020 ACM SIGMOD International Conference on Management of Data, 1493–1509. SIGMOD ’20. New York, NY, USA: Association for Computing Machinery.

[W83] P. Wolper. 1983. “Temporal Logic Can Be More Expressive.” Information and Control 56 (1): 72–99.