Computer Science
Computer Science-2021.gz:143181
Computer Science Philosophy
33c0c6cab4e950ae3d8662df3b3ff18e67bd8a4e
A Deontic Stit Logic Based on Beliefs and Expected Utility

The formalization of action and obligation using logic languages is a topic of increasing relevance in the field of ethics for AI. Having an expressive syntactic and semantic framework to reason about agents' decisions in moral situations allows for unequivocal representations of components of behavior that are relevant when assigning blame (or praise) of outcomes to said agents. Two very important components of behavior in this respect are belief and belief-based action. In this work we present a logic of doxastic oughts by extending epistemic deontic stit theory with beliefs. On one hand, the semantics for formulas involving belief operators is based on probability measures. On the other, the semantics for doxastic oughts relies on a notion of optimality, and the underlying choice rule is maximization of expected utility. We introduce an axiom system for the resulting logic, and we address its soundness, completeness, and decidability results. These results are significant in the line of research that intends to use proof systems of epistemic, doxastic, and deontic logics to help in the testing of ethical behavior of AI through theorem-proving and model-checking.


Introduction
It has been argued that an appropriate theory of agency and obligation should take into account what agents know-and what they know how to do-both before and at the moment of acting ( [41], [22], [21], [13]). Following considerations from epistemic game theory (EGT)-which has clear conceptual and technical connections to stit theory (see [16,Chapter 1] and [37])-we put forward that agents' beliefs also play an important role in the relation between agency and obligation. In recent years we have seen a growing interest in adding knowledge modalities to stit theory, but there are relatively few extensions of this logic by means of belief operators (notably those in [39] and [12]). The novelty of the present approach lies in its intention to develop a link between beliefs and ought-to-do. This is a natural step to take in the line of both Horty's formalization of act utilitarian ought-to-do ( [23]) and its extension with epistemic notions ( [21], [13]).
According to Horty ([23]), act utilitarian ought-to-do stems from a measure of optimality of actions. The consequences of optimal actions are taken to be the conditions that agents ought to have brought about in the world. Horty's idea of optimality is undeniably inspired by solution concepts from game theory, particularly by dominance of strategies. Following this idea, the recent works [21] and [1] introduce epistemic (resp. subjective) ought-to-do's to account for the relation between knowledge and obligation. To be more precise, in both these works the optimal actions once again underlie what agents epistemically (resp. subjectively) ought to do, but the measure of optimality now takes into consideration agents' epistemic states. The resulting formalization can deal with complex scenarios for which the initial-non-epistemic-ought-to-do fell short of very intuitive standards in the context of responsibility attribution. Since stit theory can-at least in principle-incorporate most game theoretic ideas into multi-agent action-settings, we find it worthy to extend the theory of ought-to-do with a notion of belief. Our long-term goal is to achieve a nuanced formalization of obligation and responsibility, where agents' hierarchies of belief would serve as explanations of the actions that these agents perform interactively.
Consider the following example, inspired by the famous film The Verdict, of 1982. Suppose that a patient is admitted to the hospital in urgent need of surgery. The nurses draw up a chart with important background information for the surgeons, but unfortunately the figure regarding how long it has been since the patient last ate has a mistake. Anesthetics for this surgery should only be supplied if the patient has had an empty stomach for at least eight hours, and they are deadly otherwise. Because of the mistake in the chart, the anesthesiologist never comes to know that the patient had had a full meal just one hour before admittance. Therefore, she gives the anesthetics and the patient dies. It is clear that the doxastic state of the anesthesiologist plays a key role in determining whether she is morally responsible for the patient's death. On the causal level, the anesthesiologist is responsible for it. However, it seems natural that she should not be held culpable, because she acted upon the false-but justified-belief that the patient had an empty stomach before admittance. Moreover, the anesthesiologist is justified in considering the action of supplying the anesthetics as something that she ought to have done, given the circumstances.
There are several options of conceptual backgrounds for incorporating beliefs into deontic stit logic (see [39], ([4], and [20] for some alternatives). In this work we adopt a quantitative version of agentive belief, and we use probability measures (on the domain of stit structures) to represent doxastic states. An agent's subjective belief in a proposition is taken to depend on the probability that the agent assigns to the indices at which the propositions holds. The reason for choosing a probabilistic semantics of belief is that it allows us to base a notion of doxastic ought on a key concept in decision theory: maximization of expected utility. Thus, we propose that at a given index of evaluation an agent had the doxastic obligation to see to it that ϕ if ϕ is a consequence of all the actions that maximized expected (deontic) utility at such index, where this utility is identified with the deontic value of the index just as in [23]. The basic aspects of the logic that we develop here, then, can be summarized in this way: we extend the basic stit language with (a) epistemic and doxastic operators, (b) objective and subjective ought-to-do operators (whose logic was developed in [1]), and (c) a doxastic ought-to-do operator, meant to build up formulas to characterize the effects of those actions that agents' belief-systems render as optimal-i.e., the effects of rational best responses (see [8]).
The paper is structured as follows. In Section 2 we introduce the syntax and semantics of the epistemic deontic logic that we use as basis for our theory of doxastic oughts. In Section 3 we present the probabilistic conceptualization of belief that we intend to incorporate into the logic of Section 2, and we elaborate on the reasons for choosing such a notion of belief. In Section 4 we introduce the syntax and semantics for formulas involving the doxastic ought-to-do operator, and we discuss an example to illustrate its reach within a stit-theoretic analysis of responsiblity and excusability. In Section 5 we develop an axiomatic system for the resulting logic and address its soundness, completeness, and decidability results, after which we conclude.

Epistemic Deontic Stit
As discussed in [21], [13], and [1], an adequate theory of ought-to-do should account for agents' epistemic states before and at the moments of action. This is all the more relevant in contexts of responsibility attribution, and more specifically for excusability (see, for instance, [27]). In principle, if an agent does not know how to fulfill an obligation, it should be excused for not having done so. The mentioned [21], [13], and [1] all extend Horty's stit theory of act utilitarian ought-to-do with knowledge operators and explore the relation between uncertainty and obligation. In turn, here we will be extending the logics of [13] and [1] with modalities for belief. 1 Definition 1 (Language) Given a finite set Ags of agent names, a countable set of propositions P such that p ∈ P and α ∈ Ags, the grammar for the formal language L KO is given by: ϕ is meant to express the 'historical necessity' of ϕ (♦ϕ abbreviates ¬ ¬ϕ).
[α]ϕ stands for 'agent α has seen to it that ϕ.' K α is the epistemic operator for α, so that K α ϕ stands for 'agent α knows that ϕ holds.' ⊙[α]ϕ is meant to express that α objectively ought to have seen to it that ϕ. Finally, ⊙ S [α]ϕ is meant to express that α subjectively ought to have seen to it that ϕ.
As for the semantics, the structures on which we evaluate formulas of the language L KO are based on what we call epistemic act-utilitarian branching-time frames.  [7] for a discussion of the property).
• For α ∈ Ags, ∼ α is the epistemic indistinguishability equivalence relation for agent α, which satisfies the following constraints: ( • Value is a deontic function that assigns to each history h ∈ H a real number, representing the utility of h. As for the deontic dimension, objective ought-to-do's come from the optimal actions for an agent: to have seen to it that ϕ is taken to be an objective obligation of an agent at a given index iff ϕ is an effect of all the optimal actions for that agent at that index. The optimality of such actions is relative to a dominance ordering, and this ordering depends on the value of the histories in those actions (provided by Value). In order to present the semantics for formulas involving the ought-to-do operator, we therefore need some previous definitions.
For m ∈ M and β ∈ Ags, we define State m β = S ⊆ H m ; S = α∈Ags−{β } s(α), where s ∈ Select m . For α ∈ Ags and m * ∈ M, we first define a general ordering ≤ on P( The optimal set of actions is the set Optimal m * α := {L ∈ Choice m * α ; there is no L ′ ∈ Choice m * α such that L ≺ L ′ }. As for subjective ought-to-do's, they involve a dominance ordering as well, but one different to the one for objective ought-to-do's. To define this subjective dominance ordering, [13] introduces a new semantic concept known as epistemic clusters, which are nothing more than a given action's epistemic equivalents in indices that are indistinguishable to the one of evaluation. Formally, we have that Just as in the case of objective ought-to-do's, this ordering allows us to think about a subjectively optimal set of actions S − optimal m * α : Analogous to what we mentioned regarding objective ought-to-do's, the idea is that to have seen to it that ϕ is a subjective obligation of an agent at a given index iff it is an effect of all the subjectively optimal actions-and their epistemic equivalents-for that agent at that index.
As is customary, the models and the semantics for the formulas are defined by adding a valuation function to the frames of Definition 2: Definition 3 An eaubt-model M consists of the tuple that results from adding a valuation function V to a eaubt-frame, where V : P → 2 M×H assigns to each atomic proposition a set of moment-history pairs. Relative to a model M , the semantics for the formulas of L KOBO is defined recursively by the following truth conditions, evaluated at a given index m, h : Satisfiability, validity on a frame, and general validity are defined as usual. We write ϕ to refer to the

Introducing Beliefs
The logic presented in the previous section offers many benefits for addressing complex interactive situations. The common thread among these situations is that agentive knowledge is taken into consideration when deciding whether an agent is responsible for having brought about some circumstance (see Horty's coin-flip puzzles in [21] and [1]). However, we want to enhance the analysis by accounting for agents' belief-systems. As mentioned in the introduction, the beliefs that an agent has at a given index serve as justifications or explanations for a particular choice of action of said agent at said index.
In this work we adapt the arguments of [6] and formalize a notion of full belief. To clarify, an agent's full belief in the truth of a proposition means that the agent assigns probability 1 to the set of indices where the proposition is true. However, the typical logic of probabilistic full belief does not involve classical probability. The reason is that it is well known that classical measures yield problems for conditional beliefs and for belief revision. In classical-probability settings, conditioning on events with measure 0 is not defined and therefore "it is unclear how to proceed if an agent learns something to which she initially assigned probability 0" ( [18], see also [17], [38], and [10]). Since we want to incorporate to stit theory a paradigm of belief that allows for revision, we follow the method of [6] and use conditional probability as primitive. 2 Therefore, we build conditional-probability spaces upon the branching-time structures from Definition 3. To simplify the terminology-and just as done in [6]-we focus on finite discrete structures, for which every subset is measurable with respect to special two-place probability functions mapping pairs of subsets to values in [0, 1]. These functions underlie the semantics for formulas of conditional belief B ψ α ϕ, which are meant to be read as 'after learning ψ, agent α believes that ϕ was the case (before the learning).'

Definition 4 (Syntax with conditional-belief)
The grammar for the formal language L KOB (an extension of L KO ) is given by Definition 5 (Epistemic act-utilitarian discrete-conditional-probability branching-time frames) A finite epistemic act-utilitarian discrete-conditional-probability branching-time frame (dcpbt-frame for short)

Remark 1
In what follows, we will refer to any function q :  [38] and [17,Chapter 3]). This means that probability theory's typical definition of conditional probability in terms of a classical-probability function is a special instance of a vf-function.
Endowed with semantics for formulas involving conditional belief, we take plain (unconditional) belief to be represented by beliefs conditional on a tautology. Therefore, in what follows we write B α ϕ to denote B ⊤ α ϕ. With these formulas and the models they are evaluated on, we have extended the epistemic stit logic of Section 2 into a system that deals with both knowledge and belief. As pointed out in [5], [4], and [6], the truth conditions in Definition 5 yield a logic for which the knowledge operators validate the S5 schemata, the conditional-belief operators validate the K schema, and the following interaction schemata are valid: Additionally, the following axioms that regard revision are also valid: 4 Why account for belief revision? Well, in [18] Halpern argues that belief revision plays a critical role in the analysis of strategic reasoning in extensive-form games, and since the stit semantics for agency over branching-time structures can adopt most ideas of the theory of extensive-form games (see [23,Chapter 7], [15], and [2]), we believe that stit theory should also benefit from an account of conditional belief and of belief revision. There is a common idea that if a formalization of the temporal evolution of a game incorporates the assumption that players can change their beliefs about the game as it progresses due to some flow of information-for instance by drawing conclusions from opponent's moves-then the analysis of interactive situations becomes much richer ( [9]). 5 In stit theory, branching-time structures represent an exhaustive set of possibilities for temporal evolution according to multi-agent interaction, and a treatment of belief change allows for a description of how agents could have constrained those possibilities if they had learned information regarding past choices about which they are uncertain. For instance, in the example that we mentioned in the introduction, the doctor did not know that the patient had eaten before being admitted to the hospital, and moreover the doctor learned-from the mistaken chart-that the patient had not eaten. In principle, if the doctor had learned that the patient had in fact eaten, then her beliefs should have been different. In other words, she would revise her beliefs after learning that the patient had eaten before being admitted to the hospital. By incorporating conditional-belief modalities into stit theory, we can analyze both syntactically and semantically the different ways in which doxastic states can change according to the learning of information. In this way, we can formalize further the justification of choices of action that 4 Observe that the semantics for conditional belief implies that an agent's belief of ϕ given ψ is relative to the agent's epistemic state. In other words, we take it that conditional beliefs depend on the information available to the agent. 5 One can easily associate a belief-revision Kripke-structure to an extensive-form game to evaluate formulas that reflect agents' belief changes as the game "progresses" (see [9] for an illustration of such an association in the analysis of backward induction in extensive-form games). The typical way to do so is to think of full strategy profiles-functions that associate each node to a player's move (or strategy) at that node-as possible worlds, so that the formulas evaluated on these worlds "[...] describe the way the game is actually played, and they provide a set of counterfactuals for evaluating the payoffs if the action taken at any node deviates from the specified action." The evaluation of formulas at full strategy profiles is reminiscent of stit theory's use of histories as part of the indices of evaluation, but in extensive-form games one also considers profiles that cannot be realized in the structure of the game: regardless of whether the nodes can be reached in a play or not, the functions that serve as possible worlds map each node to a move (or strategy) that can be played at that node. It is this feature of the beliefrevision structure associated to an extensive-form game that makes conditional-belief modalities very useful. With the syntax of conditional-belief, we can represent the beliefs of an agent at a node that was actually reached in a play, by conditioning on formulas that ensure that such a node was reached. Although this feature of the language and the semantics of conditional belief could be very well exploited in the context of strategic stit theory ([23, Chapter 7]), here we propose that it is also relevant even in instantaneous-stit theory, namely due to agents' uncertainty across the set of indices. If an agent had uncertainty about the index of evaluation it found itself at (because of some lack of information), then the conditional-belief modalities allow us to reason syntactically about the counterfactual situation in which the agent's learning of such information would change its state of uncertainty. have moral consequences.

Introducing Doxastic Oughts
In keeping with EGT, we argue that agents can be seen as having a doxastic sense of what they ought to do in interactive situations, and that this sense can be traced back both to their beliefs regarding the index at which they are and to the utilities of the histories in their available actions. Rather than delving into the analyses of rationality and rational choice in terms of best responses (see [36] and [29] for surveys of such analyses), we use the concepts of utility and belief in order to characterize a doxastic sense of ought-to-do in stit theory. Here, utility and belief underlie the process by which the beliefs of an agent explain whether that agent was justified in making a particular choice of action. Again, this extension of deontic stit is important to treat the kind of problems in excusability and responsibility attribution that stit theory deals with ( [27]), as we will illustrate by analyzing the example presented in the introduction.
Our interpretation of belief rests upon probabilities assigned to the alternative histories of branchingtime structures. Inspired by the customary treatment of decision rules under uncertainty (or risk) from decision theory, 6 we identify an agent's doxastic sense of ought-to-do with the effects of actions that maximize expected (deontic) utility.
Expected utility theory has somewhat settled interpretations for the components of interactive decision making (see [34], [24], and [25]). Typically, the utilities of outcomes quantify agents' preferences, and the probabilities assigned are seen either as objective measures for the frequency with which sets of outcomes-the events-ensue or as subjective representations of agentive belief (see Footnote 6). As mentioned before, in the context of deontic stit based on act utilitarianism we interpret the value of a history-Value(h)-as its deontic utility for the whole group of agents, with no specific interpretation for the word 'utility.' This means that we do not identify the deontic utility of a history with agentive preference but rather allow for the assignment of values to "accommodate a variety of different approaches" (see Section 2.2 [23, Chapter 3]). The notion of deontic utility itself is taken as primitive in act utilitarian stit, and it is a general notion that applies to the whole set of agents-not only to individual ones. Therefore, it may be thought of-but not necessarily so-as the "total utility of the set of agents in that history, their average utility, or perhaps some distribution-sensitive aggregation of the utilities of these individual agents" ( [23], p. 38). As for the probabilities, it must be clear by now that we interpret them as a measure of the agents' individual doxastic state.  Our notion of expected deontic utility can be seen as a stit version of EGT's interpretation of an agent's expected utility for a given strategy, conditional on that agent's information. According to [29], in EGT an agent's expected utility for one of its strategies is calculated with respect to so-called conjectures. An agent's conjecture at a given world is a probability distribution on the set of all strategy profiles involving the other agents. Such a distribution is typically based on probabilities conditional either on the agent's strategy-choice at the world of evaluation or on the agent's information set at said world ( [29]). Our framework differs from EGT's in three essential points: (1) we do not have individual utilities for each outcome; (2) in our structures, each possible world (which we refer to as an index) has a deontic utility, whereas in EGT only outcomes-or full strategy profiles-have utilities; and (3) while EGT regards information sets as subsets of the available strategies, we do not impose this condition-in fact, the semantic condition (OAC) that we adopt yields that information sets are unions of choice cells.
Since dcpbt-models are finite, we have that for every m ∈ M and h ∈ H m , the set {EU m,h α (L); L ∈ Choice m α } has a maximum. Therefore, there are actions that maximize α's expected deontic utility at every index, namely the ones whose expected deontic utility is the same as said maximum. We denote by EU We use the same dcpbt-models from Definition 5 to evaluate the formulas of L KOBO . The truth conditions are the same as before, with the following additional clause: In other words, at a given index it was the case that an agent doxastically ought to have seen to it that ϕ iff ϕ is an effect both of all the actions that maximized the agent's expected deontic utility at said index and of the epistemic equivalents of these actions.

Example
In order to illustrate the reach of the semantics introduced above, we present a formal analysis of the example in the introduction, using dcpbt models.
Example 1 Let Ags = {patient, doctor}. Let M and ⊏ be defined so as to be represented by the diagram in Figure 1. We have three moments (m 1 − m 3 ) and four histories (h 1 − h 4 ). These histories represent the different possibilities in which time may have evolved according to the actions available both to patient and doctor. The actions available to patient at moment m 1 are E 1 , which we interpret as the action of refusing to eat, and E 2 , which we interpret as the action of eating. It is according to such actions that time progressed either into moment m 2 or into moment m 3 . At both these moments, doctor chose from her available actions and executed one of them. At moment m 2 , the actions available to doctor are L 1 , which we interpret as the action of supplying anesthetics, and L 2 , which we interpret as the action of 7 Formally, our definition of expected deontic utility is in fact an instance of probability theory's conditional expectation with respect to an event-albeit in the setting where conditional probability is primitive. In this case, the so-called event is the information set of a given agent at the index of evaluation. Thus, if L is an available action for an agent at index m, h , and if E denotes the expected value of the random variable Value with respect to µ α (·|H) (where we recall that H is the set of all histories), then EU refusing to supply anesthetics. Similarly, at moment m 3 the actions available to doctor are L 3 , which we interpret as the action of supplying anesthetics, and L 4 , which we interpret as the action of refusing to supply anesthetics.
We model the utilities of the outcomes according to the statement of the example. Therefore, history h 1 , where at m 1 patient refused to eat and at m 2 doctor supplied the anesthetics, gets the highest utility-Value(h 1 ) = 1-due to the fact that such a history represents the situation in which the patient got ready for the surgery without any trouble. Histories h 2 and h 4 get a neutral utility of 0: both of them imply that doctor refused to supply anesthetics and thus the patient is not ready for the surgery. History h 3 , on the other hand, gets a negative utility of −1, since it implies that at m 1 patient ate and at m 3 doctor supplied the anesthetics, leading to patient's death. As implied by the statement of the example, we take h 3 to be the actual history.
The epistemic-doxastic states and ought-to-do's that we focus on are those of doctor, since they illustrate important semantic properties of our logic. We represent doctor's epistemic states with blue dashed lines, so that at both m 2 and m 3 , along every history running through them, doctor did not know whether the patient had eaten or not, but she knew which action she performed. The doxastic states of doctor are represented by the conditional-probability function µ doctor , given by the following rules. Let  Let e denote the atomic proposition 'the patient has eaten,' let a denote the atomic proposition 'anesthetics are supplied to the patient,' let r denote the atomic proposition 'the patient is ready for surgery,' and let d denote the atomic proposition 'the patient will die.' According to Definition 5, these atomic propositions and the formulas that are recursively built with them can be taken as true or false depending on the index of evaluation. For instance, we model the example so that at index m 2 , h 1 it was the case that patient ate, that doctor supplied the anesthetics, and that patient became ready for surgery. (M , m 2 , h 1 |= e ∧ a ∧ r).
As for the evaluation of formulas involving the basic stit-theory operators, observe that some instances of it are M , m 2 , h 1 |= e (at this index it was the case that it was settled that the patient did not eat), M , m 3  As for formulas involving the deontic operators, we first observe that a) (at the actual index it was the case that if the doctor had learned that the patient had not eaten (as she did by the mistake in the chart), then she would have fully believed that the patient had not eaten and that she objectively ought to have supplied the anesthetics.) Coupled with the fact that doctor did not know that patient had in fact eaten, the satisfaction of these last two formulas at the actual index should in principle provide a good reason for excusing doctor of actually having caused patient's death.

Axiomatization and Logic Properties
Since one of the main contributions of the present paper is the introduction of doxastic oughts, we review some of the properties of the semantics for formulas involving the operator ⊙ B [α]. First of all, we must say that this modal operator yields a KD45 logic. Secondly, the doxastic sense of ought validates a version of Kant's imperative ought implies can, as explained by the fact that the following formula is valid with respect to the class of dcpbt models: ⊙ B [α]ϕ → ♦K α ϕ. We also have that if an agent doxastically ought to have seen to it that ϕ, then the agent knows that this is settled-the formula In order to further the understanding of our logic, we present a sound, complete, and decidable proof system for it.
Definition 8 (Proof system) Let Λ be the proof system defined by the following axioms and rules of inference: • (Axioms) All classical tautologies from propositional logic. The S5 axiom schemata for , [α], K α . The following axioms and schemata for the interactions of formulas with the given operators: (Oic) For n ≥ 1 and pairwise different α 1 , . . . , α n ,

• (Rules of inference) Modus Ponens, Substitution, and Necessitation for all modal operators.
In the Appendix of this work, we discuss all these axioms and schemata, and we show that the proof system Λ is sound and complete with respect to a class of models that are more general than the ones introduced in Definition 5. These models differ from dcpbt-models in two main qualities: (1) following [1], they are multi-valued to the extent that instead of only one deontic value function, they have three: one for the objective ought-to-do's, one for the subjective ones, and one for the doxastic ones; and (2) they are Kripke-structures based on domains of possible worlds. 8 The proof of completeness in the Appendix also shows that Λ is decidable. This is a consequence of the logic's finite model property, which is shown through obtaining a finite canonical model using arguments typical of modal filtrations.
All these results become relevant in a specific line of research where proof systems of deontic logic are intended to help in the testing of ethical behavior of AI through theorem-proving and model-checking (see [3], [28], [11]).
Unfortunately, the Appendix is too long to include it here. Therefore, the reader can only find it at https://www.researchgate.net/publication/351656805_Appendix.

Conclusion
"The performance is sometimes masterful, extremely clever, but the control of the actions, their source, is deranged and depends on various morbid impressions," says the character Zossimov, in Dostoevsky's Crime and Punishment. From the discussions that appear in this paper, it is clear that what agents know and what they believe at the moment of acting-as well as the obligations that arise according to these knowledge and beliefs-can be interpreted as "sources" of their actions, as some of those "impressions" on which agency depends that Zossimov speaks about.
The main novelty of the present, logic-based, treatment of these "sources" of agency lies in the incorporation of beliefs into deontic stit theory. The relation between (a) a given agent's doxastic state, (b) the actions that are available to said agent at some point of time, and (c) the deontic utility of such actions, gives us the opportunity to reason about a sense of agentive obligation that is based on the idea of maximizing expected deontic utility. Thus, we end up with a reasonable measure for explaining why agents could have favored certain actions over others, something that is useful in formal analyses of responsibility attribution, for instance.
A prominent feature of our analysis is the use of conditional beliefs. We mentioned that, since stit theory's account of interactive scenarios would greatly benefit from adopting viewpoints typical of EGT and of epistemic logic, we wanted to introduce a notion of belief that would satisfactorily open up possibilities for belief revision. It must be said, then, that the example discussed in Section 4 does not make heavy use of the theory of belief revision underlying the probabilistic semantics of belief that we introduced. Although this was a choice made more for the sake of simplicity than anything else, it is true that the logic presented here is rather a 'first step' toward an appropriate theory of belief-based action and obligation-a theory that would admit revision in both the categories of beliefs and obligations. A very interesting problem for future work along these lines, then, regards implementing the ideas of belief revision-in terms of conditional belief-to formalize conditional doxastic oughts. The basic intuition is that, if at some index an agent has learned that ψ is the case, then the doxastic obligations that such an agent had at the index should in principle be subject to the revision with ψ-just as beliefs are. Formulas of the form ⊙ B [α] ψ ϕ could then capture these revised doxastic oughts, such that possible semantics for these formulas could depend on the restriction of the model's domain to indices where ψ holdsjust as happens for the version of conditional belief discussed in this paper. In fact, one can find good pointers in this respect in [23,Chapter 4], since a stit-theoretic account of conditional ought-to-do's is presented there. An adequate axiomatization of such possible conditional doxastic oughts, however, is still a complicated open problem.
In conclusion, this work deals with important questions in the modeling of agency, knowledge, belief, and obligation. We presented logic-based characterizations of these concepts, that allowed us to devise unequivocal representations of interactive scenarios, where agents within an environment choose courses of action through time and where those choices could be traced back both to the epistemic-doxastic states of the agents and to different senses of obligation. The logic developed here lays the groundwork for interesting future research, and there is still plenty of work to do.