Completeness and Complexity of Multi-modal CTL

We define a multi-modal version of Computation Tree Logic (ctl) by extending the language with path quantifiers Eδ and Aδ where δ denotes one of finitely many dimensions, interpreted over Kripke structures with one total relation for each dimension. As expected, the logic is axiomatised by taking a copy of a ctl axiomatisation for each dimension. Completeness is proved by employing the completeness result for ctl to obtain a model along each dimension at a time. We also show that the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for ctl.