Probabilistic Alternating-Time ?-Calculus:Satisfiability And Model Checking

Multi-agent systems?MASs?are composed of autonomous entities,which are acting in the same environment,reacting to the environment and coordinately implementing the system function.To capture the dynamic and uncertainty in MAS,researchers in-troduce probability into the system model,giving rise to a stochastic MAS.Probabilistic alternating-time temporal logics?PATL/PATL*?are used for specification and verifica-tion of concurrent stochastic MASs.However,the satisfiability problem of probabilistic alternating-time temporal logics has not been tackled yet and the model checking consid-ered therein either is turn-based multi-agent systems or do not have optimal strategies.Therefore,proposing a new temporal logic to specify the concurrent stochastic MAS,and solving the problem of its satisfiability and model checking become the core issue of this paper.First,this paper proposes PAMC,probabilistic alternating-time?-calculus,a new probabilistic temporal logic,which is used for specification and verification of concur-rent stochastic MASs.PAMC probabilistically extends alternating-time?-calculus?AMC?,and coalition modalities??A???in AMC are replaced with probabilistic coalition modal-ities??A??^??k?that probabilistically quantify over the strategic choices of a group of agents.PAMC subsumes both AMC and probabilistic modal?-calculus?P?TL?.PAMC and PATL,as well as PATL*,are incomparable.Then,we analyze the satisfiability problem of PAMC.We propose a decision proce-dure,presenting a novel reduction from the satisfiability problem of PAMC to the solving of parity games by utilizing intersection graphs and maximal independent sets,checking the existence of a distribution for the probabilistic constraints of formulae involved in the set,such that the game has some winning strategy iff the sentence is satisfiable.The satisfiability problem of PAMC is in 2-EXPTIME.And the model checking problem could be solved by leveraging the model checking algorithm for AMC and?-PCTL.The model checking problem for PAMC over probabilis-tic concurrent game structures?PCGSs?is in UP?co-UP and can be decided in O(?|?|·|M|?^c·dep???)time for some constant c.Finally,we design and implement the decision procedure for PAMC satisfiability in a prototype tool PAMCSolver,which is the first satisfiability checker for?probabilistic?alternating-time temporal logics and P?TL.