Multi-Modal CTL: Completeness,Complexity, and an Application |
| |
Authors: | Thomas Ågotnes Wiebe Van der Hoek Juan A. Rodríguez-Aguilar Carles Sierra Michael Wooldridge |
| |
Affiliation: | (1) Department of Information Science and Media Studies, University of Bergen and Bergen University College, Bergen, Norway;(2) Compute Science Department, University of Liverpool, Liverpool, UK;(3) Artificial Intelligence Research Institute – IIIA, Spanish Council for Scientific Research – CSIC, Bellaterra, Spain |
| |
Abstract: | 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 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. Presented by Jacek Malinowski |
| |
Keywords: | Computation Tree Logic ( font-variant:small-caps" >ctl) Normative Systems Social Laws |
本文献已被 SpringerLink 等数据库收录! |
|