Properties of logics ofindividual and group agency
Andreas Herzig and François Schwarzentruber

abstract. We provide proof-theoretic results about deliberative STIT
logic. First we present STIT logic for individual agents without time, where
the problem of satisﬁability has recently been shown to be NEXPTIMEcomplete in the general case. Then we study STIT logic for groups of agents.
We prove that satisﬁability of STIT formulas involving groups of agents isundecidable by reducing the problem of satisﬁability of a formula of the
product logic S5n to group STIT satisﬁability problem. We also prove thatgroup STIT is not ﬁnitely axiomatizable.

Keywords: logics of agency, deliberative STIT, joint action, decidability,
axiomatizability, complexity

1

Introduction

While logics of programs and actions such as PDL allow to reason about
the relation between an action and its effects, so-called logics of agency areabout the relation between an agent and the effects of his actions. The latterare relevant in game theory, theoretical computer science and philosophy ofaction.
In game theory, Pauly’s coalition logic (CL) allows to reason about the capabilities of coalitions [14]. It provides for expressions of the kind “coalition
J can make φ true at the next time point”.
In theoretical computer science, Alternating-time Temporal Logics ATL
and ATL∗ were introduced by Henzinger et al. in order to reason about distributed processes [2]. The formula hhJiiφ reads “coalition J has a strategy
such that φ holds”, where φ is a formula of linear temporal logic (that has
to satisfy some restrictions in the case of ATL). Goranko showed that CL is
nothing but a fragment of ATL (which in turn is a fragment of ATL∗ ), byidentifying the CL formula [J]φ with the ATL formula hhJiiXφ [9], where
X is the temporal ‘next’ operator.
In philosophy of action constructions of the form [i stit : φ] were introduced by Belnap et col. [4], read “agent i sees to it that φ” or “i brings it
about that φ”. In this paper, we focus on the basic version that is called
Chellas STIT [6] (thus baptized by [10]), noted [i cstit : φ] in the literature.
(The original operator defined by Chellas is nevertheless notably different
since it does not come with the principle of independence of agents that
Advances in Modal Logic, Volume 7. c 2008, the author(s).

134Andreas Herzig and François Schwarzentruber

plays a central role in STIT theory.) The Chellas STIT was extended togroup agency in [4, Section 10.C] and [11, Section 2.4]. For a set of agents
J, the formula [J cstit : φ] reads “group J sees to it that φ”. We here write[J]φ instead of [J stit : φ]. These logics moreover have a modal operatorof historical necessity 2. Recently Broersen et al. showed that ATL can beembedded into the logic of the Chellas STIT, by identifying hhJiiXφ with
¬2¬[J]Xφ [5]. This highlights that the modal operators of CL and ATL
are nothing but fusions of three modal operators. STIT-logics are therefore
the most general formal framework for agency, allowing not only to reason
about what agents can do, but also about what they do.
While it is known that the satisfiability problem is PSPACE-complete forcoalition logic CL [14], EXPTIME-complete for ATL [19], and 2EXPTIMEcomplete for ATL∗ [15], only little is known about the mathematical properties of STIT logic. Up to now the only known results were restricted tothe individual case: Wölfl gave an axiomatization [21], and Xu establishedaxiomatization and decidability in [22] and [4, Chapter 17]. Wansing gave acomplete tableaux calculus, but didn’t prove termination [20]. In previous
work we showed NEXPTIME completeness of the satisfiability problem [3].
The present paper investigates decidability and axiomatizability resultsfor STIT logic without temporal operators. It is organized as follows. In
Section 2 we recall the known results about individual STIT. In Section
3 we recall the definition of group STIT, providing also for an alternative
semantics and a normal form which is built by rewriting all groups that are
different from the ‘grand coalition’ (alias the set of all agents), to what wecall ‘anti-individuals’ (alias complements of singleton groups). Building on
results about the product Logic S5n that we recall in Section 4, we show in
Section 5 that group STIT is undecidable, and in Section 6 that there is no
finite axiomatization for it.

2

Individual STIT

In this section, we present the logic of agentive sentences of the form ‘individual i sees to it that φ’.
The language LSTITn of STITn logic is built from a countably infinite setof atomic propositions ATM and a finite set of agents AGT = {1, . . . , n}.
It is defined by the following BNF:
φ ::= p | ¬φ | (φ ∧ φ) | [i]φ | 2φ
where p ranges over ATM and i ranges over AGT . [i]φ is read “agent isees to it that φ (whatever the other agents do)”, and 2φ is read “φ ishistorically necessary”, or “φ holds whatever all the agents choose to do”.
We use the usual dual operators: 3φ abbreviates ¬2¬φ, and hiiφ abbreviates [i]φ.
REMARK 1. In the STIT literature the formula [i]φ is usually written[i cstit : φ], where ‘cstit’ stands for ‘Chellas STIT’. The formula 2φ issometimes written Sett φ, where ‘Sett’ stands for ‘settled’.

Properties of logics of individual and group agency

135

REMARK 2. Other STIT operators exist: the so-called deliberative STIT
operator [i dstit : φ] can be defined as an abbreviation of [i]φ ∧ ¬2φ; theso-called achievement STIT operator [i astit : φ] is more complex and will
not be considered here.
2.1

