Norms have been widely enacted in human and agent societies to regulate individuals’ actions. However, although legislators may have ethics in mind when establishing norms, moral values are only sometimes explicitly considered. This paper advances the state of the art by providing a method for selecting the norms to enact within a society that best aligns with the moral values of such a society. Our approach to aligning norms and values is grounded in the ethics literature. Specifically, from the literature’s (...) study of the relations between norms, actions, and values, we formally define how actions and values relate through the so-called value judgment function and how norms and values relate through the so-called norm promotion function. We show that both functions provide the means to compute value alignment for a set of norms. Moreover, we detail how to cast our decision-making problem as an optimisation problem: finding the norms that maximise value alignment. We also show how to solve our problem using off-the-shelf optimisation tools. Finally, we illustrate our approach with a specific case study on the European Value Study. (shrink)

We define a multi-modal version of Computation Tree Logic (CTL) by extending the language with path quantifiers $E^\delta $ and $E^\delta $ 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. (shrink)

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. (shrink)