Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions

We develop the theoretical foundations of a predicate abstraction methodology for the verification of multi-agent systems. We put forward a specification language based on epistemic logic and a weak variant of the logic ATL interpreted on a three-valued semantics. We show that the model checking problem for multi-agent systems in this setting is tractable by giving a provably correct procedure which admits a PTime bound. We give a constructive technique for generating abstract approximations of concrete multiagent systems models and show that the truth values are preserved between abstract and concrete models. We evaluate the effectiveness of the methodology on a variant of the bit-transmission problem.