# agentive_permissions_in_multiagent_systems__92f1a096.pdf

Agentive Permissions in Multiagent Systems

Qi Shi University of Southampton qi.shi@soton.ac.uk

This paper proposes to distinguish four forms of agentive permissions in multiagent settings. The main technical results are the complexity analysis of model checking, the semantic undefinability of modalities that capture these forms of permissions through each other, and a complete logical system capturing the interplay between these modalities.

1 Introduction

Imagine a large factory being built in a city on a river. The factory will dump a pollutant into the river. It is known that a small factory located in another city higher up the river already exists and can dump up to 60g/day of the same pollutant. Also, more than 100g/day of the pollutant dumped into the river combined by the two factories will kill the fish. Suppose that the large factory will dump 20g/day of the pollutant. Then, the total dumped amount by both factories will not exceed 80g/day no matter how much the other factory dumps and thus the fish in the river will survive for sure. In other words, the action that dumping 20g/day ensures the survival of the fish. On the contrary, if the large factory will dump 60g/day of the pollutant, then the fish will be killed once the other factory dumps more than 40g/day. That is to say, the action that dumping 60g/day does not ensure the survival of the fish. However, it still leaves the possibility for the fish to survive, e.g. when the other factory dumps no more than 40g/day. In this situation, we say that the action that dumping 60g/day admits of the survival of the fish. To ensure and to admit show two different types of agency of an action. The difference comes from that, in multiagent or nondeterministic settings, the effect of an action of one agent might be affected by the actions of other agents or the nondeterminacy. It is worth noting that, admitting is the dual of ensuring. To be specific, if an action of an agent ensures an outcome, then the action does not admit of the opposite outcome, and vice versa. It is easy to see that their meanings coincide in single-agent deterministic settings. In this paper, we consider the two types of agency together with permissions. Let us come back to the large factory. Sup-

The full version of this paper includes an appendix, which can be found at ar Xiv: 2404.17053.

pose the city government passes a regulation:

The factory is permitted to dump any amount of the pollutant as long as the fish is not killed.

This regulation can be interpreted in two ways corresponding to two types of agency. The first could be

any dumping amount that admits of the survival of the fish is permitted. (SA)

In this interpretation, the permitted dumping amount of the factory is any amount no more than 100g/day. As long as the factory follows this regulation, there is a chance for the fish to survive if the other factory dumps so little that the total dumped amount does not exceed 100g/day. The second interpretation of the regulation could be

any dumping amount that ensures the survival of the fish is permitted. (SE)

In this interpretation, the factory should not dump any amount over 40g/day and the fish cannot be killed as long as the factory follows the regulation, no matter how much of the pollutant is dumped by the other factory. The above two interpretations give the factory two different permissions. It is worth noting that, either of the permissions enables the factory to take any of the actions satisfying some criteria. In this paper, we call such permissions strong . Specifically, we refer to (SA) and (SE) as strong permission to admit and strong permission to ensure, respectively. Not all permissions are in the same form as strong permissions. Suppose that, instead of the city s regulation, the factory is under some contractual obligation. To satisfy this obligation, the factory has to dump at least 30g/day of the pollutant. In this case, not every amount that ensures/admits of the survival of the fish (e.g. 20g/day) is contractually permitted to be dumped. Nevertheless,

there is a permitted dumping amount that ensures the survival of the fish. (WE)

For example, 35g/day is a contractually permitted dumping amount that ensures the survival of the fish. Similarly, if the contractual obligation forces the factory to dump at least 50g/day of the pollutant, then no contractually permitted dumping amount ensures the survival of the fish. However,

there is a permitted dumping amount that admits of the survival of the fish. (WA)

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

In contrast to strong permissions, the above two permissions express the capability of the factory to achieve some statements with a permitted action. We call such permissions weak . Specifically, we refer to (WE) and (WA) as weak permission to ensure and weak permission to admit, respectively. As shown in Section 2, the terms strong permission and weak permission have already existed in the literature for decades [Raz, 1975; Royakkers, 1997; Governatori et al., 2013]. In Section 5, we show the consistency between how these terms are used in our paper and in the literature. However, as far as we see, we are the first to make a clear distinction between permission to ensure and permission to admit , which are agentive permissions specific to multiagent settings. We are also the first to cross-discuss both strong and weak agentive permissions in multiagent settings. In this paper, we discuss four forms of permissions in multiagent settings that generalise those expressed in statements (SA), (SE), (WE), and (WA). Our contribution is three-fold. First, we propose a formal semantics for the four corresponding modalities in multiagent transition systems (Section 3). We also consider the model-checking problem (Section 3.1) and the reduction to STIT logic and ATL (Section 3.2). Second, we prove these modalities are semantically undefinable through each other (Section 4). This contrasts to the fact that, when separated from permissions, ensuring and admitting are dual to each other. Third, we give a sound and complete logical system for the four modalities (Section 5 and Section 6). This reveals the interplay between the four forms of permissions and offers an efficient way for permission reasoning.

