# a_computationally_grounded_logic_of_seeingtoitthat__630eb4d5.pdf

A Computationally Grounded Logic of Seeing-to-it-that

Andreas Herzig1 , Emiliano Lorini1 and Elise Perrotin2

1IRIT, CNRS, Toulouse, France 2CRIL, CNRS, Lens, France {Andreas.Herzig,Emiliano.Lorini}@irit.fr, elise.perrotin@cril.fr

We introduce a simple model of agency that is based on the concepts of control and attempt. Both relate agents and propositional variables. Moreover, they can be nested: an agent i may control whether another agent j controls a propositional variable p; i may control whether j attempts to change p; i may attempt to change whether j controls p; i may attempt to change whether j attempts to change p; and so on. In this framework we define several modal operators of time and agency: the LTL operators on the one hand, and the Chellas and the deliberative stit operator on the other. While in the standard stit framework the model checking problem is unfeasible because its models are infinite, in our framework models are represented in a finite and compact way: they are grounded on the primitive concepts of control and attempt. This makes model checking practically feasible. We prove its PSPACE-completeness and we show how the concept of social influence can be captured.

1 Introduction One of the most prominent accounts of agency is Belnap and Horty s logical analysis of agent i sees to it that proposition ϕ is true in terms of branching time + agent choice models (BT+AC models) [Horty and Belnap, 1995; Horty, 2001]. At the core of this so-called stit logic are the Chellas stit operator, expressing the ability of a group of agents to ensure that a given formula is true regardless of the choices of other agents, and the deliberative stit operator, adding that truth of this formula is not necessary. This framework is very expressive and was put to work to account for other action-based concepts such as obligation [Horty, 2001; Broersen, 2011], influence [Lorini and Sartor, 2016], social commitment [Lorini, 2013] and responsibility [Lorini et al., 2014]. Unfortunately reasoning turned out to be hard: deciding satisfiability of formulas involving the Chellas or the deliberative stit operator is NEXPTIME-complete even without temporal modalities as soon as there is more than one agent [Balbiani et al., 2008]; it becomes 2EXPTIME-complete with temporal modalities next and until [Boudou and Lorini, 2018]; and it is undecidable as soon as agency of sets of

agents (groups) comes into play, and so again already without temporal modalities [Herzig and Schwarzentruber, 2008]. On the other hand, model checking which is often considered to be an interesting alternative to satisfiability checking [Halpern and Vardi, 1991] is basically unfeasible because BT+AC models are typically infinite. We here propose to encode BT+AC models in a finite and compact way, so that model checking becomes practically feasible. We do so by grounding the basic concepts of stit logics, namely histories and choices, on the concepts of control and attempt. The former is borrowed from [van der Hoek et al., 2011; Herzig et al., 2011] while the latter is borrowed from [Lorini and Herzig, 2008]. Both relate agents and propositional variables: when an agent i controls a propositional variable p then she is able to determine the truth value of p at the next state; if this is the case and i attempts to change p then the truth value of p gets flipped at the next state; and if nobody is able and attempting to change the truth value of p then it remains unchanged. We follow van der Hoek [2011] whose states are not just valuations of classical propositional logic (sets of propositional variables), but come equipped with a function associating to each propositional variable the agent controlling it. We basically augment these models by a function associating to each propositional variable the set of agents attempting to change it. States are therefore triples, and each triple determines a unique next state: all those variables whose change is attempted by some agent controlling it get their truth value flipped, and the other variables keep their truth value. Attempts are naturally viewed as persistent goals: agents abandon the attempt to change p once p has been successfully changed (possibly by somebody else). Representing control and attempts in this way only allows for reasoning about the next state: as control does not change, attempts that fail at the first step will always fail, and new attempts cannot appear from one state to the next. We go beyond this simple model and introduce higher-order control and attempt: for two (possibly identical) agents i and j: i may control whether j controls a propositional variable p; i may control whether j attempts to change p; i may attempt to change whether j controls p; and i may attempt to change whether j attempts to change p. This allows us to reason about future states beyond the next state: we can define meaningful temporal operators of Linear-time Temporal

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)

Logic (LTL). In these models we interpret modal operators of agency of the kind group J achieves ϕ : we define a Chellas stit operator and a deliberative stit operator. For the resulting logic we establish PSPACE completeness of model checking. The paper is organised as follows. In Section 2 we introduce the models and in Section 3 language and semantics of our logic of agency based on control and attempt (LACA). In Section 4 we show that they correspond to particular BT+AC models. Section 5 establishes complexity of model checking. Section 6 illustrates LACA by recasting the definition of social influence of [Lorini and Sartor, 2016]. Section 7 concludes.

