Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments
We present an extension of interpreted systems including probabilities and communication channels. We introduce a new logic merging probabilities, knowledge, and social commitments. We advocate a reduction-based technique to model check the logic and prove its soundness. We implement the approach using the PRISM model checker.
multi-agent systems knowledge social commitments interpreted systems probabilistic model checking verification modal logic