2 Literature Review and Notion Discussion Deontic logic [Mc Namara and van de Putte, 2022] is an appealing approach to solving AI ethics problems by enabling autonomous agents to comprehend and reason about their obligation, permission, and prohibition. It aims at translating the deontic statements in natural languages into logical propositions and building up a system for plausible deduction. Von Wright [1951] launched the active development of symbolic deontic logic from the analogies between normative and alethic modalities. Several follow-up works [Anderson, 1956; Prior, 1963] built up the Standard Deontic Logic (SDL), taking obligation as the basic modality and defining permission as the dual of obligation and prohibition as the obligation of the negation. Anderson [1967] and Kanger [1971] reduced this system by defining a propositional constant d for all (relative) normative demands are met . By this means, obligation (modality O) can be defined as O' := (d ! '), which is read as it is necessary that ' is true when all normative demands are met . As the dual of obligation, permission (modality P) is defined as P' := (d '), (1) which is read as it is possible that all normative demands are met and ' is true . In this way, the inference rule ' ! P' ! P (2)

is valid. The notion of permission that satisfies statement (2) is called weak permission. There are two well-known related paradoxes about weak permission:

(i) Ross s paradox [Ross, 1944]. The formula

P' ! P(' _ ) (3)

is valid by statement (2). However, in common sense, for a kid it is permitted to eat an apple is true but it is permitted to eat an apple or drink alcohol should be false, which contradicts statement (3). (ii) The free choice permission paradox [von Wright, 1968; Kamp, 1973]. According to linguistic intuition, if it is permitted to eat an apple or a banana , then both eating an apple and eating a banana should be permitted. This shows that disjunctive permission is treated as free choice permission, which means the formula

P(' _ ) ! P' P (4)

should be valid. However, statement (4) is not derivable in SDL. Free choice permission is a form of strong permission [Asher and Bonevac, 2005], satisfying the inference rule

' ! Ps ! Ps'. (5)

Following Anderson and Kanger s way, van Benthem [1979] captured the notion of strong permission as

Ps' = (' ! d), (6)

which is read as it is necessary that if ' is true then all normative demands are met . He then gave a complete axiom system for obligation (O) and strong permission (Ps). Most researchers agree that both weak and strong permission makes sense. As discussed by Lewis [1979], no universal comprehension of permission seems to exist. In general, weak permission is treated as the dual of obligation. Strong permission, as well as free choice permission, is more intractable and arouses more interesting discussions due to its anti-monotonic inference property in statement (5). For instance, Anglberger et al. [2015] adopted the notion of strong permission and defined a notion of obligation as the weakest form of (strong) permission. Wang and Wang [2023] axiomatised a logic of strong permission that satisfies some commonly desirable logical properties. Strong permission is also studied in defeasible logic [Asher and Bonevac, 2005; Governatori et al., 2013], which is believed to be able to capture the logical intuition about permission. The above discussion of permission applies possible-world semantics without specifically considering agents and their agency. However, it is noticed that two kinds of normative statements exist: the agentless norms that talk about states (e.g. it is permitted to eat an apple) and the agentive norms that talk about actions (e.g. John is permitted to eat an apple). The possible-world semantics cannot distinguish them. To fill the gap, Chisholm [1964] proposed a transfer from any agentive norm to an agentless norm. For instance, the statement agent a is permitted to do ' is transformed into it is permitted that agent a does ' . Some recent work [Kulicki and Trypuz, 2017; Kulicki et al., 2023] aimed at integrating the agentless and agentive norms in a unified logical frame. Things become more complicated when agents and their agency are incorporated. In the literature, STIT logic [Chellas, 1969; Belnap and Perloff, 1988; Belnap and Perloff,

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

1992] is used to express the agency. Horty and Belnap [1995] and Horty [2001, chapter 4] introduced a deontic STIT logic for ought-to-be and ought-to-do semantics, respectively. The former corresponds to the agentless obligations while the latter corresponds to the agentive obligations in STIT models. Horty [2001, chapter 3] further showed that the transfer proposed by Chisholm does not always work properly. Following Horty, van de Putte [2017] briefly discussed the dual of the ought-to-do obligation, which is the weak permission in deontic STIT logic, and then defined a form of free choice permission following statement (4). Although the agency is considered in deontic STIT logic, the distinction between to ensure and to admit is never discussed there. In the field of AI, there is a rising interest in applying deontic logic into agents planning: how to achieve a goal while complying with the deontic constraints [Pandˇzi c et al., 2022; Areces et al., 2023]. There is also some discussion of agents comprehending and reasoning norms [Arkoudas et al., 2005; Broersen and Ram ırez Abarca, 2018]. However, to the best of our knowledge, the agentive weak and strong permissions have never been cross-discussed before. In this paper, we consider both permission to ensure and permission to admit in both weak and strong forms that follow statements (1) and (6). In a word, we consider four forms of permissions as illustrated in statements (SA), (SE), (WE), and (WA). It is worth mentioning that, our formalisation has a connection with Horty s ought-to-do deontic STIT logic [Horty, 2001]. On the one hand, the notion ensure captures the same idea as see to it that in STIT logic. On the other hand, our formalisation can be seen as a reasonable reduction of Horty s formalisation. Specifically, Horty s approach is to, first, define a preference over the outcomes (i.e. histories in STIT models) of actions in the model, then, apply the dominance act utiliarianism to decide which actions are permitted (i.e. optimal in his work) in semantics, and, finally, define the ought-to-do obligation based on the permitted actions in semantics. In particular, an action in the STIT frame is the set of outcomes that may follow from the action. An action sees to it that ' if and only if ' is true in all the potential outcomes. Then, do ' is interpreted as seeing to it that ' . In this paper, we combine the first two steps of Horty s approach, directly defining the deontic constraints on actions in the model and then defining four forms of permissions in semantics. Note that, the definition of deontic notions is independent of the process that combines the first two steps in Horty s approach. In other words, our work in this paper can easily be transformed from action-based models into outcome-based models by recovering the step of deciding permitted actions based on preference over outcomes using dominance act utilitarianism. Moreover, we give a reduction of our semantics into STIT logic in Section 3.2.

