A Bitopological Approach to Finite Reduction and Bounded Exact-Value Certificates for Fitting's Finite Heyting-valued Modal Logic

技術要約：Fittingの有限ハイティング値様相論理における、ビットポロジカルなアプローチによる有限簡約化と有界な正確な値の証明書

1. 問題設定

本論文は、Fittingの有限ハイティング値様相論理における**有限状態への簡約化（finite-state reduction）および反例抽出（counterexample extraction）**の問題を扱う。この論理において、論理式はバイナリなブール代数ではなく、固定された有限のハイティング代数 $L$ に値を取る。必然性演算子 $\Box$ は、アクセス可能な状態における真理値の結び（下限）として解釈される。

核心となる課題は以下の二点である：

1. 状態の簡約化： 有限の $L$ 値クリプキ・モデル $M = (W, R, V)$ と有限の命題語彙 $\Sigma$ が与えられたとき、$\Sigma$ に含まれるすべての論理式の**正確な真理値（exact truth value）**を保持する簡約されたモデルをどのように構築するか。有効性（真理値1）のみが重要となる古典的なモデル検査とは異なり、多値検証では中間的な真理値（不確実性や部分的な真理性など）を保持する必要がある。
2. 証明書の構築： 特定の論理式 $\phi$ と状態 $x$ において $\phi$ が成立しない場合（すなわち $J\phi K_M(x) \neq 1$）、元のモデルの状態空間とは独立して、$L$ と $\phi$ の構文にのみ依存するサイズを持つ、有限の木構造のような反例を構築できるか。

濾過（filtration）や分割細分（partition refinement）といった既存の手法は、多くの場合ブール的な有効性に焦点を当てているか、あるいは正確な値の保持のためにビットポロジカルな双対性を明示的に利用していない。

2. 手法

著者らは、格子値様相代数の双対理論から導出された**関係的ビットポロジカル表現（relational bitopological representation）**を用いている。その手法は、主に以下の二つの段階で構成される。

A. ビットポロジカルな表現と双対性
本論文は、$L$-ML代数（有限ハイティング代数上の様相代数）の圏と、関係的ペア・ブール空間（$PRBS_L$）の圏との間の双対性を利用している。

• 双対空間： 代数 $A$ に対して、その双対空間は、二つの位相（$\tau_1, \tau_2$）と標準的な二項関係 $R_A$ を備えたホモモルフィズムの集合 $X_A = \text{Hom}_{VAL}(A, L)$ である。
• 標準的な関係： 関係 $R_A$ は、$h R_A k$ であることの条件を、すべての $a \in A$ に対して $h(\Box a) \leq k(a)$ と定義することで、双対空間における様相意味論を捉える。
• 表現定理： 本論文は、$L$-ML代数の圏が $PRBS_L$ と双対同値であることを確立しており、これにより代数的演算が位相的および関係的な構造に対応することを保証している。

B. 観測的同値性による有限簡約化
有限モデル $M$ と語彙 $\Sigma$ に対し、著者らは $\Sigma$ の原子的な値付け $V(p)$ によって生成される様相観測代数（modal observation algebra） $A^\Sigma_M$ を定義する。

• 評価写像： 写像 $\eta^\Sigma_M: W \to X_{A^\Sigma_M}$ は、$\eta^\Sigma_M(x)(f) = f(x)$ によって定義される。
• 観測的同値性： 二つの状態 $x, y$ は、生成された代数のすべての論理式に対して同じ真理値を与えるとき、同値である（$x \equiv^\Sigma_M y$）。
• 商構成： 簡約されたモデルは、商 $W / \equiv^\Sigma_M$ として構築される。著者らは、この商がビットポロジカル双対における有限像 $X^\Sigma_M = \eta^\Sigma_M[W]$ と同型であることを証明している。決定的なことに、簡約されたモデル上の遷移関係は、標準的な双対関係 $R_{A^\Sigma_M}$ の制限として示される。

