Model Checking Strategic Abilities in Information-sharing Agents

We study the formalism of visibly CGS (vCGS) which contains an explicit expression of private-data sharing in Multi-Agent System. In vCGS, each agent “a” has a syntactic/semantic endowment to temporarily allow som other agent “b” to see the value of some of a’s variables. We prove here the decidability of the model-checking problem for a fragment of ATL with imperfect information on a subclass of vCGS, called A-cast vCGS, where atom visibilities within a coalition A evolve simultaneously for all agents – that is, whenever some atom is made visible to some agent, it is visible to all agents in the coalition. On these, we prove that verification of the strategic abilities of coalition A is decidable, that is, for formulas which utilize only coalition A.

Authors

• Catalin Dima.

Keywords

No keywords are indexed for this paper.