Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Belardinelli, Francesco | Jones, Andrew V. | Lomuscio, Alessio

Affiliations: Imperial College London, Exhibition Road, London SW7 2AZ, UK. {f.belardinelli,andrew.jones,a.lomuscio}@imperial.ac.uk

Note: [] Address for correspondence: Imperial College London, Exhibition Road, London SW7 2AZ, UK

Abstract: 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 checking a memory-less interpreted system against a CTLK property 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.

DOI: 10.3233/FI-2011-576

Journal: Fundamenta Informaticae, vol. 112, no. 1, pp. 19-37, 2011