C. 有界な証明書構築
反例抽出に対処するため、著者らはハイティング代数 $L$ の有限な高さ $h(L)$ を利用する。

• 結びの圧縮（Meet Compression）： 補題により、任意の集合 $S \subseteq L$ の結びは、サイズ $|S_0| \leq h(L) - 1$ を満たす部分集合 $S_0 \subseteq S$ によって保持されることが証明されている。
• 木の構築： 論理式 $\phi$ の様相深さ $d$ と状態 $x$ に対し、木構造のモデル $C(M, x, \phi)$ が構築される。各ノードにおいて、$\Box$ 部分論理式の結びを保持するために必要な後続状態のみが保持される。
• サイズ境界： 分岐数は $(h(L) - 1) \times m_\Box(\phi)$ であり、ここで $m_\Box(\phi)$ は異なる $\Box$ 付きの部分論理式の数である。総サイズは元のモデルのサイズには依存しない。

3. 主な貢献と結果

1. 観測的商と双対像の同型性
主要な理論的結果は、有限のFittingモデルの観測的商が、その生成された観測代数のビットポロジカル双対における有限像と同型であることである。

• 正確な値の保持： この簡約化は、$\Sigma$ 上のすべての論理式の有効性だけでなく、正確な真理値を保持する。任意の $\phi \in \text{Form}(\Sigma)$ と状態 $x$ について、$J\phi K_{M^{red}}([x]) = J\phi K_M(x)$ が成立する。
• 最小性： この商は、すべての生成された観測が分解（factor）されるような、すべての全射的簡約の中で最小である。もし、$\Sigma$ のすべての論理式の正確な値を保持する他の全射写像 $h: W \to Y$ が存在するならば、$|W/\equiv^\Sigma_M| \leq |Y|$ となる。

2. 有界な正確な値の証明書
本論文は、任意の論理式 $\phi$ と状態 $x$ に対して、有限の木構造の証明書 $C(M, x, \phi)$ を構築する。

• 有界性： 木の深さは $\phi$ の様相深さによって抑えられ、分岐数は $(h(L)-1)m_\Box(\phi)$ によって抑えられる。
• 反例の抽出： $J\phi K_M(x) \neq 1$ である場合、この証明書（およびその後の観測的簡約）は、正確な失敗値を保持する有限のポインテッド反例を提供する。この反例のサイズは、$L$ と $\phi$ の構文にのみ依存し、システムサイズには依存しない。

3. 有限構成手順
本論文は、観測代数を反復的に生成し、同一の評価ベクトルを持つ状態をグループ化することによって、簡約モデルを計算する効果的な有限の手順を概説している。

4. 重要性と主張

本論文は、広範な検証問題と比較して、以下の領域における重要性を主張している。

• 特定の有限簡約化： 本研究は、ビットポロジカル双対を用いて、Fittingの論理に対する有限簡約化問題の具体的な解法を提供する。簡約されたモデルは単なる任意の商ではなく、双対空間における関係的像として構造的に回収されることを明らかにしている。
• 中間値の保持： ブール的な有効性に焦点を当てる多くの簡約手法とは異なり、このアプローチは真理値の全格子構造の保持を保証する。これは、段階的、不完全、または不確実な情報システムにおいて極めて重要である。
• 論理式依存の境界： 証明書定理は、システムサイズに依存しない反例のサイズ境界を提示する。これは多値モデル検査における重要な理論的前進であり、反例の抽出複雑さが、システムの規模ではなく、論理の代数的高さと論理式の構造にのみ依存することを保証する。
• 一般的な双対性との区別： 著者らは、本論文が新しい一般的な双対理論を提案するものではないことを明示している。代わりに、既存の関係的ビットポロジカル表現を利用して、特定の簡約化問題を解決し、正確な値の保持特性を確立している。

本論文は、結びの圧縮に関する議論が $L$ の有限な高さに依存していることを指摘し、無限の高さを持つファジー余代数モデルへこれらの結果を拡張することは未解決の課題であると結論付けている。