Semantics of STITn

We present two semantics for LSTITn . The first one is the original one interms of Belnap’s branching-time models [4], while the second one does not
mention time and is closer to standard presentations of Kripke models.

BT+AC models
Semantics is given to formulas of LSTITn in terms of a branching-time (BT)structure augmented by an agent choice (AC) function.
DEFINITION 3 (BT structure). A BT structure is of the form hM, <i,where M is a nonempty set of moments, and < is a partial order on M
(transitive and anti-symmetric) that is tree-like: for any m1 , m2 and m3
in M , if m1 < m3 and m2 < m3 , then either m1 = m2 or m1 < m2 or
m2 < m1 .
A maximal set of linearly ordered moments from M is a history. Whenm ∈ h we say that moment m is on the history h. Hist is the set of all
histories.
Hm = {h | h ∈ Hist, m ∈ h}is the set of histories passing through m. A moment-history pair is a couple
m/h, consisting of a moment m and a history h from Hm (i.e., a history
and a moment in that history).
BT+AC models are BT structures augmented by agents’ choices (AC)and a valuation.
DEFINITION 4 (BT+AC model). A BT+AC model is a tuple M = hM, <, Choice, V i, where:• hM, <i is a BT structure;Hist• Choice : AGT × M → 22
is a function mapping each agent andeach moment m into a partition of Hm such that for all m and all
Hmsuch that sm (i) ∈ Choice(i, m), we
mappings
T sm : AGT −→ 2
have i∈AGT sm (i) 6= ∅;• V is valuation function V : ATM → 2M ×Hist .
In terms of game theory, each mapping sm : AGT → 2Hm such thatsm (i) ∈ Choice(i, m) for all i is a strategy profile at m. We write Choicemiinstead of Choice(i, m). Each equivalence class belonging to Choicem
i canbe thought of as a choice that is available to agent i at m: when h, h′ ∈Choicemi then agent i’s current choice at the moment-history pair m/h136

Andreas Herzig and François Schwarzentruber

cannot distinguish between h and h′ . Given a moment m, we can view
Hm
Choicemby defining:i as a mapping from Hm to 2′m′
Choicemi (h) = {h ∈ Hm | there is Q ∈ Choicei and h, h ∈ Q}
mThus Choicem
i (h) returns the particular choice from Choicei containingh, or in other words, the particular action performed by i at the momenthistory pair m/h: i’s current choice at m/h forces the possible histories tobe among Choicem
i (h).
We call the constraint of nonempty intersection of all possible simultaneous choices of agents at m the independence constraint.1
A formula is evaluated with respect to a model and a moment-history
pair:M, m/h |= pM, m/h |= ¬φM, m/h |= φ ∧ ψM, m/h |= 2φ
M, m/h |= [i]φ

iff
iff
iff
iff
iff

m/h ∈ V (p), p ∈ ATM
M, m/h 6|= φM, m/h |= φ and M, m/h |= ψM, m/h′ |= φ for all h′ ∈ Hm
M, m/h′ |= φ for all h′ ∈ Choicemi (h)Validity in BT+AC models is defined as truth at every moment-history pairof every BT+AC model. A formula φ is satisfiable in BT+AC models if ¬φ
is not valid in BT+AC models.

Kripke models
We now present an alternative semantics for LSTITn -formulas that is closer
to that of standard modal logics, and was proposed in [13].
DEFINITION 5 (Kripke model). A Kripke model for the logic STITn is atuple W = hW, R, V i where:• W is a nonempty set;
• R is a mapping associating to every i ∈ AGT an
T equivalence relation
Ri on W such that for all (w1 , . . . , wn ) ∈ W n , i∈AGT Ri (wi ) 6= ∅;• V is a valuation function V : ATM → 2W .
Intuitively, Ri is nothing more than the equivalence relation corresponding to the partition Choicem
i . The condition on R corresponds to the independence constraint of BT+AC models.
REMARK 6. Our Kripke models here correspond to the class of pointgenerated models of the semantics proposed in [3]. There, the independence
constraint is formulated in a slightly different way (just because the models
might not be point-generated).
A formula is evaluated as usual with respect to a model and a point.
1 There are other constraints relating the BT structure and the choice function, suchas “no choice between undivided histories”. They are not relevant here because we do
not have temporal operators in our language, and we therefore omit them.

Properties of logics of individual and group agency

W, w |= pW, w |= ¬φW, w |= φ ∧ ψW, w |= 2φW, w |= [i]φ

iff
iff
iff
iff
iff

137

w ∈ V (p), for p ∈ ATM
W, w 6|= φW, w |= φ and W, w |= ψW, w′ |= φ for all w′ ∈ W
W, w′ |= φ for all w′ ∈ Ri (h)Validity and satisfiability in Kripke models are defined as usual.
THEOREM 7. A STITn -formula is satisfiable in BT+AC models iff it issatisfiable in Kripke models.
Proof. The proof is done by transforming a given BT+AC model into a
Kripke model and vice versa. It is a particular case of the proof of Theorem
11 in Section 3.1.


2.2

Axiomatization, decidability and complexity of STITn

Xu gave the following axioms:
S5(2)the axiom schemas of S5 for 2;

