LTLとCTLはどちらも命題論理の部分であり、CTL*の一部でもあります。
線形時相論理（LTL）
LTLは時間を参照するモダリティを持つモーダルな時相論理です[1]。スマートコントラクトの文脈では、LTLはコントラクトが通過する可能性のある状態のシーケンスにわたって保持されなければならない特性を指定および検証するために使用できます。
例えば、開発者は「もし条件$X$が$true$ならば、条件$Y$は最終的に$true$になる」というような主張を行うことができます（LTLでは$X \implies \lozenge Y$と表されます）。これは、イベントのシーケンスの後に特定の結果を保証する必要があるスマートコントラクトに特に有用です。
ユーザーが一定量の資産をデポジットすると、最終的に利息の支払いを受け取ることを保証する重要な機能を持つスマートコントラクトを想像してください。LTLを使用して、この特性を次のように正式に検証できます。
$$ G(\text{deposit} \implies F\text{ interest payment}) $$
このLTLの式は、デポジットアクションが発生すると、それが最終的に（$F$）利息の支払いに続くことがグローバルに$true$（$G$）であることを示しています。この種の時相論理により、開発者やセキュリティアナリストは、スマートコントラクトが時間をかけて意図したとおりに動作することを証明できます。
LTLは時相演算子を使用して、未来に関する論理的なステートメントを表現します。例えば：
- $G$（グローバルに）：ある条件がすべての未来の状態で保持されなければならない。
- $F$（最終的に）：ある条件が将来のある状態で最終的に保持される。
- $X$（ネクスト）：ある条件が次の状態で保持される。
- $U$（アンティル）：ある条件が別の条件が保持されるまで保持される。
計算木論理（CTL）
LTLが線形で時間の流れを単一のパスとして考慮するのに対し、CTLは分岐時間を可能にし、任意の時点から複数の未来の可能性を考慮できます[2]。CTLはパス量化子を導入して、任意の状態からのシステムのすべての可能な実行を表す構造である計算木の特性を指定します。
2つのパス量化子は：
- $A$（すべてのパスについて）：特性がすべての可能な未来のパスで保持されなければならないことを指定します。
- $E$（パスが存在する）：特性が保持される少なくとも1つの可能な未来のパスが存在することを指定します。
CTLはLTLと同じ時相演算子を使用しますが、パス量化子が前に付きます。したがって、$AG$（すべてのパスでグローバルに）や$EF$（最終的に到達するパスが存在する）のような式を見ることがあります。
例えば、特定の日付以降にのみ特定の当事者が資金を引き出すことを許可する関数を持つスマートコントラクトがあるかもしれません。CTLを使用して、「すべてのパスにおいて、もし引き出し関数が呼び出された場合、そのパスのすべての可能な継続において、呼び出し者が認可された当事者であり、日付が正しいか、または引き出しが失敗する」という特性を表現してこれを検証できます。
CTLでは、これは次のように表現できます：
$$ A[\text{withdraw} \implies (E[\text{caller} = \text{authorized} \land \text{date} \geq \text{specified}] \lor E[\text{transaction reverted}])] $$
これは、すべてのパス（$A$）において、引き出しの試みが発生した場合、呼び出し者が認可され、日付が指定された日付以降であるパス、または取引が取り消されるパス（$E$）が存在することを示しています。これにより、資金が誤って引き出されないことを保証します。
念頭に置くべきこと：LTLの合成とLTLの勝利条件に対するゲームの検証の問題は2EXPTIME完全です[3]。
これらの論理は、スマートコントラクト内の単一のトランザクションやブロックのシーケンス内の高レベルの論理シナリオをカバーするために使用して検証できると考えています。
もちろん、スマートコントラクトのようなデジタルシステムにとって、時相論理に基づく設計とモデリングは、実際の実装の前に行われるべきです。[他の検討されるデジタルシステムについても同様です]。これは検証駆動開発プロセス[4]の一部であり、可能なエラーの数を減らすために、コードの前に行われなければなりません。
参考文献
このブログ記事の議論に参加してください:
この記事は AI 搭載の翻訳ツールによって翻訳されました。翻訳に誤りがある場合はご容赦ください。すぐに校正し、考えられる誤りを修正します。誤りを見つけた場合は、GitHub で問題を作成してください。