3 Syntax and Semantics

In this section, we introduce the syntax and semantics of our logical system. Throughout the paper, unless stated otherwise, we assume a fixed set A of agents and a fixed nonempty set of propositional variables.

Definition 1. A transition system is a tuple (S, , D, M, ):

1. S is a (possibly empty) set of states; 2. = { s a}s2S,a2A is the action space, where s a is a nonempty set of actions available to agent a in state s; 3. D = {Ds a}s2S,a2A is the deontic constraints, where Ds a is a set of permitted actions and ? ( Ds a s a; 4. M = {Ms}s2S is the mechanism, where a relation Ms Q

a2A s a S satisfies the continuity condition: for each action profile δ 2 Q

a2A s a there is a state t 2 S such that (δ, t) 2 Ms; 5. (p) S for each propositional variable p. The continuity condition in item 4 above requires the existence of a next state t. We say that a transition system is deterministic if such state t is always unique. The language Φ of our logical system is defined by the following grammar:

' := p | ' | ' _ ' | WAa' | WEa' | SEa' | SAa',

where p is a propositional variable and a 2 A is an agent. Intuitively, we interpret WAa' as there is a permitted action of agent a that admits of ' , WEa' as there is a permitted action of agent a that ensures ' , SEa' as each action of agent a that ensures ' is permitted , and SAa' as each action of agent a that admits of ' is permitted . We assume that conjunction , implication !, and Boolean constants true > and false ? are defined in the usual way. Also, by V i n 'i and W

i n 'i we denote, respectively, the conjunction and the disjunction of the formulae '1, . . . 'n. As usual, we assume that the conjunction and the disjunction of an empty list are > and ?, respectively. Definition 2. For each transition system (S, , D, M, ), each state s 2 S, and each formula ' 2 Φ, the satisfaction relation s ' is defined recursively as follows: 1. s p, if s 2 (p); 2. s ', if s 1 '; 3. s ' _ , if s ' or s ; 4. s WAa', if (s, i) 6 a ' for some i 2 Ds a; 5. s WEa', if (s, i) a ' for some i 2 Ds a; 6. s SEa', if i 2 Ds a for each i such that (s, i) a '; 7. s SAa', if i 2 Ds a for each i such that (s, i) 6 a ', where the notation (s, i) a ' means that, for each tuple (δ, t) 2 Ms, if δa = i, then t '. Items 4 - 7 above capture the generalised notions of permissions in statements (WA), (WE), (SE), and (SA) in Section 1. Informally, (s, i) a ' means that that action i of agent a in state s ensures that ' is true in the next state. Accordingly, (s, i) 6 a ' means that action i of agent a in state s admits of the situation that ' is true in the next state. Observe that, if a transition system is deterministic and has only one agent a, then (s, i) 6 a ' if and only if (s, i) a '. Then, the next lemma follows from items 4 - 7 of Definition 2. Lemma 1. If set A contains only agent a, then for any formula ' 2 Φ and state s of a deterministic transition system, 1. s WAa' if and only if s WEa';

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

2. s SAa' if and only if s SEa'. Note that, in other cases (i.e. multiagent or nondeterministic systems), these modalities are not only semantically inequivalent but also undefinable through each other. We show this in Section 4.

3.1 Model Checking Following Definition 2, we consider the global modelchecking problem [M uller-Olm et al., 1999] of language Φ. For a finite transition system and a formula ' 2 Φ, the global model checking determines the truth set J'K that consists of all states satisfying ' in the transition system. Formally, we define the truth set of a formula as follows. Definition 3. For any given transition system and any formula ' 2 Φ, the truth set J'K is the set {s | s '}. The global model checking of formula ' applies a trivial recursive process on its structural complexity. The next theorem shows its time complexity. See Appendix A of the full version [Shi, 2024] for a detailed analysis of the algorithm. Theorem 1 (time complexity). For a finite transition system (S, , D, M, ) and a formula ' 2 Φ, the time complexity of global model checking is O $ |'| (|S|+|M|+| |) % , where |'| is the size of the formula, |S| is the number of states, |M| = P

s2S |Ms| is the size of the mechanism, and | | = P

s2S | s a| is the size of the action space.

