証明を、次の検証へ。
検証が進むと、取得済みの証拠と構築済みの証明が蓄積します。私たちは、その蓄積を次の判断に使える条件を研究しています。焦点は、照会のたびに繰り返される証明構造の構築と、タスクごとに重複する証拠取得です。
2,187→57
部分観測履歴 → 証明キー
対象となる7照会の研究例で、2,187通りの部分観測履歴を57の証明キーに整理しました。
照会の間にある情報の関係を利用すると、異なる履歴が共通の証明構造を使える場合があります。本研究では、その条件を構造化された実行モデルで導き、元の実行モデルと照合することで、必要な意味を保ちながら重複する表現を削減できることを確認しました。
再利用する構造は、適用先の入力と条件に結びつけて検査します。各履歴への適用だけでなく、依頼された履歴が欠けていないことも検査の対象です。共有した後も、何を根拠にどの結論を得たかを追える形にしています。
タスクをまたぐ証拠の活用
同じ観測元が複数のタスクに関わり、その故障状態が共通している場合、あるタスクの証拠は他のタスクの判断にも役立ちます。私たちは、この関係を持つ対象タスク群で、共同検証に必要な追加証拠の量を厳密に求めました。
基礎となる証拠を取得済みの条件で、各タスクを自身の証拠だけで個別に検証する場合より、追加の取得費用を減らせることを示しています。証明構造の共有と証拠の共同利用を通じて、積み重ねた検証を次の判断に活かす研究です。
証拠を取り直さずに済む条件。
更新によって一つの証明が使えなくなっても、保存された別の証拠の組合せが残っている場合があります。私たちは、所定の故障・更新・実行条件の下で、取得済みの証拠を切り替えながら、再取得なしで実行を完了できる必要十分条件を示しました。
さらに、特定の証拠構成族について、失敗した検査と追加取得を含む最悪時の継続費用を厳密に求めました。初期の証拠取得費用と、その後に必要となる費用を分け、宣言された戦略クラス全体に対する下界と、それを達成する手順を示しています。