S5(i)the axiom schemas of S5 for every [i], for every i ∈ AGT ;(2→i)

2φ → [i]φ, for every i ∈ AGT ;(AIAn )

(3[1]φ1 ∧ . . . ∧ 3[n]φn ) → 3([1]φ1 ∧ . . . ∧ [n]φn ).

(AIAn ) is called the axiom schema for independence of agents. Xu’s
axiomatics has the standard inference rules of modus ponens and necessitation for 2. From the latter necessitation rules for every [i] follow by axiom(2→i).
From Xu’s completeness theorem [4, Chapter 4] and Theorem 7 we get:
THEOREM 8. [4, Chapter 17] A formula φ of LSTITn is valid in Kripke
models iff φ is provable from the schemas S5(2), S5(i), (2→i), and (AIAn )by the rules of modus ponens and 2-necessitation.
REMARK 9. An alternative axiomatization is given
V in [3], where (AIAn ) is
replaced by the simpler axiom schema 3φ → hki {hliφ | 1 ≤ l ≤ n and l 6=k}.
It is also shown there that 3φ can be viewed as an abbreviation of hiihjiφ,for some arbitrary i and j.
The complexity of the satisfiability problem for STITn -formulas dependsof the number of agents.
THEOREM 10. [3] The problem of deciding satisfiability of a formula of
LSTITn is NP-complete if n = 1, and it is NEXPTIME-complete if n ≥ 2.

138

3

Andreas Herzig and François Schwarzentruber

Group STIT

In this section, we extend the individual STIT to group STIT: we study the
logic of agentive sentences of the form ‘group J sees to it that φ’. Now
modal operators have as arguments coalitions J ⊆ AGT .
Just as in the individual case, the language LSTITG
of STITGn logic is built
nfrom a countable set of atomic propositions ATM and a finite set of agents
AGT = {1, . . . , n}. But now the modal operators have sets of agents asarguments, and LSTITG
is defined by the following BNF:nφ ::= p | ¬φ | (φ ∧ φ) | [J]φwhere p ranges over ATM and J ranges over 2AGT .
The language of individual STIT becomes a fragment of that of group
STIT if we identify [{i}] with [i]. The semantics of group STIT will guaranteethat the LSTITG
formula [∅]φ has the same interpretation as the LSTITnnformula 2φ.
3.1 Semantics of STITGn
Again, we present the semantics both in terms of branching-time models as
defined by Horty and Belnap [10] and Belnap and Perloff [4, Chapter 10],and in terms of Kripke models [13]. We prove that both classes of models
have the same logic. The latter will be useful to establish the relationshipwith product logics.

BT+AC models