3.2 Reduction to Other Logics Recall statements (1) and (6) in Section 2, which show the way how Anderson and Kanger reduces SDL. Using a similar technique, we can translate our modalities into modalities in STIT logic and ATL [Alur et al., 2002] after properly interpreting the transition system in Definition 1. Reduction to STIT Instead of being about the states, the statements in STIT logic are about moment-history (m/h) pairs. Due to this fact, there is no exact reduction of our logic to STIT logic. However, we can interpret our modalities in STIT models in the appearance of the necessity and possibility modalities and 1. In order to do this, we first incorporate the deontic constraints into the models as atomic propositions. To be specific, m/h da represents that the action of agent a at moment m that includes history h is permitted. We use the modality XSTIT [Broersen, 2008; Broersen, 2011]. Informally, m/h XSTITa' could be interpreted as the action of agent a at moment m that includes history h sees to it that ' is true at the next moment . Then, our four modalities can be translated as: WAa' := (da XSTITa '); WEa' := (da XSTITa'); SEa' := (XSTITa' ! da); SAa' := ( XSTITa ' ! da).

Reduction to ATL Unlike in STIT logic, in ATL, the statements are about states but there is no way to express the properties of actions. For this reason, we encode deontic constraints into the states. To do this, we expand each state in

1m/h ' iff m/h0 ' for each history h0 such that m 2 h0.

our original transition system into a set of states in the ATL model. Specifically, each state s in our original transition system corresponds to a set {hs, Di | D A} of states in the ATL model. Informally, the tuple hs, Di encodes the information that state s is reached after the agents in set D taking permitted actions and the others taking non-permitted actions . Then, hs, Di da if and only if a 2 D. Also, hs, Di p if and only if s p in our original transition system. Correspondingly, the transition (hs, i, ht, Di) exists in the ATL model if there is a tuple (δ, t) 2 Ms in our original transition system such that D = {a 2 A | δa 2 Ds a} and is a wildcard. Note that, ATL requires the transitions to be deterministic. Thus, if needed, we incorporate a dummy agent Nature into the agent set A to achieve determinacy. Then, we can translate our modalities into standard ATL syntax as: WAa' := hh Aii X(da '); WEa' := hhaii X(da '); SEa' := hhaii X (' ! da); SAa' := hh Aii X (' ! da), where hh Cii X' is informally interpreted as the agents in set C can cooperate to enforce ' in the next state and hhaii is the abbreviation for hh{a}ii.

4 Mutual Undefinability As we define four modalities in the language, we would like to figure out if all of them are necessary to express the corresponding notions of permission. Specifically, if some of these modalities are semantically definable through the others, then the definable ones are not necessary for the language. As an example, a well-known result in Boolean logic is De Morgan s laws, which say conjunction and disjunction are interdefinable in the presence of negation. Therefore, to consider a minimal system for propositional logic, it is not necessary to include both conjunction and disjunction. In this section, we consider the definability of modalities in the same way as De Morgan s laws (i.e. semantical equivalence). For example, modality WA is definable through modalities WE, SE, and SA if every formula in language Φ is semantically equivalent to a formula using only modalities WE, SE, and SA. Formally, in the transition systems, we define semantical equivalence as follows. Definition 4. Formulae ' and are semantically equivalent if J'K = J K for each transition system. We prove that none of the modalities WA, WE, SE, and SA is definable through the other three. To do this, it suffices to show that, for each modality of the four modalities, there exists a formula ' 2 Φ and a transition system where J 'K 6= J K for each formula not using modality . In particular, we use the truth set algebra technique [Knight et al., 2022]. This technique uses one model (i.e. transition system) and shows that, in this model, the truth sets of all formulae not using modality form a proper subset of the family of all truth sets in language Φ, while the truth set of the formula ' does not belong to this subset. We formally state the undefinability results in the next theorem. A detailed explanation of the technique and proof can be found in Appendix B of the full version.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

Theorem 2 (undefinability of WA). The formula WAap is not semantically equivalent to any formula in language Φ that does not use modality WA. The formal statements of the undefinability results for modalities WE, SE, and SA are the same as Theorem 2 except for using the corresponding modalities instead of WA, see Theorem 5, Theorem 6, and Theorem 7 in Appendix B of the full version. Note that, all four undefinability results, as presented in Appendix B of the full version, require that our language contains at least two agents. In single-agent settings, if a transition system is nondeterministic, these undefinability results still hold. This can be observed by modifying the two-agent transition systems in the proofs into single-agent nondeterministic transition systems by treating one of the agents as the nondeterministic factor. If a single-agent transition system is deterministic, then, as observed in Lemma 1, modalities WA and WE are semantically equivalent, so as modalities SE and SA. However, modalities WA (WE) and SA (SE) are not definable through each other, see Appendix B.5 of the full version.

5 Axioms In addition to the tautologies in language Φ, our logical system contains the following schemes of axioms for all agents a, b 2 A and all formulae ', 2 Φ:

