Multi-Modal CTL: Completeness, Complexity, and an Application

Thomas Ågotnes, Wiebe Van Der Hoek, Juan A. Rodríguez-Aguilar, Carles Sierra, Michael Wooldridge

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


We define a multi-modal version of Computation Tree Logic (ctl) by extending the language with path quantifiers E and A where d 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 in turn. We also show that the logic is decidable and that its satisfiability problem is no harder than the corresponding problem for ctl. We then demonstrate how Normative Systems can be conceived as a natural interpretation of such a multi-dimensional ctl logic.
Original languageEnglish
Pages (from-to)1-26
Number of pages26
JournalStudia Logica
Issue number1
Publication statusPublished - 01 Jun 2009

Bibliographical note

Copyright 2009 Elsevier B.V., All rights reserved.

ASJC Scopus subject areas

  • Logic


Dive into the research topics of 'Multi-Modal CTL: Completeness, Complexity, and an Application'. Together they form a unique fingerprint.

Cite this