On the Logic of Normative Systems

Authors Thomas Ågotnes, Wiebe van der Hoek, Juan A. Rodriguez-Aguilar, Carles Sierra, Michael Wooldridge

Thumbnail PDF


  • Filesize: 220 kB
  • 13 pages

Document Identifiers

Author Details

Thomas Ågotnes
Wiebe van der Hoek
Juan A. Rodriguez-Aguilar
Carles Sierra
Michael Wooldridge

Cite AsGet BibTex

Thomas Ågotnes, Wiebe van der Hoek, Juan A. Rodriguez-Aguilar, Carles Sierra, and Michael Wooldridge. On the Logic of Normative Systems. In Normative Multi-agent Systems. Dagstuhl Seminar Proceedings, Volume 7122, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


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.
  • Normative systems
  • normative temporal logic
  • deontic logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail