交互時間時相論理

コンピュータサイエンスにおいて、交互時間時相論理（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年に、van der HoekとWoodridgeは、認識論的論理からの認識論的演算子で拡張された論理ATLであるATELを提案した。^[5] 2004年に、Pierre-Yves Schobbensは不完全な想起を持つ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). 「交互時間時相論理」. Journal of the ACM . 49 (5): 672–713. doi :10.1145/585265.585270. S2CID 15984608.
^ ベラディネリ、フランチェスコ;ロムシオ、アレッシオ。ムラーノ、アニエロ。ルービン、サーシャ（2018）。「有限トレース上の交互時相論理」: 77–83。 {{cite journal}}:ジャーナルを引用するには|journal=(ヘルプ)が必要です
^ van der Hoek, Wiebe; Wooldridge, Michael (2003-10-01). 「協力、知識、および時間: 交互時間時間認識論理とその応用」. 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). 「交互時間時相論理」. Journal of the ACM . 49 (5): 672–713. doi :10.1145/585265.585270. S2CID 15984608.

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

[5] van der Hoek, Wiebe; Wooldridge, Michael (2003-10-01). 「協力、知識、および時間: 交互時間時間認識論理とその応用」. 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.