2 Models of Control and Attempt

We define the models of the logic of agency based on control and attempt LACA. Let Agt = {1, . . . , card(Agt)} be a finite set of agent names, typically noted i, j,. ..Groups are subsets of Agt, typically noted J, J ,. .. The complement of J is J = Agt \ J. We write i instead of {i}.

2.1 Atoms and Valuations

Let Prp be a set of propositional variables, or facts, typically noted p, q,. .. Atomic formulas, or atoms for short, follow the grammar α ::= p | ciα | tiα,

where p ranges over Prp and i over Agt. ciα reads agent i controls α and tiα reads agent i attempts to act on α , or agent i attempts to change the truth value of α . Atoms are therefore sequences of ci and ti that are followed by a propositional variable: the variable the atom is about. Atoms of the form ciα are control atoms and atoms of the form tiα are attempt atoms. The set of all atoms is noted Atm. States are simply valuations over atoms: subsets of the set Atm of atoms, noted V , V , etc. If α V then α is true at V , and if α / V then α is false at V . When tiα is false then i is indifferent about the value of p (as opposed to i wanting to maintain the truth value of p). We say that V and V agree on α if α has the same status in V and V , that is, either α V and α V , or α / V and α / V . Otherwise V and V disagree on α. Given a valuation V and a group of agents J Agt, Att J(V ) = {tiα : i J} is the set of J s attempt atoms in V and Ctrl J(V ) = {ciα : i J} is the set of J s control atoms of V , alias J s abilities at V .

Example 1. Two agents 1 and 2 are in a room with a window and a radiator. The state of the room is described by the propositional variables w ( the window is closed ) and h ( the heating is on ). 1 controls h and 2 controls w. Moreover, 1 has authority over 2 and can order 2 to open or close the window: 1 controls t2w. Initially w and h are both false, and 1 is going to try to switch the heating on and to make 2 flip his goal about the window. This is modelled by the valuation

V hw = {c1h, t1h, c2w, c1t2w, t1t2w}.

In our example control is exclusive: no variable is controlled by more than one agent. For the sake of generality we do not impose this as a general constraint.

2.2 Successor Valuations

A given valuation determines its successor valuation; let us discuss in detail how this should work. We have said that tiα means that i is going to try to act on α. If i does not control α then this is going to fail; and if i controls α then the effect of i s trying is that the truth value of α gets flipped. For example, the successor of V h 1 = {c1h, t1h} should contain h and the respective successors of V h 2 = {c1h} and V h 3 = {t1h} should not. We understand an attempt atom tiα as a persistent goal in the sense of Cohen and Levesque s logic of intentions [1990] that is only abandoned once it has been satisfied: i will basically keep on trying until either the truth value of α has changed, or until an agent j (possibly i herself) terminates i s commitment to achieve α. When i has the goal to change the truth value of p then i typically also has the goal to abandon the goal tip, i.e., to change the truth value of tip. Therefore the valuations V h 1 {c1t1h} and V h 1 {c1t1h, t1t1h} should have the same successor, namely {h, c1h, c1t1h}. We consider that abilities (i.e., control) are a priori preserved, unless they get flipped by a successful higher-order attempt. Therefore the successor of the above V h 1 should intuitively be {c1h, h} and the successor of V h 2 should be V h 2 . We also consider that attempts should be preserved if they failed. Hence the successor of V h 3 should be V h 3 . In our example it is possible that 1 achieves h (and therefore abandons her goal to flip h) and simultaneously makes 2 adopt the goal to flip h. Consider V h 1 {c1t2h, t1t2h, c2h}. On the one hand, 1 s successful attempt to act on h will make 1 abandon her goal to act on h, i.e., t1h will become false; on the other hand, her successful second-order attempt to act on t2h will make the latter true. Hence the successor should be {c1h, c1t2h, c2h, t2h, h}, and the successor of the latter should be {c1h, c1t2h, c2h}. Overall, h was initially false, then became true, and ends up false again. The changeset of a valuation V is

V = {α : ciα V and tiα V for some i Agt}.

The elements of V are the goals that should a priori be abandoned: the atoms of V whose change of truth value is directly caused by the agents successful attempts in V . The definition of the successor of a valuation then is:

