A Logical Model of Intention and Plan Dynamics

Abstract. We propose a formal semantics of intention and plan dy-namics based on the notion of local assignment. The function of a local assignment is to change the truth value of a given proposition at a specific time point along a history. We combine a static modal logic including a temporal modality and modal operators for mental attitudes belief and choice, with three kinds of dynamic modalities and corresponding three kinds of local assignments operating on an agent’s beliefs, on the agent’s choices and on the physical world. An agent’s intention is defined in our approach as the agent’s choice to perform a given action at a certain time point in the future and two operations called intention generation and intention reconsideration are defined as specific kinds of local assignments on choices. In Sec-tion 1 we introduce a static logic of time, action, and mental attitudes. In Section 2 we add the dynamic notion of local assignment to the logic of Section 1. In Section 3, we focus on two specific kinds of local assignment on choice which allow to model the processes of intention and plan generation and reconsideration. 1 A logic of time, action and mental attitudes Let N be the set of non negative integers. Let ATM Fact = {f1, f2,...} be a nonempty finite set of atoms denoting facts, and ATMAct = {α, β,...} be a nonempty finite set of atoms denoting actions. The atom α stands for ‘the agent performs a certain action α’. We define ATM = ATM Fact ∪ATMAct to be the set of atomic formulae. The language L of the logic L is the set of formulae de-fined by the following BNF: ϕ:: = p | ¬ϕ | ϕ ∨ ϕ | [B]ϕ | [C]ϕ | ©ϕ where p ranges over ATM. The three operators of our logic have the following reading: [B]ϕ means ‘the agent believes that ϕ’, [C]ϕ means ‘the agent has chosen ϕ ’ (or ‘the agent wants ϕ to be true’), and©means ‘ϕwill be true in the next state, if no event affecting the world occurs’. The operator© describes the passive/inertial evolution of the world, that is, how the world evolves over time when no event affecting it occurs. Operators of the form [C]ϕ have been studied in the past by [1, 2, 3]. We write ©nϕ to indicate that the sentence ϕ is subject to n iterations of the modality © where n ∈ N. The following abbreviation defines the concept of intention for every α ∈ ATMAct and n ∈ N: In(α) de