A1. WAa?; A2. WEa>; A3. SAa?; A4. SEa> ! SAa>; A5. WAa(' _ ) ! WAa' _ WAa ; A6. SAa' SAa ! SAa(' _ ); A7. WEa' WEa ! WAa(' ); A8. SEa' SEa ! SAa(' ); A9. WAa' SAa ! WAb(' ) SAb(' ).

Axiom A1 says agent a does not have a permitted action that has no next state. This is true because of the continuity property of the mechanism (item 4 of Definition 1). Axiom A2 says agent a always has a permitted action that ensures a next state. This is true because of the continuity property and the nonempty set of permitted actions (item 3 of Definition 1). Axiom A3 says every action that may have no next state is permitted. This is true because no such actions exist again due to the continuity property. Axiom A4 is true because both SEa> and SAa> mean that every action of agent a is permitted. Axiom A5 says, if agent a has a permitted action that admits of ' _ , then agent a either has a permitted action that admits of ' or has a permitted action that admits of . This is true because the permitted action that admits of ' _ indeed either admits of ' or admits of (item 3 of Definition 2). Axiom A6 says, if every action of agent a that admits of ' is permitted and every action of agent a that admits of is permitted, then every action of agent a that admits of '_ is permitted. This is true because any action that admits of '_ either admits of ' or admits of (item 3 of Definition 2).

Axiom A7 says, if agent a has a permitted action that ensures ' and has no permitted action that ensures , then agent a has a permitted action that admits of ' . This is true because the permitted action i that ensures ' does not ensure . Hence, action i admits of while ' is ensured to happen. Axiom A8 says, if agent a has a non-permitted action that ensures ' and every action that ensures is permitted, then agent a has a non-permitted action that admits of ' . This is true because the non-permitted action j that ensures ' does not ensure . Hence, action j admits of while ' is ensured to happen. Axiom A9 says, if agent a has no permitted action that admits of ' and every action that admits of is permitted, then agent b has no permitted action that admits of ' and every action of agent b that admits of ' is permitted. This is true because the antecedent means agent a s permitted actions ensure ' and non-permitted actions (if existing) ensure . Thus, every action of agent a ensures ' _ (item 3 of Definition 2). Hence, (' ) is unavoidable in the next state. This implies that agent b has no permitted action that admits of ' , and any action of agent b that admits of ' is permitted because no such action of agent b exists. We write ' and say that formula ' is a theorem of our logical system if it can be derived from the axioms using the following four inference rules:

IR1. ' , ' ! (Modus Ponens);

IR2. ' ! WAa' ! WAa ;

IR3. ' ! SAa ! SAa';

IR4. '1 'm ! 1 _ _ n WEa1'1 WEam'm ! SEb1 1 _ _ SEbn n ,

where agents a1, . . . , am, b1, . . . , bn are distinct. Rule IR2 is the monotonicity rule for modality WA. It is valid because, in each state of each transition system, the permitted action of agent a that admits of ' also admits of , as ' ! is universally true. By this rule, modality WA represents a form of weak permission following statement (2). Rule IR3 is the anti-monotonicity rule for modality SA. It is valid because, in each state of each transition system, the set of actions that admits of is a superset of the set of actions that admits of ', as ' ! is universally true. Hence, as long as the actions in the former set are all permitted, those in the latter set are also permitted. This rule shows that modality SA represents a form of strong permission following statement (5). It can be derived that modality WE represents a form of weak permission and modality SE represents a form of strong permission, see Appendix C.1 of the full version. Rule IR4 is a conflict-preventing rule following the notion of ensure in semantics. The premise says, if every one of '1, . . . , 'm is true, then at least one of 1, . . . , n is false. The conclusion says, for a set of distinct agents {a1, . . . , am, b1, . . . , bn} A, if every agent ai has a permitted action to ensure 'i, then for at least one agent bj, every action that ensures j is permitted. This is valid because there would be a conflict otherwise. To be specific, if there is

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

a state s where the conclusion of the rule is false, then, each agent ai has a permitted action ki that ensures 'i and each agent bj has a non-permitted action j that ensures j. Consider an action profile δ such that δai = ki for each i m and δbj = j for each j n. By the continuity condition in item 4 of Definition 1, there is a state t such that (δ, t) 2 Ms. In such state t, each of the formulae '1, . . . , 'm, 1, . . . , n is true. However, this conflicts with the premise of the rule. We write X ' if a formula ' can be derived from the theorems of our logical system and an additional set of assumptions X using only the Modus Ponens rule. Note that statements ? ' and ' are equivalent. We say that a set of formulae X is consistent if X 0 ?.

Lemma 2 (deduction). If X, ' , then X ' ! .

See the proof of Lemma 2 in Appendix C.2 of the full version.

Lemma 3 (Lindenbaum). Any consistent set of formulae can be extended to a maximal consistent set of formulae.

The standard proof of this lemma can be found in [Mendelson, 2009, Proposition 2.14].

Lemma 4. WEa' WAa ! WEa(' ).

Lemma 5. SEa' SAa ! SEa(' ).

See the proofs of the above two lemmas in Appendix C.3 of the full version. The next theorem follows from the above discussion of the axioms and the inference rules.

Theorem 3 (soundness). If ', then s ' for each state s of each transition system.

6 Completeness

In this section, we prove the strong completeness of our logical system. As usual, at the core of the completeness theorem is the canonical model construction. In our case, it is a canonical transition system.

6.1 Canonical Transition System In this subsection, we define the canonical transition system (S, , D, M, ).

Definition 5. Set S of states is the family of all maximal consistent subsets of our language Φ.