succ(V ) = (V \ V ) V \ V {tiα V : α V , i Agt} .

Hence (1) everything in the changeset that is false becomes true; (2) everything that is true and is neither in the changeset nor a goal to be abandoned remains true. Put differently: V and succ(V ) agree on α if and only if α / V and there is no β V such that α = tiβ. Some examples are:

succ({c1h, c2h, t1h}) = {c1h, c2h, h}, succ({c1h, c2h, t1h, t2h}) = {c1h, c2h, h}, succ({c1h, c1t1h, h}) = {c1h, c1t1h, h}, succ({c1h, c1t1h, t1t1h}) = {c1h, c1t1h, t1h}, succ({c1h, c1t1h, t1t1h, t1h}) = {c1h, c1t1h, h}.

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)

The function succ(.) is total: every valuation has exactly one successor. A valuation may have more than one predecessor, as illustrated by the first two lines of our examples. (Another example is succ( ) = succ(Atm) = .) We inductively define the n-th successor of V :

succ0(V ) = V ,

succn+1(V ) = succ(succn(V )).

Example 2 (Example 1, ctd.). In the valuation

V hw = {c1h, t1h, c2w, c1t2w, t1t2w},

agent 1 is going to try to switch the heating on and to make 2 flip his goal about the window. Both attempts are going to be successful because 1 controls h and 1 controls 2 s attempts on w. Hence at succ(V ) the heating is on and the window is open, and at succ2(V ) and beyond the heating is on and the window is closed:

succ1(V ) = {c1h, h, c2w, c1t2w, t2w}, succn(V ) = {c1h, h, c2w, c1t2w, w}, for n 2.

2.3 Agent Choices We define the relation J between valuations as follows:

V J V if V and V agree on every atom in Prp Ctrl {tiα : i J, α Prp Ctrl and ciα V }.

That is, V J V iff V and V agree on facts, abilities, and on successful attempts by agents in J to flip facts and abilities at the next step. We call the latter the immediate choices of J at V . Put differently, V J V when V and V agree on facts and abilities as well as in the way that agents of J collectively influence the evolution of these facts and abilities in the immediate future. For example, for the valuation of Example 2 we have V hw {1} {c1h, t1h, c2w, c1t2w, t2w}. When V V then V and V agree on facts and abilities, abbreviated V V . The relations J are reflexive, transitive, and symmetric. Moreover, V Agt V implies succ(V ) succ(V ). We generalize this and define the relation n J between valuations as follows, for n N0:

V n J V if succn(V ) J succn(V ) and

for every m < n, succm(V ) Agt succm(V ).

That is, V n J V if V and V agree on facts and abilities and on immediate choices of all agents up to step n 1; and moreover agree on immediate choices of J at step n. Hence V 0 J V iff V J V . We define n = n . That is, V n V if succm(V ) Agt succm(V ) for all m < n.

3 The Logic LACA We now define language and semantics of LACA.

3.1 Language of LACA The language of LACA, LLACA(Atm), is defined by the following grammar:

ϕ ::= α | ϕ | ϕ ϕ | Xϕ | Gϕ | [J cstit]ϕ | [J dstit]ϕ,

where α ranges over Atm and J ranges over the powerset of Agt. The formula Xϕ reads ϕ holds next ; Gϕ reads ϕ holds henceforth ; [J cstit]ϕ reads J sees to it that ϕ (the so-called Chellas stit operator); and [J dstit]ϕ reads J deliberately sees to it that ϕ (the deliberative stit operator). The language LLACA(Prp) is the fragment of LLACA(Atm) without control and attempt atoms and is the language of the original group stit logic (in its discrete time version). When convenient we drop set parentheses of coalitions and write e.g. [1, 2 cstit]p instead of [{1, 2} cstit]p. Historic necessity is defined as ϕ = [ cstit]ϕ. The dual of historic necessity is ϕ = ϕ and that of the cstit operator is J cstit ϕ = [J cstit] ϕ. We define the set of atoms of a formula ϕ as follows:

Atm(α) = {α}, Atm(ϕ ψ) = Atm(ϕ) Atm(ψ), Atm( ϕ) = Atm(ϕ) for { , X, G, [J cstit], [J dstit]}.

For example, Atm(c1t2p [1, 2 cstit]c3p) = {c1t2p, c3p}.

