 Next there is Rao &amp; Georgeff’s formalization of BDI agents using the branching-time temporal logic CTL (Rao and Georgeff 1991, Rao and Georgeff 1998, Wooldridge 2000). On top of CTL they introduce modal operators for Belief \((\lbel)\), Goal \((\lgoal)\) (sometimes replaced by Desire \((\ldes)\)) and Intention (of the to_be kind, \(\lintend\)) as well as operators to talk about the success \((\lsucceeded(e))\) and  failure \((\lfailed)\) of elementary actions \(e\). So they do not try to define intention in terms of other notions, but rather introduce intention as a separate operator, of which the meaning is later constrained by ‘reasonable’ axioms. The formal semantics is based on Kripke models with accessibility relations between worlds for the belief, goal and intention operators. However, possible worlds here are complete time trees (modeling the various behaviors of the agent) on which CTL formulas are interpreted in the usual way. Next they propose a number of postulates/axioms that they find reasonable interactions between the operators, and constrain the models of the logic accordingly so that these axioms become validities. For example, they propose the formulas \(\lgoal(\alpha) \rightarrow \lbel(\alpha)\) and \(\lintend(\alpha) \rightarrow \lgoal(\alpha)\), for a certain class of formulas \(\alpha\), of which \(\alpha = \mathop{\mathbf{E}}(\psi)\) is a typical example. Here \(\mathop{\mathbf{E}}\) stands for the existential path quantifier in CTL. Rao and Georgeff also show that one can express commitment strategies in their logic. For example, the following expresses a ‘single-minded committed’ agent, that keeps committed to its intention until it believes it has achieved it or thinks it is impossible (which is very close to what we saw in the definition of intention in the approach of Cohen and Levesque):