Models for STITG
n are the same those of the logic STITn , i.e. BT+AC models
satisfying the independence constraint. The only thing we have to do is toextend the definition of Choice in order to interpret group agency.
Horty defines in [11] the notion of collective choice. He first introduces
action selection functions sm from AGT into 2Hm such that for each m ∈ M
and a ∈ AGT , sm (a) ∈ Choicem
a . So a selection function sm selects aparticular action for each agent at m. Then for a given m,
Selectm = {sm : AGT → 2Hm | sm (a) ∈ Choicem
a , for all a ∈ AGT }is the set of all such selection functions. This allows to extend the definitionof Choice. A collective choice for a nonempty group of agents ∅ ( J ⊆ AGT
at moment m is defined as:\
Choicemsm (j) | sm ∈ Selectm }
J ={
j∈J
m
For J = ∅ we define Choicem∅ = {Hm }. We can check that every ChoiceJ
is a partition of Hm .
As before,′m′
Choicem
J (h) = {h ∈ Hm | there is Q ∈ ChoiceJ and h, h ∈ Q}

Properties of logics of individual and group agency

139

is the particular choice from Choicem
J containing h, or in other words, theparticular joint action performed by coalition J at the moment-history pairm/h. And as before, formulas are interpreted with respect to a model anda moment-history pair:M, m/h |= [J]φiff

M, m/h′ |= φ for all h′ ∈ Choicem
J (h).

Observe that the LSTITG-formula [∅]φ is true at m/h if and only if then
LSTITn -formula 2φ is true at m/h.
Validity and satisfiability are defined as before.

Kripke models

Kripke models for STITG
n are the same as for STITn . Just as we definedm
ChoicemJ from Choicei in the last section, we here define RJ from the Ri s.
Let W = hW, R, V i be a Kripke model for STITn . For all nonempty
J ⊆ AGT , we define
\
RJ =
Ri
i∈J

and R∅ = W × W .
A formula is evaluated as usual with respect to a model and a world:W, w |= [J]φiff

W, w′ |= φ for all w′ ∈ RJ (w)

THEOREM 11. A STITG
n -formula is satisfiable in BT+AC models iff it issatisfiable in Kripke models.
Proof. ⇒ Let M′ = hM ′ , <, Choice, V ′ i be a BT+AC model such that
M′ , m0 /h0 |= φ for some a moment-history pair m0 /h0 . We define the tuple
W = hW, R, V i as follows:• W = Hm 0 ;0• Ri = {(h, h′ ) | there exists Q ∈ Choicem
such that h, h′ ∈ Q};i• V (p) is the set of histories h ∈ Hm0 such that m0 /h ∈ V ′ (p).
We can check that W is a Kripke model. We can prove by induction on ψthat for all formulas ψ and for all h ∈ Hm0 , W, h |= ψ iff M′ , m0 /h |= ψ.
Hence, W, h0 |= φ.
⇐ Let W = hW, R, V i be a Kripke model such that W, w0 |= φ for someworld w0 ∈ W . We define the BT+AC model M′ = hM ′ , <, Choice, V ′ i asfollows:• M ′ = {m0 } ∪ W for some m0 6∈ W ;• < = {m0 } × W (and thus Hist = Hm0 = {{m0 , w} | w ∈ W });0• Choicem= {{{m0 } × Ri (w)} | w ∈ W }, andiw
Choicei = {{h}, h ∈ Hw } for every w ∈ W ;140

Andreas Herzig and François Schwarzentruber• V ′ (p) is the set of moment-history pairs m0 /{m0 , w} such that w ∈V (p).
We can check that M′ is a BT+AC model. We can also prove by inductionon ψ that for all STITn formulas ψ and worlds w ∈ W , M′ , m0 /{m0 , w} |= ψ
iff W, w |= ψ. Hence M′ , m0 /{m0 , w0 } |= φ.

3.2 Normal form for STITG
n formulas
We now show that every formula of LSTITG
is equivalent to a formula wherenonly the ‘grand coalition’ AGT and ‘anti-individuals’ occur, where the latterare complements of singleton groups.
LEMMA 12. Let W = hW, R, V i be a Kripke model. For all (w1 , . . . , wk ) ∈kAGTWsuch that j 6= l implies Jj ∩ Jl = ∅ we have:
T and J1 , . . . , Jk ∈ 2
j∈{1...k} RJj (wj ) 6= ∅.
Proof. This follows
from the independence constraint, which says thatTni∈AGT Ri (wi ) 6= ∅ for all (w1 , . . . , wn ) ∈ W .



The following theorem holds for any J1 and J2 (that are not necessarily
disjoint).
THEOREM 13. Let J1 , J2 ⊆ AGT . We have:|=STITG[J1 ∩ J2 ]φ ↔ [J1 ][J2 ]φnProof. Let M = hW, R, V i be a Kripke model. We are going to prove that
RJ1 ∩J2 = RJ1 ◦ RJ2 .
⊇ As J1 ∩ J2 ⊆ J1 , we have RJ1 ⊆ RJ1 ∩J2 by definition of the relation
RJ . Likewise, RJ2 ⊆ RJ1 ∩J2 . As RJ1 ∩J2 is transitive, we have RJ1 ◦ RJ2 ⊆RJ1 ∩J2 .
⊆ Let w, w′ ∈ W such that (w, w′ ) ∈ RJ1 ∩J2 . We are going to prove that
RJ1 (w) ∩ RJ1 (w′ ) 6= ∅, i.e. that W contains a point u such that (w, u) ∈ RJ1
and (u, w′ ) ∈ RJ2 (from which it immediately follows that RJ1 ∩J2 ⊆ RJ1 ◦
RJ2 ).
First, we have
RJ1 (w) ∩ RJ1 (w′ ) = RJ1 ∩J2 (w) ∩ RJ1 \J1 ∩J2 (w) ∩ RJ1 ∩J2 (w′ ) ∩ RJ2 \J1 ∩J2 (w′ )by the above Lemma 12. Then, as RJ1 ∩J2 (w) = RJ1 ∩J2 (w′ ), we have
RJ1 (w) ∩ RJ1 (w′ ) = RJ1 ∩J2 (w) ∩ RJ1 \J1 ∩J2 (w) ∩ RJ2 \J1 ∩J2 (w′ ).
As J1 ∩ J2 , J1 \ J1 ∩ J2 , and J2 \ J1 ∩ J2 are pairwise disjoint, we have
RJ1 (w) ∩ RJ1 (w′ ) 6= ∅ again by the above Lemma 12.
THEOREM 14. Let J ( AGT such that AGT \ J = {j1 , . . . , jr }, and let
j¯i = AGT \ {ji }. Then|=STITG[J]φ ↔ [j¯1 ] . . . [j¯r ]φnProperties of logics of individual and group agency

141

Proof. By induction on r, with base case r = 1 and using Theorem 13 forthe induction step.
It follows that every STITG
n -formula can be written only using the grandcoalition [AGT ] and anti-individuals [ī]s. From now on, we consider that a
STITG
n -formula contains only such operators.

4

The product logic S5n

In this part, we briefly recall the product logic S5n . The reader is referredto [7] for more details.
Just as LSTITn , the language of S5n logic is built from a countably infinite
set of atomic propositions ATM and a set of parameters {1, . . . , n}. It isdefined by the following BNF:
φ ::= p | ¬φ | (φ ∧ φ) | 2i φwhere p ranges over ATM and i ranges over {1, . . . , n}.
4.1 Semantics of S5n
A Kripke model for S5n is a cartesian product.
DEFINITION 15 (S5n model). A S5n model is a tuple X = (X, R, V )where:• X = X1 × . . . × Xn for some nonempty sets X1 , . . . , Xn ;• R is a mapping associating to every i ∈ {1, . . . , n} the equivalence
relation
Ri = {h(x1 , . . . , xn ), (y1 , . . . , yn )i ∈ X 2 | xj = yj for all j 6= i}• V : ATM → 2X .
Note that the usual S5n models are more generally products of equivalence relations. Our S5n models here are the subclass of point-generated
models (that suffice for the characterization of S5n ).
Definitions of truth conditions, validity and satisfiability are as usual.
4.2 A nonstandard axiomatics for S5n
We first recall the definition of finite axiomatizability of [7, Chapter 1].
DEFINITION 16 (finite axiomatizability). A logic L is finitely axiomatizable if there is a finite set Ax of formula schemas such that φ ∈ L iff there
is a sequence (φ1 , . . . , φk ) of formulas such that for 1 ≤ i ≤ k, one of thefollowing holds:• φi is a tautology of classical proposition logic or an instance of anaxiom in Ax;

142

Andreas Herzig and François Schwarzentruber• φi is obtained by necessitation from φj , where j < i;
• φi is obtained by modus ponens from φj and φk , where j, k < i;
• φk = φ.
THEOREM 17. [7, Theorem 8.2] The logic S5n is not finitely axiomatizable
for n ≥ 3.
While S5n can thus not be axiomatized in the standard way, there exists
an axiomatization by means of a nonstandard rule.
THEOREM 18. [18] S5n is axiomatized by the following axiom schemas:• S5(2i ): the axiom schemas for S5, for every modal operator 2i• ⊢ 2 i 2 j φ ↔ 2j 2 i φ• Modus Ponens rule:• Necessitation rule:

⊢φ

⊢φ→ψ
⊢ψ
⊢φ
⊢ 2i φ• Rectangle Rule:⊢ (p ∧ τ (¬φ ∧ p)) → φ
if p does not occur in φ⊢φV
where τ (χ) = 21 . . . 2n [( i∈{1,...,n} 31 . . . 3i−1 3i+1 . . . 3n χ) → χ].
It is the Rectangle Rule which is nonstandard.
REMARK 19. The axiomatics in [18] does not have all the axioms ofS5(2i ). These are nevertheless valid in S5n models and we have chosen
to add them explicitly.
4.3

Undecidability of the satisfiability problem for S5n -formulas

While satisfiability of a formula of S5n is decidable for n = 2, things getworse beyond.
THEOREM 20. [18, Theorem 8.6] The problem of satisfiability of a formulaof S5n is undecidable for n ≥ 3.

Properties of logics of individual and group agency

5143Group STIT satisfiability is undecidable

We are going to map the problem of satisfiability in S5n to the problem ofsatisfiability in STITG
n . The range of our mapping is the fragment of LSTITG
nformulas where only the ‘grand coalition’ and ‘anti-individuals’ occur, i.e.
the set of groups J such that either J = AGT , or J = AGT \ {i} for somei ∈ AGT . We note ī such sets. As satisfiability is undecidable for S5n ,satisfiability in STITG
n cannot be decidable either.
The LS5n formula 2i φ will be mapped to the LSTITG
formula [ī]φ. Fornthe ease of exposition, we identify these two kinds of formulas from now on,
and suppose that formulas 2i φ are part of the STITG
n language.
Let atm(φ) be the set of all atomic propositions occurring in φ.
THEOREM 21. For any φ ∈ LS5n , the following are equivalent:
1. φ is S5n -satisfiable;
2. φ is satisfiable in a STITG
n model where RAGT = idW ;V2
3. [∅]( p∈atm(φ) [AGT ]p ↔ p) ∧ φ is STITG
n -satisfiable.
Proof. 1. ⇒ 2. Let X = hX, R, V i be an S5n model and let x0 ∈ X be apoint such that X , x0 |= φ. We define a triple W ′ = hW ′ , R′ , V ′ i as follows:• W ′ = X;
• R′ is a mapping associating to every i ∈ AGT the equivalence relation
Ri′ = {h(x1 , . . . , xn ), (y1 , . . . , yn )i ∈ W ′2 | xi = yi };• V′ =V.

T
We can check that for all (w1 , . . . , wn ) ∈ W ′n , i∈AGT Ri (wi ) 6= ∅. Thus,G
W ′ is a STITTn -Kripke model as defined in Section 3.1. We can see that′Rī =R′ (by definition, cf. Section 3.1)
Tj∈ī j′2=
| xj = yj }j∈ī {h(x1 , . . . , xn ), (y1 , . . . , yn )i ∈ W′2= {h(x1 , . . . , xn ), (y1 , . . . , yn )i ∈ W | xj = yj for all j 6= i}= Ri
and thatT′
RAGT=
R′ (by definition, cf. Section 3.1)
Tj∈AGT j′2| xj = yj }=j∈AGT {h(x1 , . . . , xn ), (y1 , . . . , yn )i ∈ W′2= {h(x1 , . . . , xn ), (x1 , . . . , xn )i ∈ W }= idW ′
We can check by induction on φ that X , z |= φ iff W ′ , z |= φ for allz ∈ W.
2. ⇒ 3. Let W = hW, R, V i be a STITG
n Kripke model such that RAGT =idW , and let V
w0 ∈ W be a world s.t. W, w0 |= φ. As RAGTV = idW , we haveW, w0 |= [∅]( p∈atm(φ) [AGT ]p ↔ p). Thus W, w0 |= [∅]( p∈atm(φ) [AGT ]p↔ p) ∧ φ.
2 Remember that [∅] abbreviates [1̄] . . . [n̄].

144

Andreas Herzig and François Schwarzentruber′′
3. ⇒ 2. Let W ′ = hW ′ , R′ , V ′ i be aVSTITG
n Kripke model and let w0 ∈ W
be a world such that W ′ , w0′ |= [∅]( p∈atm(φ) [AGT ]p ↔ p) ∧ φ. We provethat there exists a STITG
n Kripke model W = hW, R, V i with RAGT = idW
and a point w0 ∈ W such that W, w0 |= φ. Let W = hW, R, V i where:′• W = {RAGT(x) | x ∈ W ′ };′′• Ri = {(RAGT(x), RAGT(y)) | (x, y) ∈ Ri′ };• V (p) = {U ∈ W | U ⊆ V ′ (p)}.
′′Notice that RJ = {(RAGT(x), RAGT(y)) | (x, y) ∈ RJ′ }, and that RAGT
= idW . We can prove by structural induction that for all w ∈ W ′ and forall subformulas ψ of φ:′W ′ , w |= ψ iff W, RAGT(w) |= ψIndeed:W ′ , w |= p

W ′ , w |= [AGT ]pV(because W ′ , w |= [∅]( p∈atm(φ) [AGT ]p ↔ p))′
W ′ , w′ |= p for all y ∈ RAGT
(z)
′
′
′
′
w ∈ V (p) for all w ∈ RAGT
(w)
′
RAGT
(w) ⊆ V ′ (p)′RAGT(w) ∈ V (p)′W, RAGT(w) |= p

iff
iff
iff
iff
iff
iff

W ′ , w |= [ī]ψ

iff
iff
iff
iff

W ′ , w′ |= ψ for all w′ ∈ Rī′ (w)′W, RAGT(w′ ) |= ψ for all w′ ∈ Rī′ (w)′W, RAGT (w′ ) |= ψ′′for all RAGT(w′ ) ∈ Rī (RAGT(w))′
W, RAGT (w) |= [ī]ψ

2. ⇒ 1. Let W = hW, R, V i be a STITG
n Kripke model with RAGT = idW ,and let w0 ∈ W be a world such that W, w0 |= φ. From W we define a S5nmodel X ′ = hX ′ , R′ , V ′ i as follows:• X ′ = X1 × . . . × Xn where for all i ∈ AGT , Xi = {Ri (w) | w ∈ W };• R′ is a mapping associating to every i ∈ AGT the equivalence relation
Ri′ = {((x1 , . . . , xn ), (y1 , . . . , yn )) ∈ X ′2 | xj = yj for all j 6= i};• V ′ (p) = {(x1 , . . . , xn ) |{y} and y).

Ti∈AGT xi ∈ V (p)} (identifying

We can check that
X ′ , (R1 (w), . . . , Rn (w)) |= φ iff W, w |= φTi∈AGT xi =Properties of logics of individual and group agency

145

for all w ∈ W . Indeed:′X ′ , (R1 (w), . . . , Rn (w)) |= p iff (RT 1 (w), . . . , Rn (w)) ∈ V (p)iffi∈AGT Ri (w) ∈ V (p)iff w ∈ V (p) T(notice that i∈AGT Ri (w) = {w})iff W, w |= pand
X ′ , (R1 (w), . . . , Rn (w)) |= [ī]ψ
iff X ′ , (R1 (w), . . . , Ri−1 (w), Ri (w′ ), Ri+1 (w), . . . Rn (w)) |= ψfor all w′ ∈ W
iff X ′ , (R1 (w′′ ), . . . , Ri (w′′ ), . . . Rn (w′′ )) |= ψ
where R1 (w) ∩ . . . ∩ Ri (w′ ) ∩ . . . ∩ Rn (w) = {w′′ } for all w′ ∈ W
iff X ′ , (R1 (w′′ ), . . . , Ri (w′′ ), . . . Rn (w′′ )) |= ψ for all w′′ ∈ Rī (w)iff W, w′′ |= ψ for all w′′ ∈ Rī (w)iff W, w |= [ī]ψ
THEOREM 22. The problem of satisfiability of a formula of STITG
n is undecidable for n ≥ 3.
Proof. By Theorem 20 and 21.

6Group STIT is not finitely axiomatizable

THEOREM 23. There is no finite axiomatization of logic STITG
n if n ≥ 3.
Proof. Suppose for a contradiction that STITG
n is finitely axiomatizable,
i.e. that there exists a finite set of axioms Ax such that for every STITG
nφiff
there
is
a
deductionofφfrom(instances
formula φ, we have |=STITG
nof) Ax using Modus Ponens and Necessitation. Let us define an axiomatics
Ax′ obtained from Ax by removing all [AGT ] operators. We are going toprove that for all formulas φ ∈ LS5n , |=nS5 φ iff there is a deduction of φfrom (instances of) Ax using Modus Ponens and Necessitation. Hence, S5nwould be finitely axiomatizable and there is a contradiction.
Let us prove first that ⊢Ax′ φ implies |=nS5 φ. We do so by proving thateach instance of Ax′ is valid in S5n . Let us consider an instance ψ ′ of anaxiom of Ax′ . ψ ′ is obtained from an instance ψ of Ax by removing all[AGT ] operators. We have |=STITG
ψ. Therefore, ψ is valid in the classn146

Andreas Herzig and François Schwarzentruber′of STITGn -models where RAGT = idW . Hence, ψ is valid in the class of-models
where
R
=
id
.
It
follows
that|=nS5 φ.
STITG
AGT
W
n

φ,

Here is an outline of the ⇐ -sense of the proof. First, for all S5n -formulas

V
iff|=STITG[∅]( p∈atm(φ) [AGT ]p ↔ p) → φn Viff⊢Ax [∅]( p∈atm(φ) [AGT ]p ↔ p) → φ
implies (1) ⊢Ax,[AGT ]ψ↔ψ φimplies (2) ⊢Ax′ φ
It remains to prove (1) and (2).
|=nS5 φAs to (1), it suffices to prove the following:^⊢Ax [∅]([AGT ]p ↔ p) → φ implies ⊢Ax,[AGT ]ψ↔ψ φp∈atm(φ)

This can be established using necessitation and principles of classical propositional logic. Basically the proof goes as follows:. . . (necessitation and principles of classical propositional logic)V⊢Ax,[AGT ]ψ↔ψ [∅]( p∈atm(φ) [AGT ]p ↔ p)(by hypothesis)V⊢Ax,[AGT ]ψ↔ψ [∅]( p∈atm(φ) [AGT ]p ↔ p) → φ⊢Ax,[AGT ]ψ↔ψ φ
As to (2), suppose Ax + ψ ↔ [AGT ]ψ is the axiom system obtained
from Ax by adding the schema ψ ↔ [AGT ]ψ. Then we can prove that
⊢Ax + ψ↔[AGT ]ψ φ implies ⊢Ax′ φ.
The proof of that goes as follows. Assume that ⊢Ax,[AGT ]ψ↔ψ φ. Thereexists a proof of φ, that is to say a sequence (φ1 , . . . , φk ) such that for1 ≤ i ≤ k, one of the following holds:• φi is a tautology, an instance of an axiom in Ax or an instance of[AGT ]ψ ↔ ψ;
• φi is obtained by necessitation from φj where j < i;
• φi is obtained by modus ponens from φj and φk where j, k < i;
• φk = φ.
Now, we construct (φ′1 , . . . , φ′n ) where φ′i is φi in which we have removed
all [AGT ] operators. The reader can check that (φ′1 , . . . , φ′n ) is a proof of φ.
This concludes the proof.

Properties of logics of individual and group agency

7147

Discussion

Now, we are going to propose a generalization of these results, and try to
AGTclassify some more fragments of STITG
n . First, for a given a family C ⊆ 2of subsets of 2AGT we define the language LSTIT[C] by the following BNF:
φ ::= p | ¬φ | (φ ∧ φ) | [J]φwhere p ranges over ATM and J ranges over the set of coalitions C.
Let us call STIT[C] the fragment of STITG
n where formulas are in LSTIT[C] .
2AGT
]
and
STIT
=
STIT[{∅, {1}, . . . , {n}}].
Thus, STITG=
STIT[2nn
We have the following result:
PROPOSITION 24. Let C ⊆ 2AGT . If C has a linear structure, then the
problem of satisfiability of a formula in STIT[C] is NP-complete.
Proof. We can prove that if a formula is satisfiable, then it is so in apolynomial-sized model. The proof is based on a selection-of-points argument. More details can be found in [16].

We conjecture the following result (which would cover Theorems 10 and
22).
CONJECTURE 25. Given C ⊆ 2AGT , the problem of satisfiability of aformula in STIT[C] is:
1. undecidable if there are J1 , J2 , J3 ∈ C such that J1 , J2 , J3 , J1 ∩ J2 andJ2 ∩ J3 , J1 ∩ J3 are distinct;
2. NEXPTIME-complete if there is no J1 , J2 , J3 ∈ C such that J1 , J2 ,J3 , J1 ∩ J2 , J2 ∩ J3 and J1 ∩ J3 are distinct, but there exists J1 , J2 ∈ Csuch that J1 , J2 , J1 ∩ J2 are distinct;
We therefore conjecture, e.g., that: the problem of satisfiability of aformula in STIT[C] is undecidable if C = {{1, 3, 4}, {1, 3, 5}, {4, 5}}, that
it is NEXPTIME-complete if C = {{1, 3, 4}, {1, 3, 5}, {1}}, and that it isNP-complete if C = {∅, {1}, {1, 2}, . . . , {1, 2, . . . , n}}.
Finally, we also conjecture that a nonstandard axiomatization of STITGncan be obtained from that of S5n .

8Conclusion

The paper contains mathematical results for deliberative STIT logic, bothin its individual and group version: while the fragment STITn allowing
to reason only about individual agency is decidable in nondeterministic
exponential time (NEXPTIME), the entire logic STITGn (allowing for joint
agency) is undecidable and cannot be finitely axiomatized. The result for
STITn was established in [3], while the general result for STITG
n is new.

148

Andreas Herzig and François SchwarzentruberG
The results for STITG
n apply a fortiori to extensions of STITn with thetemporal ‘next’ operator. Given these rather negative results, it is interesting to look for decidable fragments of STITG
n and its temporal extensions.
One of these fragments is Pauly’s coalition logic, whose satisfiability problem is decidable in polynomial space (PSPACE-complete). As we said in
the introduction, the CL and ATL formula hhJiiXφ corresponds to STITG
n ’s¬2¬[J]Xφ: in CL, the three modal operators 2, [J] and X are fused into asingle operator. The latter is non-normal: it does not satisfy the K-axiomof standard modal logics. In recent work we have investigated a non-normal
modal logic between coalition logic and STITG
n where 2 and [J] are fused,while X is the standard temporal ‘next’ [8]. We called the resulting logic
CL∗ because it extends CL in the same way as ATL∗ extends ATL. We haveshown that contrarily to ATL∗ , the extension CL∗ provides is for free: CL∗
has the same complexity as CL. We have also argued that the epistemic
extension of CL∗ is more powerful than that of CL: contrarily to the latter,CL∗ allows to reason about the agents’ power, i.e. about agents’ knowledgeof the right action to choose in order to achieve something. In other words,
in the epistemic extension of CL∗ we can say that an agent ‘knows how toplay’. Logics having such expressive power have attracted a lot of attention
recently [17, 12, 1].

BIBLIOGRAPHY[1] Thomas Ågotnes. Action and knowledge in alternating-time temporal logic. Synthese,149(2):377–409, 2006.
[2] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal
logic. In Proceedings of the 38th IEEE Symposium on Foundations of Computer
Science, Florida, October 1997.
[3] Philippe Balbiani, Andreas Herzig, and Nicolas Troquard. Alternative axiomatics andcomplexity of deliberative STIT theories. Journal of Philosophical Logic, 2008. toappear.
[4] Nuel Belnap, Michael Perloﬀ, and Ming Xu. Facing the Future: Agents and Choices
in Our Indeterminist World. Oxford University Press, Oxford, 2001.
[5] 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.
[6] Brian F. Chellas. Time and modality in the logic of agency. Studia Logica, 51(3/4):485–
518, 1992.
[7] Dov M. Gabbay, Agnes Kurucz, Frank Wolter, and Michael Zakharyaschev. ManyDimensional Modal Logics: Theory and Applications. Number 148 in Studies in Logic
and the Foundations of Mathematics. Elsevier, North-Holland, 2003.
[8] Olivier Gasquet, Andreas Herzig, and François Schwarzentruber. The complexity ofreasoning about ability and power. submitted, 2008.
[9] Valentin Goranko. Coalition games and alternating temporal logics. In TARK’01:
Proceedings of the 8th Conference on Theoretical Aspects of Rationality and Knowledge, pages 259–272, San Francisco, CA, USA, 2001. Morgan Kaufmann Publishers
Inc.
[10] 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.
[11] John F. Horty. Agency and Deontic Logic. Oxford University Press, 2001.
[12] Wojtec Jamroga and Wiebe van der Hoek. Agents that know how to play. Fundamenta
Informaticae, 63(2-3):185–219, 2004.

Properties of logics of individual and group agency

149[13] Barteld Kooi and Allard Tamminga. Moral conﬂicts between groups of agents. Journalof Philosophical Logic, 37(1):1–21, 2008.
[14] Marc Pauly. A modal logic for coalitional power in games. Journal of Logic andComputation, 12(1):149–166, 2002.
[15] Sven Schewe. ATL∗ satisﬁability is 2EXPTIME-complete. In 35th International
Colloquium on Automata, Languages and Programming (ICALP 2008), 2008.
[16] François Schwarzentruber.
S52 plus inclusion axioms is NP-complete.
http://www.irit.fr/∼Francois.Schwarzentruber/documents/S52andimplication.pdf,
2008.
[17] Wiebe van der Hoek and Mike Wooldridge. Cooperation, knowledge, and time:
Alternating-time temporal epistemic logic and its applications. Studia Logica, 75:125–
157, 2003.
[18] Yde Venema. Rectangular games. The Journal of Symbolic Logic, 63(4), December
1998.
[19] Dirk Walther, Carsten Lutz, Frank Wolter, and Michael Wookdridge. ATL satisﬁability is indeed exptime-complete. Journal of Logic and Computation, 16:765–787,
2006.
[20] Heinrich Wansing. Tableaux for multi-agent deliberative-STIT logic. In Guido Governatori, Ian Hodkinson, and Yde Venema, editors, Advances in Modal Logic, Volume
6, pages 503–520. King’s College Publications, 2006.
[21] Stefan Wölﬂ. Propositional Q-logic. Journal of Philosophical Logic, 31:387–414, 2002.
[22] Ming Xu. Axioms for deliberative STIT. Journal of Philosophical Logic, 27:505–552,
1998.

Andreas Herzig
IRIT-CNRS,
118 Route de Narbonne, F-31062 Toulouse Cedex 9,France.
herzig@irit.fr
François Schwarzentruber
IRIT-Université Paul Sabatier,
118 Route de Narbonne, F-31062 Toulouse Cedex 9,France.
schwarze@irit.fr