A Temporal Logic of Normative Systems

  • Thomas ÅgotnesEmail author
  • Wiebe van der Hoek
  • Juan A. Rodríguez-Aguilar
  • Carles Sierra
  • Michael Wooldridge
Part of the Trends in Logic book series (TREN, volume 28)


We study Normative Temporal Logic (ntl), a formalism intended for reasoning about the temporal properties of normative systems. ntl is a generalisation of the well-known branching-time temporal logic ctl, in which the path quantifiers \({\mathsf{A}}\) (“on all paths…”) and \({\mathsf {E}}\) (“on some path…”) are replaced by the indexed deontic operators \({\mathsf{O}}_{\eta}\) (“it is obligatory in the context of the normative system η that …”) and \({\mathsf{P}}_{\eta}\) (“it is permissible in the context of the normative system η that…”). After introducing the logic, we give a sound and complete axiomatisation. We then present a symbolic representation language for normative systems, and we 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 a concrete interpretation for the normative systems named in formulae to be model checked. We show that the complexity of model checking varies from p-complete in the simplest case (explicit state model checking where we are given a specific interpretation for all normative systems in the formula) up to exptime-hard in the worst case (symbolic model checking, no interpretation given). We present examples to illustrate the use of ntl, and conclude with discussions of related work (in particular, the relationship of ntl to other deontic logics), and some issues for future work.


