Model checking Temporal-Epistemic Logic using alternating tree automata

We introduce a novel automata-theoretic approach for the verification of multi-agent systems. We present epistemic alternating tree automata, an extension of alternating tree automata, and use them to represent specifications in the temporal epistemic logic CTLK. We show that model check- ing a memory-less interpreted system against a CTLK prop- erty can be reduced to checking the language non-emptiness of the composition of two epistemic tree automata. We report on an experimental implementation and discuss preliminary results. We evaluate the effectiveness of the technique using two real-life scenarios: a gossip protocol and the train gate controller.

Authors

• Francesco Belardinelli Imperial College
• Andrew Vaughan Jones
• Alessio Lomuscio Imperial College London

Keywords

No keywords are indexed for this paper.