交互時間時相論理

時相論理の種類

コンピュータサイエンスにおいて、交互時間時相論理（ATL ）は、計算木論理（CTL）を複数のプレイヤーに拡張した分岐時間時相論理です。 ^[1] ATLは、マルチエージェントシステムや並行ゲームの計算を自然に記述します。^[2] ATLにおける定量化は、ゲームの可能な結果であるプログラムパスに対して行われます。^[3] ATLは、受容性、実現可能性、制御可能性などの問題に対処するために、交互時間式を使用してモデルチェッカーを構築します。

例

ATL では、システムの他のエージェントが何を実行していても、エージェントaとb がプロパティpが将来も保持されることを保証する戦略を持っているという事実を表現するような論理式を記述できます。 $\langle \langle \{a,b\}\rangle \rangle Fp$

拡張機能とバリアント

ATL*はATLの拡張であり、CTL*はCTLを拡張します。ATL*では、例えばより複雑な時間的目的関数を記述できます。Belardinelliらは有限トレース上のATLの変種を提案しています。^[4] ATLは、エージェントが現在行っている戦略を保存するためにコンテキストが拡張されています。ATL*は戦略ロジックによって拡張されています。 $\langle \langle \{a,b\}\rangle \rangle (Fp\land Gq)$

ATLは認識論的特徴を含むように一般化されている。2003年、ファン・デル・フックとウッドリッジは、認識論的論理の認識論的演算子を拡張した論理ATLであるATELを提案した。^[5] 2004年、ピエール＝イヴ・ショベンスは不完全な想起を持つATLの変種を提案した。^[6]

ATLでは個々の目的に関する特性を表現することはできません。そのため、2010年にChatterjee、Henzinger、Pitermanは戦略論理を導入しました。これは、戦略が一階の構成要素となる一階論理です。^[7]戦略論理はATLとATL*の両方を包含します。

参照

線形時相論理

参考文献

^ Alur, Rajeev ; Henzinger, Thomas A. ; Kupferman, Orna (1997). 「交互時間時相論理」.第38回コンピュータサイエンス基礎シンポジウム議事録. IEEEコンピュータソサエティ. pp. 100– 109. doi :10.1109/SFCS.1997.646098. ISBN 0-8186-8197-7。
^ van Drimmelen, Govert (2003). 「交互時間時相論理における充足可能性」.第18回IEEEコンピュータサイエンスにおける論理シンポジウム議事録. IEEEコンピュータ協会. doi :10.1109/LICS.2003.1210060. ISBN 0-7695-1884-2。
^ Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (2002). 「Alternating-Time Temporal Logic」. Journal of the ACM . 49 (5): 672– 713. doi :10.1145/585265.585270. S2CID 15984608.
^ ベラディネリ、フランチェスコ;ロムシオ、アレッシオ。ムラーノ、アニエロ。ルービン、サーシャ（2018）。「有限トレース上の交互時相論理」: 77–83 . {{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）が必要です
^ ファン・デル・フック、ウィーベ; ウールドリッジ、マイケル (2003年10月1日). 「協力、知識、そして時間：交互時間型時間認識論理とその応用」. Studia Logica . 75 (1): 125– 157. doi :10.1023/A:1026185103185. ISSN 1572-8730. S2CID 10913405.
^ Schobbens, Pierre-Yves (2004-04-01). 「不完全な想起を伴う交互時間論理」.電子計算機科学理論ノート. LCMAS 2003, マルチエージェントシステムにおける論理と通信. 85 (2): 82– 93. doi : 10.1016/S1571-0661(05)82604-0 . ISSN 1571-0661.
^ Chatterjee, Krishnendu ; Henzinger, Thomas A. ; Piterman, Nir (2010-06-01). 「戦略論理」(PDF) .情報と計算. 特集号: 第18回国際並行性理論会議 (CONCUR 2007). 208 (6): 677– 693. doi :10.1016/j.ic.2009.07.004. ISSN 0890-5401.

[1] Alur, Rajeev ; Henzinger, Thomas A. ; Kupferman, Orna (1997). 「交互時間時相論理」.第38回コンピュータサイエンス基礎シンポジウム議事録. IEEEコンピュータソサエティ. pp. 100– 109. doi :10.1109/SFCS.1997.646098. ISBN 0-8186-8197-7。

[2] van Drimmelen, Govert (2003). 「交互時間時相論理における充足可能性」.第18回IEEEコンピュータサイエンスにおける論理シンポジウム議事録. IEEEコンピュータ協会. doi :10.1109/LICS.2003.1210060. ISBN 0-7695-1884-2。

[3] Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (2002). 「Alternating-Time Temporal Logic」. Journal of the ACM . 49 (5): 672– 713. doi :10.1145/585265.585270. S2CID 15984608.

[4] ベラディネリ、フランチェスコ;ロムシオ、アレッシオ。ムラーノ、アニエロ。ルービン、サーシャ（2018）。「有限トレース上の交互時相論理」: 77–83 . {{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）が必要です

[5] ファン・デル・フック、ウィーベ; ウールドリッジ、マイケル (2003年10月1日). 「協力、知識、そして時間：交互時間型時間認識論理とその応用」. Studia Logica . 75 (1): 125– 157. doi :10.1023/A:1026185103185. ISSN 1572-8730. S2CID 10913405.

[6] Schobbens, Pierre-Yves (2004-04-01). 「不完全な想起を伴う交互時間論理」.電子計算機科学理論ノート. LCMAS 2003, マルチエージェントシステムにおける論理と通信. 85 (2): 82– 93. doi : 10.1016/S1571-0661(05)82604-0 . ISSN 1571-0661.

[7] Chatterjee, Krishnendu ; Henzinger, Thomas A. ; Piterman, Nir (2010-06-01). 「戦略論理」(PDF) .情報と計算. 特集号: 第18回国際並行性理論会議 (CONCUR 2007). 208 (6): 677– 693. doi :10.1016/j.ic.2009.07.004. ISSN 0890-5401.