A dynamic logic of agency. II: Deterministic \({\mathcal{DLA}}\), coalition logic, and game theory (Q1959225)

The author specialises the framework of \(\mathcal{DLA}\), the \textit{Dynamic Logic of Agency}, developed in [\textit{A. Herzig} and \textit{E. Lorini}, ibid. 19, No.~1, 89--121 (2010; Zbl 1189.03025)] to \(\mathcal{DDLA}\), \textit{Deterministic} \(\mathcal{DLA}\). The language is the same and 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. This condition allows one to define a \textit{next time} operator: \(\varphi\) will be true at the next state if, denoting by \(A\) the set of actions and by \(i\) an arbitrary agent, \(\bigwedge_{a\in A}\neg\langle i\!:\!a\rangle\neg\varphi\) holds. 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 all agents in parallel. A key constraint of \(\mathcal{DLA}\) is that, given possible worlds \(w_1\), \dots, \(w_n\) belonging to the same equivalence class, where \(n\) is the number of agents, and given actions \(a_1\), \dots, \(a_n\), where, for all \(j\in\{1,\dots,n\}\), \(a_j\) is the action performed by the \(j\)th agent in world \(w_j\), 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\}\), the \(j\)th agent performs action \(a_j\) in \(w\). \(\mathcal{DDLA}\) adds to \(\mathcal{DLA}\) a principle of \textit{joint determinism}, which states that if two distinct worlds \(w\) and \(w'\) are in the same equivalence class, then some agent performs a different action from \(w\) than from \(w'\). A complete axiomatisation of \(\mathcal{DDLA}\) is provided. The two notions of ``seeing to it that'' (STIT), both already defined for \(\mathcal{DLA}\), are recalled. 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}. The first notion, 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, if these actions are going to be performed then the formula \(\varphi\) holds in the current state. 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, if these actions are going to be performed then the formula \(\varphi\) holds in the current state. Some properties satisfied by these notions are proved, in particular, that ``two disjoint coalitions can combine their efforts to ensure a conjunction of outcomes''. Then Coalition Logic is translated into \(\mathcal{DDLA}\). In the second part of the paper, the language of \(\mathcal{DDLA}\) is expanded with preferential operators: for an agent \(i\), the formula \([\mathrm{pref}]_i\varphi\) is meant to express that \textit{\(\varphi\) is preferred by \(i\)}. Semantically, given an agent \(i\), a pre-order \(\preceq_i\) is defined over \(W\), with \(w\preceq_i w'\) meaning that agent \(i\) considers \(w'\) to be at least as good as \(w\), subjected to the constraints that (i) for all \(w,w'\in W\), if \(w\preceq_i w'\) then \(w\) and \(w'\) are equivalent (it has to be possible to act at \(w\) so as to get to \(w'\)), and (ii) for all \(w\in W\), \(\prec_i\) restricted to the class of possible worlds equivalent to \(w\) is complete. A formula of the form \([\mathrm{pref}]_i\varphi\) is set to evaluate to true at \(w\in W\) if \(\varphi\) is true at all possible worlds \(w'\) with \(w\preceq_i w'\). A completeness result is provided for this extension of \(\mathcal{DDLA}\), denoted \(\mathcal{DDLA^{+P}}\), as well as the proofs that some formulas are valid. The last part of the paper is devoted to showing that \(\mathcal{DDLA^{+P}}\) is ``sufficiently expressive to formalize some crucial concepts of games in strategic form such as Nash-equilibrium.'' This is done via the fomalization in \(\mathcal{DDLA^{+P}}\) of the game-theoretic notion of \textit{best reponse}. The paper ends with a detailed discussion and comparison on related frameworks.