3.2 Truth Conditions Here are the truth conditions for LLACA(Atm) formulas: V , n |= α if α succn(V ), V , n |= Xϕ if V , n + 1 |= ϕ, V , n |= Gϕ if V , m |= ϕ for every m n, V , n |= [J cstit]ϕ if V , n |= ϕ for every V n J V , V , n |= [J dstit]ϕ if V , n |= [J cstit]ϕ and V , n |= ϕ, and as usual for the Boolean operators. The idea underlying the Chellas stit modality [J cstit]ϕ is that the current choices of the agents in J guarantee that ϕ is true no matter what the opponents in J attempt. This is the same as: it is not the case that the agents in J are able to achieve ϕ while the agents in J stick to what they currently attempt. We can therefore view [J cstit] as an operator of inability of J s opponents to avoid ϕ. The deliberative stit modality adds to the Chellas stit a negative condition: for J to deliberately see to it that ϕ, ϕ should not be necessarily true.

Example 3 (Example 2, ctd.). We have

V hw, 0 |= h w X(h w) XX(h w) [1 cstit]Xh X[2 cstit]Xw.

The formula remains true when the cstit operator is replaced by the dstit operator.

A LLACA(Atm) formula ϕ is satisfiable if V , 0 |= ϕ for some V ; and it is valid if V , 0 |= ϕ for every V .

Example 4. In Homer s Odyssey, Ulysses escapes the sirens by removing his own control to follow their calls. This example is considered by the philosopher Jon Elster to be paradigmatic of the idea that self-control can be used for coping with weakness of will [Elster, 1979]. We model two versions of the situation: what might have happened if Ulysses had not been so clever to get tied to the mast and what actually happens. Initially Ulysses (u) is not on the sirens island and controls whether he is on the island or not (cu On Is). He can abandon his control (cucu On Is). The sirens, for simplicity viewed as a single agent s, can make Ulysses change his mind about

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)

swimming to the island (cstu On Is) and indeed attempt to do so (tstu On Is). This corresponds to the following valuation:

V u 1 = {cu On Is, cucu On Is, cstu On Is, tstu On Is}.

But Ulysses actually decides to abandon his control by getting tied to the mast: the valuation corresponding to Homer s story is V u 2 = V u 1 {tucu On Is}. Then V u 1 s V u 2 and:

succ(V u 1 ) = {cu On Is, cucu On Is, cstu On Is, tu On Is}, succ(V u 2 ) = {cucu On Is, cstu On Is, tu On Is}.

V u 1 , 0 |= X[s cstit]XOn Is, V u 2 , 0 |= [u dstit]XX On Is [u dstit]X[u cstit]X On Is.

In V u 1 , the sirens get their wishes and see to it that Ulysses follow their calls. In V u 2 , Ulysses manages to avoid this outcome and (deliberately) sees to it that he stays on his ship by choosing to remove his own control.

4 Reconstruction of BT+AC Structures

We now assess our controland attempt-based logic w.r.t. Belnap and Horty s stit logic by establishing the relation with their semantics in terms of BT+AC models. Our construction leads to a discrete time structure and inverses the standard way the definition of BT+AC models proceeds. The latter takes moments that are ordered in time to be primitives, then defines histories, and finally adds agent choices. In contrast, our construction starts from histories (which are induced by valuations via the successor function) and then defines moments, their temporal ordering, and agent choices. We start by recalling BT+AC models.

4.1 Discrete BT+AC Models

We recall the definitions from [Horty, 2001], which we adapt to the case of discrete tree structures as done e.g. in [Boudou and Lorini, 2018; Broersen et al., 2006; Schwarzentruber, 2012]. A discrete BT structure is a pair (W, <) where W is a non-empty set of moments and < is a strict partial order on W that is tree-like1 and discrete. Histories are maximal sets of linearly ordered moments. The set of all histories of (W, <) is Hist. The set of histories sharing the moment w is Hw Hist. The (unique) successor of w on history h is succ(w/h). A BT+AC model is a quadruple M = (W, <, Choice, V) where (W, <) is a BT structure, Choice maps every moment-agent pair (w, i) to a partition of Hw, and V associates to each p Prp a set of moment-history pairs: V(p) W Hist. Essentially, Hw represents all possible timelines branching from moment w, each corresponding to different choices of agents at w, and Choice(w, i) represents the possible choices of a single agent i at w, each leading to a different subset of Hw. It is assumed that Choice is such that:2

1. For every Q Choice(w, i) we have Q = .

