A dynamic logic of agency. I: STIT, capabilities and powers (Q2268355)

The authors define \(\mathcal{DLA}\), the \textit{Dynamic Logic of Agency}, whose language extends that of modal logic with formulas of the form \(\langle i\!:\!a\rangle\varphi\), where \(i\) and \(a\) belong to finite sets whose members denote \textit{agents} and \textit{actions}, respectively. Intuitively, \(\langle i\!:\!a\rangle\varphi\) expresses that ``agent \(i\) performs action \(a\) and \(\varphi\) holds afterwards.'' In any given member of a set \(W\) of possible worlds, all agents concurrently perform a unique action, which leads into another possible world. An equivalence relation on \(W\) partitions \(W\) into sets of worlds that share a common history, but might lead later to different worlds depending on the actions performed by some agents. A key constraint is that, given a positive number \(n\) at most equal to the number of agents, \(n\) possible worlds \(w_1\), \dots, \(w_n\), \(n\) pairwise distinct agents \(i_1\), \dots, \(i_n\) and \(n\) actions \(a_1\), \dots, \(a_n\), if for all \(j\in\{1,\dots,n\}\), agent \(i_j\) performs action \(a_j\) in world \(w_j\) then there exists a possible world \(w\) in the same equivalence class as \(w_1\), \dots, \(w_n\) such that for all \(j\in\{1,\dots,n\}\), agent \(i_j\) performs action \(a_j\) in \(w\). The authors provide an axiomatisation of \(\mathcal{DLA}\) before defining two notions of ``seeing to it that'' (STIT), both expressible in the language of \(\mathcal{DLA}\). Use the notation \(\delta_C\) to represent an assignment of actions to each member of a set \(C\) of agents, referred to as a \textit{coalition}. One notion of STIT, written \(\mathrm{Stit}(\delta_C,\varphi)\), expresses that all agents in \(C\) are going to perform the actions as indicated by \(\delta_C\), and that, necessarily, after that happens, the formula \(\varphi\) holds. The other notion of STIT, written \(\mathrm{Stit}_C\varphi\), is the disjunction of all formulas of the form \(\mathrm{Stit}(\delta_C,\varphi)\), hence expresses that all agents in \(C\) are going to perform some action, and that, necessarily, after that happens, the formula \(\varphi\) holds. The paper provides many properties satisfied by these notions. In the second part of the paper, the authors extend their formalism in two different ways. A first extension consists in imposing that time be discrete, with an initial moment and no endpoint; a formula of the form \(\square\varphi\) reads as ``\(\varphi\) is historically necessary'', whereas a new modal operator \(X\) can be applied for formulas so that \(X\varphi\) reads as ``\(\varphi\) will be true next.'' A second extension adds epistemic operators, one for each agent. The authors discuss the relationships between their formalism and other frameworks, and the relationships between their formalism and the notions of \(\exists\forall\)-capability and \(\forall\exists\)-capability from game theory.