カード異議申し立てワークフロー検証
合成フォーム追加ワークフローにおいて、有効な請求エラー通知が調査を経ることなくモデル上の6日目にクローズ状態に到達します。「Dispute Workflow Verification」は、提供されたそのモデル内のあらゆる到達可能ルートを探索し、設定された義務をチェックして、不合格となったプロパティの背後にあるイベントパスを明らかにします。
93
探索された到達可能状態
同梱のフォーム追加モデル
4 of 4
設定されたプロパティが不合格
同一の合成モデル
Day 6
通知がクローズされたデッドステートに到達
モデルクロック上の値（実際の顧客案件ではありません）
これらは作成されたJSONモデルおよびエンコードされたデモルールの結果であり、銀行の実稼働異議申し立て運用に関する評価ではありません。
従来のトラッカーは、自身が受け取った異議申し立てを報告することはできます。しかし、想定ケースのテストにそのルートが含まれていなければ、有効な通知が調査前にクローズされたルートを示すことはできません。
この CFPBの2024年10月Apple同意命令 では、最初の異議申し立て提出後に追加のフォームが要求され、そのフォームが完了しなかった場合に要件を満たす通知が転送されなかった事例が記述されています。本デモのフォーム追加ケースは、その障害モードを説明するための再構成であり、Appleのステートマシンや実際の顧客記録の再現ではありません。
レビューにおける問いは明確です：有効な通知の後、モデル化されたルートのいずれかが、調査がもはや不可能となる状態に到達し得るか？
状態グラフとルールの結果は、提供されたJSONワークフローに対して実行される決定論的Pythonコードから導出されます。
01 / MODEL
位置、遷移、タイミング範囲、フラグ、および製品やネットワークのラベルが、4つの合成ワークフローを定義します。
02 / EXPLORE
幅優先探索により、有効な通知の状態が調査から隔離されたまま行き詰まる可能性がないかをチェックし、設定されたタイミングフラグに照らしてパスを追跡します。
03 / REVIEW
結果は、プロパティの判定をグラフ、モデルクロック値を含む順序付きの反例、およびエクスポート可能なレビュー証明書へと結びつけます。
プロパティの判定は、 COUNTEREXAMPLE （チェッカーが違反ルートを検出したとき）、 PROVEN （探索された有限モデル全体で成立するとき）、または BOUNDED （200暦日の上限によりタイムライン結論が制約されるとき）となります。決定論的チェッカーのみがこれらのステータスを割り当てます。オプションのモデル合成エージェントはモデルを起草できますが、検証を行うことはありません。
記録されたウォークスルーの解説
これらの画面は提供された合成ワークフローからのものです。まずベースラインの緑色の結果を確認し、次にチェックされなかった分岐をたどります。各画像はフルサイズで開きます。
01 / COMPARE THE CHECKS
標準的なトラッカーはフォーム完了ルートを追跡し、判定として COMPLIANTを報告します。状態探索は、到達可能な別の分岐が失敗し得るかを問います。同一の作成済みフォーム追加モデルにおいて、判定は NON-COMPLIANT （設定されたルールに対する不適合）となります。
これら2つの結果は異なる問いに答えています。ベースラインは選択されたルートが合格したことを示しますが、調査前にそのルートから外れた通知については何も語っていません。
02 / FIND THE BRANCH
グラフ上では、モデル化された通知は Messages Submitted から Secondary Form Requestedへと遷移します。フォームを完了するとルーティングおよび調査へと進みます。これに対し、タイムアウトが発生すると Closed Incompleteに到達します。チェッカーは93の到達可能状態を探索し、提供されたこのモデル内で設定された4つのプロパティすべてが不合格であることを検出します。
03 / INSPECT THE WITNESS
不合格となったプロパティには、順序付けられた反例が付随します。ここでは、モデル化されたシーケンスが0日目の提出、1日目の二次フォームの要求、および6日目のタイムアウトによるクローズを記録しています。そのパス上では通知が調査に到達することはありません。
04 / CHECK THE CHANGE
個別に用意された修正モデルでは、不完全フォーム通知をクローズするのではなく、ルーティングおよび調査へと送信します。このルート変更により、設定された4つのプロパティすべてについて PROVEN が153の到達可能状態にわたり成立します。この結論は、提供された有限モデルおよびそのエンコードされたプロパティに固有のものです。
A SECOND WORKFLOW / TIMING
夜間バッチの例では、別の合成モデルにエンコードされた条件付き仮クレジットの前提条件をテストします。あるパスでは、モデル化されたクレジットがそのモデルの10-business-day check（10営業日チェック）の制限を超えた14営業日目に初めて計上されます。チェッカーは、79の到達可能状態において設定された7つのプロパティのうち1つの反例を返します。実際の Reg E の例外規定や適用期間には個別のレビューが必要です。
この比較は、同一の作成済みワークフローにおける想定ルートのベースラインと状態探索との比較です。実際に配備された銀行システムに対するベンチマークではありません。
| レビュー対象ルート | ここで確認できること | 未解決のまま残されること |
|---|---|---|
| ハッピーパスのベースライン | 想定されたルートは COMPLIANT を報告します。 | 二次フォームのタイムアウト分岐を探索することは決してありません。 |
| 状態空間探索 | 提供されたフォーム追加モデルにおいて、93の到達可能状態、および調査を経ずに ClosedIncomplete に至るルート。 | 提供されたモデルが実際のワークフローと一致しているかどうか。 |
| 修正済みモデル | 153の到達可能状態にわたり、設定された4つのプロパティすべてが成立します。 | これらのプロパティが適用可能なあらゆる義務や例外規定を網羅しているかどうか。 |
本デモの4つのワークフローおよび10件のベンチマークフィクスチャは、作成された合成モデルです。このページには、ライブの銀行、カードネットワーク、勘定系コアシステム、書面生成システム、または消費者データへの接続は一切なく、レビュー証明書はモデル検証の成果物であり規制当局による承認ではありません。エンコードされた Reg Z および Reg E のクロックは、 Reg Z の請求エラー規則 および Reg E のエラー解決規則を簡略化したものです。それらの通知条件、例外規定、および実際の適用可能性については、専門家による個別の評価が必要です。Visa および Mastercard の処理期間は例示用に設定された値であり、検証された最新のネットワーク規則ではありません。
すでにキューに入っている案件のみを追跡するダッシュボードは、そのキューに到達しなかった有効な通知を見落とす可能性があります。この合成フォーム追加モデルでは、ハッピーパスのベースラインは COMPLIANT と報告しますが、状態探索によって、調査を経ることなくモデル上の6日目に有効な通知から ClosedIncomplete に至るルートが検出されます。反例はそのルート上の各イベントを示します。
いいえ。PROVEN は、提供された有限モデルの探索された状態全体において、設定されたプロパティが成立したことを意味します。実際のコンプライアンスは、モデルが実稼働のワークフローと一致しているか、通知が要件を満たしているか、どの規則や例外が適用されるかによって左右されます。本デモはレビューを支援するツールであり、法的意見ではありません。
記録された本デモは、4つの合成 JSON ワークフローモデルを使用しています。銀行のキュー、勘定系コアシステム、通知生成システム、Visa または Mastercard のシステム、あるいは顧客記録へのライブ接続はありません。実際の評価には、まず実際のプロセスおよび適用される義務に関する検証済みモデルが必要となります。
不合格となった設定プロパティについて、チェッカーは状態グラフ、モデル化されたイベントとクロック値を含む順序付きの反例トレース、およびエクスポート可能なレビュー証明書を提示します。フォーム追加の例では、トレースは調査を経ずに二次フォームのタイムアウト後に ClosedIncomplete に到達します。証明書には検証されたモデルと制限事項が記録されますが、規制当局による承認ではありません。
本デモでは簡略化されたエンコード済みクロックを使用しています。Reg Z の解決チェックでは「丸2請求サイクル」の条件を90-calendar-day ceiling（90暦日の上限）に縮約し、Reg E の10-business-day check（10営業日チェック）では休日を考慮しない固定の7/5 conversion（7/5変換）を使用しています。例外規定、延長期間、およびルールの適用可能性については、専門家による個別のレビューが必要です。
探索は200 calendar days（200暦日）に制限されています。適用可能なタイムラインプロパティについて反例が見つからずにその上限に達した場合、チェッカーは PROVEN ではなく BOUNDED を報告します。探索されたパス内で検出された反例は引き続き表示されます。
いいえ。設定されている場合、オプションのモデル合成エージェントがワークフローモデルを提案することはできますが、その状態を探索し PROVEN、COUNTEREXAMPLE、または BOUNDED を割り当てるのは決定論的 Python コードです。付属する4つのケースは、LLM やライブのネットワーク接続なしで実行されます。
本デモのより広い背景については、関連するリサーチをご覧ください。
ソリューション全体
銀行向け金融コンプライアンス形式検証ソリューションを見る →有益な第一歩は、要件を満たす通知がどこで受付され、待機し、ルーティングされ、クローズされるかをマッピングすることです。
本稼働プロセスの証拠としてモデルを扱う前に、ワークフローモデルの策定、テストすべき義務の選定、および異議申し立て運用・エンジニアリング・コンプライアンスの専門家を交えた反例のレビューを支援します。