1 If w1<w3 and w2<w3 then w1=w2 or w1<w2 or w2<w1. 2It is often assumed that Choice(w, i) = , but this is redundant.

2. For every w and mapping sw : Agt 2Hw such that sw(i) Choice(w, i) (that is, a selection of one choice for each agent) we have T i Agt sw(i) = .

3. If h and h are undivided at w then h Choice(w, i)(h).3

The second constraint says that the agents choices are independent. The third constraint is called no choice between undivided histories . Letting the set of all selection functions at w be

Selectw = {sw : sw(i) Choice(w, i), for every i Agt},

choices of groups of agents J are defined by:

Choice(w, J) = n \

i J sw(i) : sw Selectw o .

In particular, Choice(w, ) = {Hw} for the empty group. Moreover, given a history h Hw,

Choice(w, J)(h) = {h Hw : h, h Q for some Q Choice(w, J)}.

That is, Choice(w, J)(h) is the particular set of histories containing h among the choices of group J, or in other words, the choice of group J at moment w in the history h. Then the formulas of the language given in Section 3.1 are interpreted at moment-history pairs as follows: M, w/h |= p if w/h V(p), M, w/h |= Xϕ if M, succ(w/h)/h |= ϕ, M, w/h |= [J cstit]ϕ if M, w/h |= ϕ for every h Choice(w, J)(h), M, w/h |= [J dstit]ϕ if M, w/h |= [J cstit]ϕ and M, w/h |= ϕ, and as expected for the Boolean operators. In the rest of the section we show how to construct BT+AC structures from the valuations of Section 2. We start by defining histories as mappings from natural numbers to valuations and then show how every valuation generates a history.

4.2 From Valuations to BT Structures In the context of our models of control and attempt, moments can be identified with n equivalence classes, choices correspond to agents attempts, and branching histories stem from different choices for agents. We start with BT structures. Let V0 be a valuation. Let V0

be the -equivalence class of V0: V0 = {V : V V0}. The set of moments is defined as

n N0 W n V0,

where for all n N0, W n V0 = V0 / n is the quotient operator. We use disjoint union ( ) in order to ensure that two equivalent moments, whereby agents control the same variables and make the same attempts, can occur at different depths of the BT structure. Given a moment w W n V0, the set of successors of w for the order <V0 is:

succ(w) = {w W n+1 V0 : w w = }.

3Two histories h and h are undivided at a moment w W if either w and succ(w/h) are both on h , or w has no successor. That is, if w has a successor then w has the same successor in h and h .

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)

Fact 1. succ(w) is a partition of w. Proposition 1. <V0 is a tree-like order. Recall that histories in BT structures are maximal sets of linearly ordered moments. If h is a history of (WV0, <V0), then for all n N0 we denote by h(n) the unique member of h W n V0. Every valuation V clearly induces a single history h V such that V h V (n) for all n N0. The other way round, each history is induced by at least one valuation. Proposition 2. For every history h of (WV0, <V0), there exists V V0 such that h = h V . Corollary 1. For every w WV0, the set Hw of histories containing w is exactly the set of histories induced by valuations in w, i.e., we have Hw = {h V : V w}.

4.3 From Valuations to Agent Choices We now show how to construct a full BT+AC model MV0 = (WV0, <V0, Choice V0, VV0) from a valuation V0. We have already defined WV0 and <V0. As all valuations in an equivalence class for agree on propositional variables, VV0 is naturally defined by

VV0(p) = {w/h : w W n V0 for some n N0, h Hw,

and p succn(V ) for V w}.

If i is an agent and w W n V0, we define

Ctrli(w) = {α Prp Ctrl : there is a V w such that ciα succn(V ) and tiα succn(V )}.

Intuitively, the set Ctrli(w) is the set of possible immediate choices of agent i at w. We now define Choice V0(w, i) for w W n V0 as:

Choice V0(w, i) = {{h V : V w and Atti(succn(V )) (Prp Ctrl) = Γ} : Γ Ctrli(w)}.

Proposition 3. Consider w WV0. Then: 1. Choice V0(w, i) is a partition of Hw; 2. Any H Choice V0(w, i) is nonempty; 3. Choice V0(w, i) satisfies the no choice between undivided histories constraint; 4. For every selection function sw : Agt 2Hw such that sw(i) Choice V0(w, i) we have T i Agt sw(i) = .

The choices of group J at w are:

