要約
形式的な手法を使用して合成された戦略は複雑になる可能性があり、多くの場合、無限のメモリを必要とします。これは、マルチ エージェント システム (MAS) をモデル化しようとするときに予期される動作に対応しません。
このような行動を捕捉するために、自然戦略は、記憶を使って戦略を立てるエージェントの能力とモデルチェックの複雑さの間のバランスを取る最近提案されたフレームワークですが、これまでは完全に決定論的な設定に制限されていました。
初めて、自然戦略の下で確率的時相論理 PATL および PATL* を検討します (それぞれ NatPATL および NatPATL*)。
主な結果として、確率的 MAS において、アクティブな連合が決定論的戦略に制限されている場合、NatPATL モデル検査が NP 完全であることを示します。
また、同じ制限を持つ NatPATL* の 2NEXPTIME 複雑さの結果も提供します。
制限のない場合、NatPATL には EXPSPACE 複雑度、NatPATL* には 3EXPSPACE 複雑度を与えます。
要約(オリジナル)
Strategies synthesized using formal methods can be complex and often require infinite memory, which does not correspond to the expected behavior when trying to model Multi-Agent Systems (MAS). To capture such behaviors, natural strategies are a recently proposed framework striking a balance between the ability of agents to strategize with memory and the model-checking complexity, but until now has been restricted to fully deterministic settings. For the first time, we consider the probabilistic temporal logics PATL and PATL* under natural strategies (NatPATL and NatPATL*, resp.). As main result we show that, in stochastic MAS, NatPATL model-checking is NP-complete when the active coalition is restricted to deterministic strategies. We also give a 2NEXPTIME complexity result for NatPATL* with the same restriction. In the unrestricted case, we give an EXPSPACE complexity for NatPATL and 3EXPSPACE complexity for NatPATL*.
arxiv情報
著者 | Raphaël Berthon,Joost-Pieter Katoen,Munyque Mittelmann,Aniello Murano |
発行日 | 2024-01-22 18:04:26+00:00 |
arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google