For each formula ' 2 Φ, we introduce two actions: a permitted action '+ and a non-permitted action ' . Formally, by '+ and ' we mean the pairs (', +) and (', ), respectively. By item 7 of Definition 2, the formula SAa> expresses that agent a is permitted to use every action. In other words, if SAa> is true, then there are no non-permitted actions available to agent a in the current state. This explains the intuition behind the following definition.

Definition 6. For each state s 2 S and each agent a 2 A,

s a = {'+ | ' 2 Φ}, if SAa> 2 s, {'+, ' | ' 2 Φ}, otherwise;

Ds a = {'+ | ' 2 Φ}.

The next definition is the key part of the canonical transition system construction. It specifies the mechanism of the transition system. Recall that WAa' means that agent a is

not permitted to use any action that admits of '. Hence, each permitted action of a must ensure '. We capture this rule in item 1 of the definition below. Recall that WEa' means that agent a has at least one permitted action that ensures '. In the canonical transition system, this action is defined to be '+. The rule captured in item 2 below guarantees ' in the next state whenever agent a uses action '+. Next, SEa' means that agent a is not permitted to use at least one action that ensures '. We denote such action by ' . The rule captured by item 3 stipulates that action ' ensures '. Finally, SAa' means that agent a is permitted to use all actions that admit of '. In other words, SAa' means that all non-permitted actions ensure '. This is captured by item 4 below. Definition 7. (δ, t) 2 Ms when for each agent a 2 A and each formula ' 2 Φ, 1. if δa 2 Ds a and WAa' /2 s, then ' 2 t; 2. if δa = '+ and WEa' 2 s, then ' 2 t; 3. if δa = ' and SEa' /2 s, then ' 2 t; 4. if δa 2 s a \ Ds a and SAa' 2 s, then ' 2 t. Note that, each state s is a maximal consistent set by Defintion 5. Hence, for item 1 above, the statement WAa' /2 s is equivalent to WAa' 2 s. The same goes for item 3. Definition 8. (p) = {s 2 S | p 2 s} for each p. This concludes the definition of the canonical transition system (S, , D, M, ). Next, we show that it satisfies the continuity condition in item 4 of Definition 1. Lemma 6 (continuity). For each state s 2 S and each action profile δ 2 Q

a2A s a, there is a state t such that (δ, t) 2 Ms.

Proof. Consider a partition {A, B} of the set A of agents:

A = {a 2 A | δa 2 Ds a}; (7) B = {b 2 A | δb 2 s b \ Ds b}. (8)

Then, SAb> /2 s for each agent b 2 B by Definitions 6. Hence, SAb> 2 s for each agent b 2 B because s is a maximal consistent set. Then, by the contrapositive of axiom A4,

SEb> 2 s. (9)

Consider the set of formulae X ={ | 9 a 2 A ( WAa 2 s)}

[ {σ | 9 a 2 A (δa = σ+, WEaσ 2 s)} [ { χ | 9 b 2 B (SAbχ 2 s)}

[ { | 9 b 2 B (δb = , SEb 2 s)}.

Claim 1. Set X is consistent.

Proof of Claim. Suppose the opposite. Then, by axiom A2, statements (9) and (10), there are formulae

WAa1 11, . . . , WAa1 1k1, WEa1bσ1 2 s, WAam m1, . . . , WAam mkm, WEambσm 2 s, (11)

and SAb1χ11, . . . , SAb1χ1 1, SEb1b 1 2 s, SAbnχn1, . . . , SAbnχn n, SEbnb n 2 s, (12)

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

a1, . . . , am, b1, . . . , bn are distinct agents, (13)

bσi = σi, if δai = σ+ i and WEaiσi 2 s, >, otherwise,

for each i m, and

b i = i, if δbi = i and SEbi i 2 s, >, otherwise,

for each i n, such that

j i χij ?. (14)

By multiple application of the countrapositive of axiom A5 and propositional reasoning, statement (11) implies that

j ki ij for each i m. (15)

Note that, in the specific case where ki = 0, statement (15) follows directly from axiom A1. By Lemma 4, statement (15) and the part WEaibσi 2 s of statement (11) imply

s WEai bσi _

j ki ij for each i m. (16)

Meanwhile, by multiple application of Lemma 2 and propositional reasoning, statement (14) can be reformulated to

j ki ij ! _

j i χij . (17)

By statement (13) and rule IR4, statement (17) implies

i m WEai bσi _

j ki ij ! _

i n SEbi b i

Then, by statement (16) and the Modus Ponens rule,

i n SEbi b i _

j i χij . (18)

At the same time, by multiple application of axiom A6 and propositional reasoning, statement (12) implies

j i χij for each i n. (19)

Note that, in the specific case where i = 0, statement (19) follows directly from axiom A3. By Lemma 5, statement (19) and the part SEbib i 2 s of statement (12) imply

s SEbi b i _

j i χij for each i n,

which contradicts statement (18).

Let t be any maximal consistent extension of set X. By Lemma 3, such t must exist. Hence, t 2 S by Definition 5.

Claim 2. (δ, t) 2 Ms.

Proof of Claim. It suffices to verify that conditions 1 4 of Definition 7 are satisfied for the tuple (δ, t) for each agent x 2 A. Recall that sets A and B form a partition of the agent set A. Hence, it suffices to consider the following two cases. Case 1: x 2 A. Condition 1 of Definition 7 follows from line 1 of statement (10) because X t. Condition 2 follows from line 2 of statement (10). Conditions 3 and 4 trivially follow from δx 2 Ds x by statement (7). Case 2: x 2 B. Conditions 1 and 2 of Definition 7 trivially follow from δx /2 Ds x by statement (8). Condition 3 follows from line 4 of statement (10) because X t. Condition 4 follows from line 3 of statement (10).

The statement of this lemma follows from Claim 2.

6.2 Strong Completeness Theorem As usual, at the core of the proof of completeness is a truth lemma proven by induction on the structural complexity of a formula. In our case, it is the Lemma 7. The completeness result, as shown in Theorem 4, is proved with Lemma 7 in the standard way. We put the formal proofs in Appendix D of the full version. Lemma 7. s ' if and only if ' 2 s for each state s of the canonical transition system and each formula ' 2 Φ. Theorem 4 (strong completeness). For each set of formulae X Φ and each formula ' 2 Φ such that X 0 ', there is a state s of a transition system such that s χ for each χ 2 X and s 1 '.

7 Conclusion and Future Research We are the first to classify the agentive permissions in multiagent settings into permissions to ensure and permissions to admit and cross-discuss them in both weak and strong forms. To do this, we propose and formalise four forms of agentive permissions in multiagent transition systems, analyse the time complexity of the model checking algorithm, prove their semantical undefinability through each other, and give a sound and complete logical system that reveals their interplay. Future research could be in two directions. One is to extend the deontic constraints from one-step actions to multi-step actions. Indeed, multi-step deontic constraints are commonly seen in application scenarios. For example, if a child is permitted to eat only one ice cream per day, then whether to eat an ice cream in the morning affects whether she is permitted to eat one in the afternoon. This is closely related to conditional norms (e.g. conditional obligations) discussed in the literature [van Fraassen, 1973; Chellas, 1974; De Cew, 1981; Rulli, 2020] but is interpreted in multiagent transition systems instead of possible-world semantics. The other direction could be the interaction between permission and responsibility in multiagent settings. It might have been noticed that our introductory example about factories and fish is a variant of [Halpern, 2015, Example 3.11] and [Halpern, 2016, Example 6.2.5], which talk about causality and responsibility in multiagent settings. Indeed, the connection between obligation and responsibility in linguistic intuition has already been noticed by philosophers [van de Poel, 2011]. However, a formal investigation of the interaction among norm, causation, and responsibility in multiagent settings is still lacking.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

Acknowledgements

I would like to express my sincere gratitude to Dr. Pavel Naumov, my Ph D supervisor, for his selfless help in completing this paper. The research is funded by the China Scholarship Council (CSC No.202206070014).

[Alur et al., 2002] Rajeev Alur, Thomas A Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672 713, 2002.

[Anderson, 1956] Alan Ross Anderson. The formal analysis of normative systems. Technical report, Office of Naval Research, 1956.

[Anderson, 1967] Alan Ross Anderson. Some nasty problems in the formal logic of ethics. Noˆus, pages 345 360, 1967.

[Anglberger et al., 2015] Albert JJ Anglberger, Nobert Gratzl, and Olivier Roy. Obligation, free choice, and the logic of weakest permissions. The Review of Symbolic Logic, 8(4):807 827, 2015.

[Areces et al., 2023] Carlos Areces, Valentin Cassano, Pablo F Castro, Raul Fervari, and Andr es R Saravia. A deontic logic of knowingly complying. In Proceedings of the 22nd International Conference on Autonomous Agents and Multi Agent Systems, volume 23, 2023.

[Arkoudas et al., 2005] Konstantine Arkoudas, Selmer Bringsjord, and Paul Bello. Toward ethical robots via mechanized deontic logic. In AAAI Fall Symposium on Machine Ethics, pages 17 23. The AAAI Press Menlo Park, CA, USA, 2005.

[Asher and Bonevac, 2005] Nicholas Asher and Daniel Bonevac. Free choice permission is strong permission. Synthese, 145:303 323, 2005.

[Belnap and Perloff, 1988] Nuel Belnap and Michael Perloff. Seeing to it that: a canonical form for agentives. Theoria, 54(3):175 199, 1988.

[Belnap and Perloff, 1992] Nuel Belnap and Michael Perloff. The way of the agent. Studia Logica, pages 463 484, 1992. [Broersen and Ram ırez Abarca, 2018] Jan Broersen and Aldo Iv an Ram ırez Abarca. Formalising oughts and practical knowledge without resorting to action types. In Proceedings of the 17th International Conference on Autonomous Agents and Multi Agent Systems, pages 1877 1879, 2018.

[Broersen, 2008] Jan Broersen. A complete STIT logic for knowledge and action, and some of its applications. In Proceedings of the 6th International Workshop on Declarative Agent Languages and Technologies, pages 47 59. Springer, 2008.

[Broersen, 2011] Jan Broersen. Deontic epistemic STIT logic distinguishing modes of mens rea. Journal of Applied Logic, 9(2):137 152, 2011.

[Chellas, 1969] Brian Farrell Chellas. The logical form of imperatives. Stanford University, 1969. [Chellas, 1974] Brian F Chellas. Conditional obligation. In Logical Theory and Semantic Analysis: Essays Dedicated to Stig Kanger on His Fiftieth Birthday, pages 23 33. Springer, 1974. [Chisholm, 1964] Roderick M Chisholm. The ethics of requirement. American Philosophical Quarterly, 1(2):147 153, 1964. [De Cew, 1981] Judith Wagner De Cew. Conditional obligation and counterfactuals. Journal of Philosophical Logic, pages 55 72, 1981. [Governatori et al., 2013] Guido Governatori, Francesco Olivieri, Antonino Rotolo, and Simone Scannapieco. Computing strong and weak permissions in defeasible logic. Journal of Philosophical Logic, 42:799 829, 2013. [Halpern, 2015] Joseph Y Halpern. A modification of the halpern-pearl definition of causality. In Proceedings of the 24th International Conference on Artificial Intelligence, pages 3022 3033, 2015. [Halpern, 2016] Joseph Y Halpern. Actual causality. MIT Press, 2016. [Horty and Belnap, 1995] John F Horty and Nuel Belnap. The deliberative STIT: a study of action, omission, ability, and obligation. Journal of Philosophical Logic, 24(6):583 644, 1995. [Horty, 2001] John F Horty. Agency and Deontic Logic. Oxford University Press, 2001. [Kamp, 1973] Hans Kamp. Free choice permission. In Proceedings of the Aristotelian Society, volume 74, pages 57 74. JSTOR, 1973. [Kanger, 1971] Stig Kanger. New Foundations for Ethical Theory. Springer, 1971. [Knight et al., 2022] Sophia Knight, Pavel Naumov, Qi Shi, and Vigasan Suntharraj. Truth set algebra: a new way to prove undefinability. ar Xiv:2208.04422, 2022. [Kulicki and Trypuz, 2017] Piotr Kulicki and Robert Trypuz. Connecting actions and states in deontic logic. Studia Logica, 105:915 942, 2017. [Kulicki et al., 2023] Piotr Kulicki, Robert Trypuz, Robert Craven, and Marek J Sergot. A unified logical framework for reasoning about deontic properties of actions and states. Logic and Logical Philosophy, pages 1 35, 2023. [Lewis, 1979] David Lewis. A problem about permission. In Essays in Honour of Jaakko Hintikka, pages 163 175. Springer, 1979. [Mc Namara and van de Putte, 2022] Paul Mc Namara and Frederik van de Putte. Deontic logic. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, 2022. [Mendelson, 2009] Elliott Mendelson. Introduction to Mathematical Logic. CRC press, 2009.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

[M uller-Olm et al., 1999] Markus M uller-Olm, David Schmidt, and Bernhard Steffen. Model-checking: a tutorial introduction. In Static Analysis: Proceedings of the 6th International Symposium, pages 330 354. Springer, 1999. [Pandˇzi c et al., 2022] Stipe Pandˇzi c, Jan Broersen, and Henk Aarts. Boid*: autonomous goal deliberation through abduction. In Proceedings of the 21st International Conference on Autonomous Agents and Multi Agent Systems, pages 1019 1027, 2022. [Prior, 1963] Arthur N Prior. The logic of modality. In Formal Logic, pages 186 229. Oxford University Press, 1963. [Raz, 1975] Joseph Raz. Permissions and supererogation. American Philosophical Quarterly, 12(2):161 168, 1975. [Ross, 1944] Alf Ross. Imperatives and logic. Philosophy of Science, 11(1):30 46, 1944. [Royakkers, 1997] Lamber MM Royakkers. Giving permission implies giving choice. In Proceedings of the 8th International Conference on Database and Expert Systems Applications, pages 198 203. IEEE, 1997. [Rulli, 2020] Tina Rulli. Conditional obligations. Social Theory and Practice, pages 365 390, 2020. [Shi, 2024] Qi Shi. Agentive permissions in multiagent systems. ar Xiv:2404.17053, 2024. [van Benthem, 1979] Johan van Benthem. Minimal deontic logics. Bulletin of the Section of Logic, 8(1):36 42, 1979. [van de Poel, 2011] Ibo van de Poel. The relation between forward-looking and backward-looking responsibility. In Moral Responsibility: Beyond Free Will and Determinism, pages 37 52. Springer, 2011. [van de Putte, 2017] Frederik van de Putte. Free choice permission in STIT. In Logica yearbook 2016, pages 289 303. College Publications, 2017. [van Fraassen, 1973] Bas C van Fraassen. The logic of conditional obligation. In Exact Philosophy, pages 151 172. Springer, 1973. [von Wright, 1951] Georg Henrik von Wright. Deontic logic. Mind, 60(237):1 15, 1951. [von Wright, 1968] Georg Henrik von Wright. An Essay in Deontic Logic and the General Theory of Action: With a Bibliography of Deontic and Imperative Logic. North Holland Pub. Co, 1968. [Wang and Wang, 2023] Zilu Wang and Yanjing Wang. Strong permission bundled: first steps. In Proceedings of the 16th International Conference on Deontic Logic and Normative Systems, pages 217 234. Springer, 2023.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)