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 journalArticle

3 Citations (Scopus)

Abstract

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
Volume92
Issue number1
DOIs
Publication statusPublished - 01 Jun 2009

Fingerprint

Completeness
Logic
Satisfiability Problem
Axiomatization
Quantifiers
Denote
Path
Demonstrate

Bibliographical note

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

Cite this

Ågotnes, T., Van Der Hoek, W., Rodríguez-Aguilar, J. A., Sierra, C., & Wooldridge, M. (2009). Multi-Modal CTL: Completeness, Complexity, and an Application. Studia Logica, 92(1), 1-26. https://doi.org/10.1007/s11225-009-9184-3
Ågotnes, Thomas ; Van Der Hoek, Wiebe ; Rodríguez-Aguilar, Juan A. ; Sierra, Carles ; Wooldridge, Michael. / Multi-Modal CTL : Completeness, Complexity, and an Application. In: Studia Logica. 2009 ; Vol. 92, No. 1. pp. 1-26.
@article{5629e76184734e718edddd9fdf43c2af,
title = "Multi-Modal CTL: Completeness, Complexity, and an Application",
abstract = "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.",
author = "Thomas {\AA}gotnes and {Van Der Hoek}, Wiebe and Rodr{\'i}guez-Aguilar, {Juan A.} and Carles Sierra and Michael Wooldridge",
note = "Copyright 2009 Elsevier B.V., All rights reserved.",
year = "2009",
month = "6",
day = "1",
doi = "10.1007/s11225-009-9184-3",
language = "English",
volume = "92",
pages = "1--26",
journal = "Studia Logica",
issn = "0039-3215",
publisher = "Springer Netherlands",
number = "1",

}

Ågotnes, T, Van Der Hoek, W, Rodríguez-Aguilar, JA, Sierra, C & Wooldridge, M 2009, 'Multi-Modal CTL: Completeness, Complexity, and an Application', Studia Logica, vol. 92, no. 1, pp. 1-26. https://doi.org/10.1007/s11225-009-9184-3

Multi-Modal CTL : Completeness, Complexity, and an Application. / Ågotnes, Thomas; Van Der Hoek, Wiebe; Rodríguez-Aguilar, Juan A.; Sierra, Carles; Wooldridge, Michael.

In: Studia Logica, Vol. 92, No. 1, 01.06.2009, p. 1-26.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Multi-Modal CTL

T2 - Completeness, Complexity, and an Application

AU - Ågotnes, Thomas

AU - Van Der Hoek, Wiebe

AU - Rodríguez-Aguilar, Juan A.

AU - Sierra, Carles

AU - Wooldridge, Michael

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

PY - 2009/6/1

Y1 - 2009/6/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?partnerID=yv4JPVwI&eid=2-s2.0-66049156538&md5=89562f8f171de60a12381231bd7000bd

U2 - 10.1007/s11225-009-9184-3

DO - 10.1007/s11225-009-9184-3

M3 - Article

AN - SCOPUS:66049156538

VL - 92

SP - 1

EP - 26

JO - Studia Logica

JF - Studia Logica

SN - 0039-3215

IS - 1

ER -

Ågotnes T, Van Der Hoek W, Rodríguez-Aguilar JA, Sierra C, Wooldridge M. Multi-Modal CTL: Completeness, Complexity, and an Application. Studia Logica. 2009 Jun 1;92(1):1-26. https://doi.org/10.1007/s11225-009-9184-3