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.