2026-07-21T23:57:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:921 2024-03-06T11:07:26Z ddc:004 open_access

On the Logic of Normative Systems Ågotnes, Thomas van der Hoek, Wiebe Rodriguez-Aguilar, Juan A. Sierra, Carles Wooldridge, Michael Normative systems normative temporal logic deontic logic We introduce emph{Normative Temporal Logic} (acro{ntl}), a logic for reasoning about normative systems. acro{ntl} is a generalisation of the well-known branching-time temporal logic acro{ctl}, in which the path quantifiers $Apath$ (``on all pathsldots'') and $Epath$ (``on some pathldots'') are replaced by the indexed deontic operators $O{ s}$ and $P{ s}$, where for example $O{ s}phi$ means ``$phi$ is obligatory in the context of normative system $ s$''. After defining the logic, we give a sound and complete axiomatisation, and discuss the logic's relationship to standard deontic logics. We present a symbolic representation language for models and normative systems, and identify four different model checking problems, corresponding to whether or not a model is represented symbolically or explicitly, and whether or not we are given an interpretation for the normative systems named in formulae to be checked. We show that the complexity of model checking varies from acro{p}-complete up to acro{exptime}-hard for these variations. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thomas Ågotnes and Wiebe van der Hoek and Juan A. Rodriguez-Aguilar and Carles Sierra and Michael Wooldridge 2007 Is Part Of Dagstuhl Seminar Proceedings, Volume 7122, Normative Multi-agent Systems (2007) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.07122.24 urn:nbn:de:0030-drops-9210 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07122.24 eng https://creativecommons.org/licenses/by/4.0/legalcode