资源分类
》 资源 》论文》Symbolic Model Checking for One-Resource RB±ATL†

Symbolic Model Checking for One-Resource RB±ATL†

2019-11-18 | |  61 |   47 |   0

Abstract RB±ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The modelchecking problem for RB±ATL is known to be decidable. However the only available modelchecking algorithm for RB±ATL uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB±ATL, 1RB±ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB±ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces.

上一篇：Active Learning from Crowds with Unsure Option

下一篇：The Complexity of Model Checking Succinct Multiagent Systems

用户评价
全部评价

热门资源

  • Learning to Predi...

    Much of model-based reinforcement learning invo...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • The Variational S...

    Unlike traditional images which do not offer in...

  • A Mathematical Mo...

    Direct democracy, where each voter casts one vo...

  • Rating-Boosted La...

    The performance of a recommendation system reli...