Multi-agent systems involve multiple distinct, autonomous agents which typically act to achieve a private or common goal. We are often interested in specifications concerning both the temporal evolution of such systems as well as other properties of the agents, such as knowledge.
This talk will discuss some of my work on symbolic model checking for CTL*K specifications. I will introduce the Clarke, Grumberg and Hamaguchi symbolic tableau algorithm for reducing LTL model checking to CTL model checking with fairness, and then show how this can be used and adapted to handle CTL* and epistemic modalities.
I will also discuss an implementation of these algorithms in MCMAS-CTL*K, an extension of the MCMAS model checker which supports CTL*K specifications.