Choice V0(w, J) = {{h V : V w and i J, Atti(succn(V )) (Prp Ctrl) = Γi} : i J, Γi Ctrli(w)}.

Given a history h V with w = h V (n), Choice V0(w, J)(h V ) corresponds to fixing the immediate attempts of agents of J at h V (n) to those of succn(V ):

Choice V0(w, J)(h V ) = {h V : V w and

succn(V ) J succn(V )}

= {h V : V n J V }.

Proposition 4. MV0 = (WV0, <V0, Choice V0, VV0) is a BT+AC structure satisfying all constraints of Section 4.1.

4.4 Equivalence

We are ready to show that all standard stit validities are also valid in models of control and attempt.

Proposition 5. Let ϕ LLACA(Prp) be a formula and V0 2Atm be a valuation. For all n N0 and V V0, MV0, h V (n)/h V |= ϕ iff V , n |= ϕ.

4.5 Beyond Standard Validities

The above inclusion is strict: there are LACA-valid LLACA(Prp) formulas that not valid in BT+AC models. First of all, standard validities in BT+AC models with discrete time such as [J cstit]Xϕ X ϕ. are also LACA valid. Beyond that, facts and abilities are moment determinate in LACA, as expressed by the implications α α and α α, for α Prp Ctrl. This property is discussed as optional in the stit literature [Horty, 2001]. Here are three formulas that are not standardly valid but are valid in LACA. The implication Xp p, for p Prp expresses that facts don t change by themselves, and ( p Xp) W i Agt[i cstit]Xp expresses that every fact change is caused by some agent. Finally, the equivalences [i cstit](p q) ([i cstit]p [i cstit]q) and [J cstit]p W i J[i cstit]p are valid because in LACA, agency is based on a relation between individuals and atoms.

5 Complexity of Model Checking

The model checking problem we are interested in is the following: given a valuation V Atm, a time point n N0 and formula ϕ LLACA(Prp), do we have V , n |= ϕ? In this section we prove that it is PSPACE-complete.

5.1 Relevant Valuations

A key factor in the complexity of evaluating formulas is the infinity of valuations that need to be checked when evaluating G and [J cstit] operators. Let us investigate whether we can restrict ourselves to considering only a finite number of valuations. First, we define the length of an atom of Atm to be the length of the prefix of the propositional variable:

ℓ p = 0, ℓ ciα = 1 + ℓ α , ℓ tiα = 1 + ℓ α .

For example, ℓ c1c2t3p = 3. We extend the definition of length to finite valuations: ℓ V = P α V ℓ α . We can now establish that finite valuations only have a finite number of successors:

Proposition 6. Let V Atm be a finite valuation.

1. card(V ) card(succ(V ));

2. Either ℓ V > ℓ succ(V ) or succ(V ) = V .

Given a valuation V and a group of agents J, considering all valuations such that V n J V amounts to considering variations on J s attempts as well as on attempts of agents of J outside of their immediate choices. There is actually no need to consider variations on attempt atoms that are not a suffix of any control atom in V .

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)

Proposition 7. Let V be a valuation, J be a group of agents and ϕ be a formula of LLACA(Prp). Then V , n |= [J cstit]ϕ iff V , n |= ϕ for all V such that V n J V and V and V differ only by attempt atoms tiα such that ciα is a suffix of a control atom in Ctrl Agt(V ).

5.2 PSPACE-Completeness Using the results of the previous section, we now prove that model checking formulas of LLACA(Prp) in our framework is PSPACE-complete. Proposition 8. The LLACA(Prp) model checking problem is in PSPACE-complete.

Proof sketch. The membership proof is based on an algorithm computing whether V, n |= ϕ. The number and size of alternative valuations that need to be checked in the cases of Gϕ, [J cstit]ϕ and [J dstit]ϕ are limited by Propositions 6 and 7. Hardness is shown through a polynomial reduction of the problem of model checking Quantified Boolean Formulas (QBF), which is known to be PSPACE-complete.

6 Application: Modelling Influence In this section we we put our logic LACA into practice and show how it allows us to formalise Lorini and Sartor s [2016] definition of social influence. Their concept is based on the idea that for the influencer i to induce an influencee j to make a certain choice, i has to change j s choice context, so that a choice differing from j s preferred option without this modification becomes preferable to j. Agent j s choice context includes both j s available choices determined by what agent j controls (i s choice set) and j s preferences. i influences j so that ϕ is defined as:

[i inflj]ϕ = [i cstit]X(Ratj [j dstit]ϕ),

