Skip to content

Instantly share code, notes, and snippets.

@y-taka-23
Created May 30, 2026 11:14
Show Gist options
  • Select an option

  • Save y-taka-23/c609c4b78c717381fdcb3f04fed3425f to your computer and use it in GitHub Desktop.

Select an option

Save y-taka-23/c609c4b78c717381fdcb3f04fed3425f to your computer and use it in GitHub Desktop.
形式手法特論:公平性制約の位相的特徴づけ

形式手法特論:公平性制約の位相的特徴づけ

安全性-活性分解定理

並行システムにおいて、安全性(safety)と 活性 (liveness)という仕様のクラスは広く知られており、それぞれ「悪いことが決して起こらない」「良いことがいつか起こる」として説明されることが多い。この非形式的な定義に対して、1985 年、Alpern と Schneider によって、以下のような位相的な特徴づけが与えられた。

  • 定義:安全性とは閉集合のことである
  • 定義:活性とは稠密集合のことである

システムの動作を表した実行列が二つ与えられたとする。このとき「先頭から各ステップを見て、あるところまで一致する」という関係を考えると、この関係を用いて実行列の間に距離を定義することができる。つまり、例えば実行列 σ1 と σ2 が 3 ステップ目まで一致しており、一方で σ1 と σ3 は5 ステップ目まで一致している場合、σ1 と σ 3 の方が σ1 と σ 2 よりも「近い」と定義するのである。

実行列の全体はこの距離により位相空間をなす。Alpern-Schneider の定義を言い換えると、安全性とは「先頭から有限ステップで違反が判明する性質」であり、活性とは「途中までのステップがどうであっても、そこから先の進行を調整すれば成り立つ性質」である。さらに、位相空間の言葉で定式化したことの恩恵で、以下のような非常にクリアな主張が成り立つ。

  • 定理:任意の仕様は、安全性と活性の連言として表現できる。

公平性の定式化

一方、複数のプロセスが並行して動作するシステムにおいて、しばしば公平性 (fairness) という仕様が扱われることがある。公平性は「非決定的な動作が偏りなく生じること」を意味する性質であり、種々のバリエーションがあるが、代表的なものは弱公平性 (weak fairness) と強公平性 (strong fairness) である。非形式的には、前者は「ある遷移が生じ得る条件が常に成り立つならば、その遷移は無限回生じる」、後者は「ある遷移が生じ得る条件が無限回発生するならば、その遷移は無限回生じる」と表現される。

では、この公平性は位相的にはどのように特徴づけられるだろうか?「いつか生じる」というニュアンスから見ると、公平性は活性と近いように見える。実際「プロセス A と B が並行して動作しているとき、A も B も無限回動作する」という性質は典型的な公平性であるが、位相的な意味で活性でもある。途中までのステップがどうであれ、その後に ABABAB… を繋げれば成り立つからである。

しかし、活性は必ずしも公平性として自然なものだけとは限らない。例えば「ある時点以降、常に A だけが動作する」という公平性とは逆方向の性質も活性の一種である。実際、途中までのステップがどうあれ、その後に AAAAA… を繋げれば成り立つ。逆に、典型的な「公平なスケジューリング」であると思われるラウンドロビン、つまり「最初のステップから常に A と B が交互に動作する」という性質は、活性ではなくむしろ安全性である。実際、違反が発生するときは有限ステップのどこかで AA や BB が観測されるはずである。

また、活性すなわち稠密集合の難点として、連言に対して閉じていないことが挙げられる。通常、複数プロセスのそれぞれについて公平性を考えたいため、それら条件の連言もまた公平性であることが期待されるが、活性はこれを満たさない。

このような問題設定のもとに、公平性に対して位相的定義を与える研究とし、 Völzer、Varacca、Kindler による 2005 年の論文がある。彼らは公平性に対して以下のような定義を与えた。以下、この定義が公平性のニュアンスをよく表していることを解説する。

  • 定義:閉包の内部が空となる集合を疎集合 (nowhere-dense set) と呼ぶ

  • 定義:疎集合の可算和を痩集合 (meager set) と呼ぶ

  • 定義:公平性とは補集合が痩集合 (co-meager) な集合のことである

Co-Meager 性の直感的理解

前置きとして、システムの仕様を検査する上で、公平性は「検査の前提」として扱われることが多い。すなわち「並行プロセスがある程度公平にスケジューリングされるならば、その動作の結果は何らかの条件を満たす」という命題をチェックするのである。このことから考えると、ある性質 F が公平性であるとしたら、典型的な実行では F が成り立つべきであり、成り立たないケースは全体か見てエッジケースであることが期待される。すなわち F は自身が十分に「典型的な集合」であり、F の補集合は「例外的な集合」として定式化されるべきであると思われる。この「例外性」を痩集合として特徴づけたのが Völzer-Varacca-Kindler の貢献である。

実行列の位相の話の前に痩集合のイメージを得るため、実数を例に考えよう。有理数は実数の中で稠密である。実際、どのような実数に対しても、それを任意距離で近似するような有理数が存在する。同様に、無理数も実数の中で稠密である。つまり「稠密である」という性質だけだと有理数と無理数は同じ立ち位置にいる。

一方、よく知られている話として、有理数は可算個しか存在しない一方、無理数は非可算個存在している。このことからも予感される通り、無理数の方が実数として「典型的」である。実際、一点のみからなる集合は疎集合であるため、可算集合である有理数は痩集合である。すなわちその補集合である無理数は co-meager な集合であり、これが今考えたい「典型的さ」に相当する。有理数は実数の内部にくまなく存在するが、それ自体はとても「細い」のである。

再び、実行列の位相を考えよう。公平性 F とは「動作 A が無限回生じる」というニュアンスを持つ性質だった。ここで集合 A_n で「n ステップ目以降にいつか一回でも A が生じる」という性質を表すことにしよう。このとき F は全ての n にわたって A_n の連言を取ったものである。

まず、各 A_n は開集合である。実際、A_n の否定は「n ステップ目以降は永遠に A が生じない」なので、もし A が生じるという違反があれば有限ステップで確定する。つまり否定が閉集合なのだから A_n は開集合である。さらに、各 A_n は稠密でもある。実際、途中までのステップがどうあれ、その後に A を繋げれば A_n を満たすようにできる。

ここで、今考えている実行列がなす位相空間は、Baire 空間と呼ばれるクラスに属する。Baire 空間の定義は可算個の稠密開集合の共通部分は再び稠密、というものであり、したがって上記の F は稠密な G_δ 集合となる。また、以下の定理が知られている。

  • 命題:Baire 空間において、集合 F が co-meager であることと、ある稠密 G_δ 集合 E が存在して E ⊆ F となることは同値

非形式的に述べると、Baire 空間は、可算個の「例外的な集合」を除外しても、まだ「典型的な集合」が十分豊富に残るような空間であるといえる。この事実により、「動作 A が無限回生じる」という公平性の直感的な理解と、Völzer-Varacca-Kindler による co-meager 性の定義が整合性を持って繋がることになる。また、co-meager な集合は可算個の連言について閉じており、この点でも公平性の定義として適切である。

まとめ

以上が、公平性に対する位相的特徴づけの概要である:

  • 安全性や活性にはもともと位相的な定義が知られていた
  • 公平性は活性の一部だが、それだけでは条件不足
  • 公平性は co-meager 性として特徴づけられる
  • co-meager 性は「無限回生じる」という直感とうまく対応
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment