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

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 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

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, AttJ(V) = {tiα : i ∈ J} is the set of J's attempt atoms in V and CtrlJ(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

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

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:

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:

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 :

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

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 succ 2 (V ) and beyond the heating is on and the window is closed:

2.3 Agent Choices

We define the relation ∼J between valuations as follows:

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 ∼nJ between valuations as follows, for n ∈ N0:

That is, V ∼nJ 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.

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:

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:

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 α ∈ succ n (V),

V , n |= Xϕ

if V , n+1 |= ϕ,

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

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 (cuOnIs). He can abandon his control (cucuOnIs). The sirens, for simplicity viewed as a single agent s, can make Ulysses change his mind about swimming to the island (cstuOnIs) and indeed attempt to do so (tstuOnIs). This corresponds to the following valuation:

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 ∪ {tucuOnIs}. Then V u 1 ∼s V u 2 and:

Therefore:

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 control- and 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+ACModels

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-like 1 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.

2 It is often assumed that Choice(w, i) ̸= ∅, but this is redundant.

1. 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 ⋂i∈Agt sw(i) ̸= ∅.
2. 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

choices of groups of agents J are defined by:

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

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:

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 FromValuations 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

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:

3 Two 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′ .

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 hV such that V ∈ hV (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 = hV .

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 = {hV : V ∈ w}.

4.3 FromValuations to Agent Choices

We now show how to construct a full BT+AC model MV0 = (WV0 , <V0 , ChoiceV0 , 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

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

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

Proposition 3. Consider w ∈WV0 . Then:

1. ChoiceV0 (w, i) is a partition of Hw;
2. Any H ∈ ChoiceV0 (w, i) is nonempty;
3. ChoiceV0 (w, i) satisfies the "no choice between undivided histories" constraint;
4. For every selection function sw : Agt -→ 2Hw such that sw(i) ∈ ChoiceV0 (w, i) we have ⋂i∈Agt sw(i) ̸= ∅.

The choices of group J at w are:

Given a history hV with w = hV (n), ChoiceV0 (w, J)(hV ) corresponds to fixing the immediate attempts of agents of J at hV (n) to those of succ n (V ):

Proposition 4. MV0 = (WV0 ,<V0 ,ChoiceV0 , 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 , hV (n)/hV |= ϕ 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) → ∨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 ↔ ∨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:

For example, ℓ(c1c2t3p) = 3. We extend the definition of length to finite valuations: ℓ(V ) = ∑α∈V ℓ(α).

We can now establish that finite valuations only have a finite number of successors:

Proposition 6. Let V ⊆ Atm be a finite valuation.

Given a valuation V and a group of agents J, considering all valuations such that V ∼nJ 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 .

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 ′ ∼nJ V and V and V ′ differ only by attempt atoms tiα such that ciα is a suffix of a control atom in CtrlAgt(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:

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 ↔ ϕip where ϕip 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

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 → [2dstit]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 → [2dstit]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

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.

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 BE4musIA.