where Ratj expresses that j is rational. For agent i (the influencer) to induce agent j (the influencee) to see to it that ϕ, i s actual choice must guarantee that every rational choice of j will make ϕ true. The reason why agent j s action is modeled by the deliberative stit operator is that for agent j to be influenced by agent i, j should have a choice available in his choice set possibly leading to ϕ; i.o.w., influence requires that the consequence of the influencee s action could have been avoided, had the influencee made a different choice. Let us see how we can express that an agent j is rational. Simply supposing that Ratj is yet another special propositional variable (as done in [Lorini and Sartor, 2016]) fails to do the job because that variable would not be related to the agent s choices. Instead, we suppose that for every agent i there is a formula Rati characterising the states where an outcome with maximal utility obtains next: an agent is rational in a valuation if the successor valuation is ideal for the agent. One possibility is that Rati is of the form Xϕ: i prefers ϕ to be true next; in particular, when i prefers ϕ to be true from the next state on then Rati contains XGϕ. Another possibility is that Rati characterises, for each action in i s choice set, under which conditions it is rational for i to try to perform it. Then Rati is typically a conjunction of equivalences of the

form tip ϕi p where ϕi p does not involve attempt atoms. For example, if i prefers to make p true whatever the values of the other variables are then Rati contains tip p. Example 5 (Example 1, ctd.). Suppose agent 2 wants to to save energy: she prefers that the window is closed (w) when the heating is on (h); otherwise she does not care. We therefore have Rat2 = X(h w). Consider the valuation

V hw 1 = {c1h, t1h, c2w, c2t2w}.

Hence 1 is going to try to switch the heating on, which, intuitively, should influence 2 so that the window is going to be closed. In terms of actions: 1 s switching the heating on is going to make 2 close the window. We therefore expect V hw 1 , 0 |= [1 infl2]Xw, i.e., V hw 1 , 0 |= [1 cstit]X(Rat2 [2 dstit]Xw). Let us check in detail that this is indeed the case. First, when interpreting the modality [1 cstit] at V hw 1 we check whether V hw 1 S, 0 |= X(Rat2 [2 dstit]Xw), for every S {t2α : α Atm} {t1α : c1α / V or α = tiβ}. Thanks to Proposition 7, we know that it is enough to consider variations on t2w and t2t2w. Let us consider the three sets V hw 1 , V2 = V hw 1 {t2w}, and V3 = V hw 1 {t2t2w}. Their respective successors are

succ(V hw 1 ) = {h, c1h, c2w, c2t2w}, succ(V2) = {h, c1h, c2w, c2t2w, w}, succ(V3) = {h, c1h, c2w, c2t2w, t2w}.

Observe that succ(V2) is obtained from V hw 1 by 1 switching the heating on and 2 simultaneously closing the window, so to speak anticipating 1 s influence. Both (V2, 1) and (V3, 1) satisfy Rat2, and it therefore remains to check whether V2, 1 |= [2 dstit]Xw and V3, 1 |= [2 dstit]Xw, which are indeed the case. Therefore V hw 1 , 0 |= [1 infl2]Xw.

7 Conclusion We have presented a stit framework in which the notion of action is conceptually and computationally grounded on the notions of control and attempt. We have proved that, unlike the standard stit framework in which model checking is unfeasible because histories are infinite, model checking in our framework is PSPACE-complete. In future work, we expect to broaden its scope of application by formalizing further action-related concepts that have been investigated in the literature on stit logic. The latter include the concept of controllability, as an agent i s capacity to influence another agent j to perform a certain action [Lorini and Sartor, 2021], as well as the concept of responsibility in its active form (i.e., responsibility for action) and passive form (i.e., responsibility for omission) [Lorini et al., 2014; Lorini and Schwarzentruber, 2011]. As we have shown in Section 6, our logic LACA offers a minimalistic and computionally grounded framework for modeling these concepts. Moreover, we plan to come up with an axiomatisation of the validities of our discrete group stit logic. Last but not least, we plan to enrich our temporal stit framework with past tense modalities for yesterday (Y) and always in the past (H) and to formalize the concept of achievement stit studied in [Belnap et al., 2001] that better approximates agent causation.

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)

Acknowledgments

We thank the reviewers for their comments. Our research was partly supported by the ANR-3IA Artificial and Natural Intelligence Toulouse Institute (ANITI), the EU ICT-48 2020 project TAILOR (No. 952215) and the ANR chair BE4mus IA.

