Verification of Multi-Agent Systems via Predicate Abstraction against ATLK Specifications

We present a predicate abstraction technique for the verification of multi-agent systems against specifications defined in the epistemic logic ATLK, interpreted on a three-valued semantics. We reduce an infinite-state multi-agent program to a finite model by generating predicates automatically via SMT calls. We show that if an ATLK specification is either true or false in the abstract model, then that is also the case on the original infinite state model. We introduce and describe MCMAS PA, a toolkit implementing the technique here described. MCMAS PA supports the three-valued semantics for ATLK, automatically generates program abstractions for a multi-agent system by means of automatic SMT calls, encodes the corresponding program in BDDs and reports the result. The experimental results obtained confirm that MCMAS PA can verify infinite-state multi-agent systems of interest.