资源论文Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems

Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems

2019-11-06 | |  48 |   46 |   0
Abstract In this work we study the model checking problem for probabilistic multiagent systems with respect to the probabilistic epistemic logic PETL, which can specify both temporal and epistemic properties. We show that under the realistic assumption of uniform schedulers, i.e., the choice of every agent depends only on its observation history, PETL model checking is undecidable. By restricting the class of schedulers to be memoryless schedulers, we show that the problem becomes decidable. More importantly, we design a novel algorithm which reduces the model checking problem into a mixed integer non-linear programming problem, which can then be solved by using an SMT solver. The algorithm has been implemented in an existing model checker and experiments are conducted on examples from the IPPC competitions.

上一篇:Unchaining the Power of Partial Delete Relaxation, Part II: Finding Plans with Red-Black State Space Search

下一篇:Goal-HSVI: Heuristic Search Value Iteration for Goal-POMDPs ?

用户评价
全部评价

热门资源

  • 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...

  • Learning to learn...

    The move from hand-designed features to learned...

  • A Mathematical Mo...

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