Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T., Computer-aided verification, 1999. Manuscript.
Alur, R., Henzinger, T.A., ‘Reactive modules’, Formal Methods in System Design, 15(11): 7–48, 1999.
Alur, R., Henzinger, T.A., Kupferman, O., ‘Alternating-time temporal logic’, Journal of the ACM, 49(5): 672–713, 2002.
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.
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.
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.
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.
Brunel, J., Combining temporal and deontic logics. with an application to computer security, Ph.D. thesis, IRIT, Toulouse, France, 2007.
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.
Cheng, A., ‘Complexity results for model checking’, Tech. Rep. RS-95-18, BRICS, Department of Computer Science, University of Aarhus, 1995.
Clarke, E.M., Grumberg, O., Peled, D.A., Model Checking, The MIT Press, Cambridge, MA, 2000.
Dignum, F., ‘Autonomous agents with norms’, Artificial Intelligence and Law, 7: 69–79, 1999.
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.
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.
Francez, N., Fairness, Springer-Verlag, Berlin, Germany, 1986.
Harel, D., Kozen, D., Tiuryn, J., Dynamic Logic, The MIT Press, Cambridge, MA, 2000.
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.
van der Hoek, W., Roberts, M., Wooldridge, M., ‘Social laws in alternating time: Effectiveness, feasibility, and synthesis’, Synthese, 156(1): 1–19, 2007.
Lomuscio, A., Sergot, M., ‘Deontic interpreted systems’, Studia Logica, 75(1): 63–92, 2003.
Moses, Y., Tennenholtz, M., ‘Artificial social systems’, Computers and AI, 14(6): 533–562, 1995.
Prakken, H., Sergot, M., ‘Contrary-to-duty obligations’, Studia Logica 57(1): 91–115, 1996.
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.
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.
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.
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.
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.
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.
Shoham, Y., Tennenholtz, M., ‘On the emergence of social conventions: Modelling, analysis, and simulations’, Artificial Intelligence, 94(1–2): 139–166, 1997.
Stockmeyer, L.J., Chandra, A.K., ‘Provably difficult combinatorial games’, SIAM Journal of Computing, 8(2): 151–174, 1979.
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.
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Ågotnes, T., van der Hoek, W., Rodríguez-Aguilar, J.A., Sierra, C., Wooldridge, M. (2009). A Temporal Logic of Normative Systems. In: Makinson, D., Malinowski, J., Wansing, H. (eds) Towards Mathematical Philosophy. Trends in Logic, vol 28. Springer, Dordrecht. https://doi.org/10.1007/978-1-4020-9084-4_5
Download citation
DOI: https://doi.org/10.1007/978-1-4020-9084-4_5
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-9083-7
Online ISBN: 978-1-4020-9084-4
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)