References [Balbiani et al., 2008] Philippe Balbiani, Andreas Herzig, and Nicolas Troquard. Alternative axiomatics and complexity of deliberative stit theories. Journal of Philosophical Logic, 37(4):387 406, 2008. [Belnap et al., 2001] N. Belnap, M. Perloff, and M. Xu. Facing the Future: Agents and Choices in Our Indeterminist World. Oxford University Press, 2001. [Boudou and Lorini, 2018] Joseph Boudou and Emiliano Lorini. Concurrent game structures for temporal STIT logic. In Elisabeth Andr e, Sven Koenig, Mehdi Dastani, and Gita Sukthankar, editors, Proceedings of the 17th International Conference on Autonomous Agents and Multi Agent Systems, AAMAS 2018, Stockholm, Sweden, July 10-15, 2018, pages 381 389. IFAAMAS/ACM, 2018. [Broersen et al., 2006] Jan Broersen, Andreas Herzig, and Nicolas Troquard. Embedding Alternating-time Temporal Logic in strategic STIT logic of agency. Journal of Logic and Computation, 16(5):559 578, 2006. [Broersen, 2011] Jan Broersen. Deontic epistemic stit logic distinguishing modes of mens rea. Journal of Applied Logic, 9(2):137 152, 2011. [Cohen and Levesque, 1990] Philip R Cohen and Hector J Levesque. Intention is choice with commitment. Journal of Artificial intelligence, 42(2):213 261, 1990. [Elster, 1979] Jon Elster. Ulysses and the Sirens. Cambridge University Press, Cambridge, 1979. [Halpern and Vardi, 1991] Joseph Y. Halpern and Moshe Y. Vardi. Model checking vs. theorem proving: A manifesto. In James F. Allen, Richard Fikes, and Erik Sandewall, editors, Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 91). Cambridge, MA, USA, April 22-25, 1991, pages 325 334. Morgan Kaufmann, 1991. Also in Artificial and Mathematical Theory of Computation 1991: 151-176. [Herzig and Schwarzentruber, 2008] Andreas Herzig and Francois Schwarzentruber. Properties of logics of individual and group agency. In Carlos Areces and Robert Goldblatt, editors, Advances in Modal Logic (Ai ML), pages 133 149, Nancy, 2008. College Publications. [Herzig et al., 2011] Andreas Herzig, Emiliano Lorini, Nicolas Troquard, and Fr ed eric Moisan. A dynamic logic of normative systems. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), pages 228 233, 2011. [Horty and Belnap, 1995] John 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. [Lorini and Herzig, 2008] Emiliano Lorini and Andreas Herzig. A logic of intention and attempt. Synthese, 163(1):45 77, 2008. [Lorini and Sartor, 2016] Emiliano Lorini and Giovanni Sartor. A STIT logic for reasoning about social influence. Studia Logica, 104(4):773 812, 2016. [Lorini and Sartor, 2021] Emiliano Lorini and Giovanni Sartor. The ethics of controllability as influenceability. In Schweighofer Erich, editor, Legal Knowledge and Information Systems - JURIX 2021: The Thirty-fourth Annual Conference, Vilnius, Lithuania, 8-10 December 2021, volume 346 of Frontiers in Artificial Intelligence and Applications, pages 245 254. IOS Press, 2021. [Lorini and Schwarzentruber, 2011] Emiliano Lorini and Francois Schwarzentruber. A logic for reasoning about counterfactual emotions. Artificial Intelligence, 175(3-4):814 847, 2011. [Lorini et al., 2014] Emiliano Lorini, Dominique Longin, and Eunate Mayor. A logical analysis of responsibility attribution: emotions, individuals and collectives. Journal of Logic and Computation, 24(6):1313 1339, 2014. [Lorini, 2013] Emiliano Lorini. Temporal STIT logic and its application to normative reasoning. Journal of Applied Non Classical Logics, 23(4):372 399, 2013. [Schwarzentruber, 2012] Franc ois Schwarzentruber. Complexity results of STIT fragments. Studia Logica, 100(5):1001 1045, 2012. [van der Hoek et al., 2011] Wiebe van der Hoek, Nicolas Troquard, and Michael Wooldridge. Knowledge and control. In Liz Sonenberg, Peter Stone, Kagan Tumer, and Pinar Yolum, editors, Proceedings of the 10th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2011), pages 719 726. IFAAMAS, 2011.

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)