normative systems temporal logic multi-agent systems 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Alur, R., Henzinger, T., Computer-aided verification, 1999. Manuscript. Google Scholar
  2. [2]
    Alur, R., Henzinger, T.A., ‘Reactive modules’, Formal Methods in System Design, 15(11): 7–48, 1999. CrossRefGoogle Scholar
  3. [3]
    Alur, R., Henzinger, T.A., Kupferman, O., ‘Alternating-time temporal logic’, Journal of the ACM, 49(5): 672–713, 2002. CrossRefMathSciNetGoogle Scholar
  4. [4]
    Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Taşiran, S., ‘Mocha: Modularity in model checking’, in CAV 1998: Tenth International Conference on Computer-aided Verification, LNCS, vol. 1427, Springer-Verlag, Berlin, Germany, 1998, pp. 521–525. Google Scholar
  5. [5]
    Attie, Paul C., Allen Emerson, E., ‘Synthesis of concurrent systems with many similar processes’, ACM Transactions on Programming Languages and Systems, 20(1): 51–115, 1998. CrossRefGoogle Scholar
  6. [6]
    Broersen, J., ‘Strategic deontic temporal logic as a reduction to ATL, with an application to Chisholm’s scenario’, in Proceedings Eighth International Workshop on Deontic Logic in Computer Science (DEON’06), LNAI, vol. 4048, Springer, Berlin, 2006, pp. 53–68. Google Scholar
  7. [7]
    Broersen, J., Dignum, F., Dignum, V., Meyer, J.-J. Ch., ‘Designing a deontic logic of deadlines’, in Lomuscio, A., Nute, D. (eds.), Proceedings Seventh International Workshop on Deontic Logic in Computer Science (DEON’04), LNAI, vol. 3065, Springer, Berlin, 2004, pp. 43–56. Google Scholar
  8. [8]
    Brunel, J., Combining temporal and deontic logics. with an application to computer security, Ph.D. thesis, IRIT, Toulouse, France, 2007. Google Scholar
  9. [9]
    Carmo, Jose, Jones, Andrew J.I., ‘Deontic logic and contrary-to-duties’, in Gabbay, D.M., Guenthner, F. (eds.), Handbook of Philosophical Logic, 2nd edition, vol. 8, Kluwer Academic Publishers, Dordrecht, 2002, pp. 265–343. Google Scholar
  10. [10]
    Cheng, A., ‘Complexity results for model checking’, Tech. Rep. RS-95-18, BRICS, Department of Computer Science, University of Aarhus, 1995. Google Scholar
  11. [11]
    Clarke, E.M., Grumberg, O., Peled, D.A., Model Checking, The MIT Press, Cambridge, MA, 2000. Google Scholar
  12. [12]
    Dignum, F., ‘Autonomous agents with norms’, Artificial Intelligence and Law, 7: 69–79, 1999. CrossRefGoogle Scholar
  13. [13]
    Dignum, F., Broersen, J., Dignum, V., Meyer, J.-J. Ch., ‘Meeting the deadline: Whey, when and how’, in Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff C.A. (eds.), Formal Approaches to Agent-Based Systems, LNAI, vol. 3228, Springer, Berlin, 2004, pp. 30–40. Google Scholar
  14. [14]
    Emerson, E.A., ‘Temporal and modal logic’, in van Leeuwen J. (ed.), Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, Elsevier Science Publishers B.V., Amsterdam, The Netherlands, 1990, pp. 996–1072. Google Scholar
  15. [15]
    Francez, N., Fairness, Springer-Verlag, Berlin, Germany, 1986. zbMATHGoogle Scholar
  16. [16]
    Harel, D., Kozen, D., Tiuryn, J., Dynamic Logic, The MIT Press, Cambridge, MA, 2000. zbMATHGoogle Scholar
  17. [17]
    van der Hoek, W., Lomuscio, A., Wooldridge, M., ‘On the complexity of practical ATL model checking’, in Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS-2006), Hakodate, Japan, 2005, pp. 201–208. Google Scholar
  18. [18]
    van der Hoek, W., Roberts, M., Wooldridge, M., ‘Social laws in alternating time: Effectiveness, feasibility, and synthesis’, Synthese, 156(1): 1–19, 2007. zbMATHCrossRefMathSciNetGoogle Scholar
  19. [19]
    Lomuscio, A., Sergot, M., ‘Deontic interpreted systems’, Studia Logica, 75(1): 63–92, 2003. zbMATHCrossRefMathSciNetGoogle Scholar
  20. [20]
    Moses, Y., Tennenholtz, M., ‘Artificial social systems’, Computers and AI, 14(6): 533–562, 1995. MathSciNetGoogle Scholar
  21. [21]
    Prakken, H., Sergot, M., ‘Contrary-to-duty obligations’, Studia Logica 57(1): 91–115, 1996. zbMATHCrossRefMathSciNetGoogle Scholar
  22. [22]
    Schnoebelen, P., ‘The complexity of temporal logic model checking’, in Balbiani, P., Suzuki, N.-Y., Wolter, F., Zakharyascev, M. (eds.), Advances in Modal Logic, vol. 4, King’s College Publications, London, 2003, pp. 393–436. Google Scholar
  23. [23]
    Sergot, M., ‘Modelling unreliable and untrustworthy agent behaviour’, in Dunin-Keplicz, B., Jankowski, A., Skowron, A., Szczuka, M. (eds.), Monitoring, Security, and Rescue Techniques in Multiagent Systems, Advances in Soft Computing, Springer, Berlin, 2005, pp. 161–178. CrossRefGoogle Scholar
  24. [24]
    Sergot, M., Craven, R., ‘The deontic component of action language nC+’, in Goble, L., Meyer, J.-J. Ch. (eds.), Deontic Logic and Artificial Systems, Proc. 8th International Workshop on Deontic Logic in Computer Science, LNAI, 4048, Springer, Berlin, 2006, pp. 222–237. CrossRefGoogle Scholar
  25. [25]
    Shoham, Y., Tennenholtz, M., ‘Emergent conventions in multi-agent systems’, in Rich, C., Swartout, W., Nebel, B. (eds.), Proceedings of Knowledge Representation and Reasoning (KR&R-92), 1992, pp. 225–231. Google Scholar
  26. [26]
    Shoham, Y., Tennenholtz, M., ‘On the synthesis of useful social laws for artificial agent societies’, in Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92), San Diego, CA, 1992, pp. 276–281. Google Scholar
  27. [27]
    Shoham, Y., Tennenholtz, M., ‘On social laws for artificial agent societies: Off-line design’, in Agre, P.E., Rosenschein, S.J. (eds.), Computational Theories of Interaction and Agency, The MIT Press, Cambridge, MA, 1996, pp. 597–618. Google Scholar
  28. [28]
    Shoham, Y., Tennenholtz, M., ‘On the emergence of social conventions: Modelling, analysis, and simulations’, Artificial Intelligence, 94(1–2): 139–166, 1997. zbMATHCrossRefGoogle Scholar
  29. [29]
    Stockmeyer, L.J., Chandra, A.K., ‘Provably difficult combinatorial games’, SIAM Journal of Computing, 8(2): 151–174, 1979. zbMATHCrossRefMathSciNetGoogle Scholar
  30. [30]
    Wieringa, R.J., Meyer, J.-J.Ch., ‘Deontic logic in computer science’, in Meyer, J.-J.Ch., Wieringa, R.J. (eds.), Deontic Logic in Computer Science—Normative System Specification, John Wiley & Sons, New York, 1993, pp. 17–40. Google Scholar
  31. [31]
    Wooldridge, M., van der Hoek, W., ‘On obligations and normative ability: Towards a logical analysis of the social contract’, Journal of Applied Logic, 4(3–4): 396–420, 2005. CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  • Thomas Ågotnes
    • 1
    Email author
  • Wiebe van der Hoek
    • 2
  • Juan A. Rodríguez-Aguilar
    • 3
  • Carles Sierra
    • 3
  • Michael Wooldridge
    • 2
  1. 1.Bergen University CollegeBergenNorway
  2. 2.Department of Computer ScienceUniversity of LiverpoolLiverpoolUnited Kingdom
  3. 3.Spanish Council for Scientific Research — CSICArtificial Intelligence Research Institute — IIIABarcelonaSpain

Personalised recommendations