Toward a Model Theory of Actions: How Agents do it in Branching Time

A clear understanding and formalization of actions is essential to computing, and especially so to reasoning about and constructing intelligent agents. Several approaches have been proposed over the years. However, most approaches concentrate on the causes and effects of actions, but do not give general characterizations of actions themselves. A useful formalization of actions would be based on a general, possibly nondiscrete, model of time that allows branching (to capture agents' choices). A desirable formalization would also allow actions to be of arbitrary duration and would permit multiple agents to act concurrently. We develop a branching-time framework that allows great flexibility in how time and action are modeled. We motivate and formalize several coherence constraints on our models, which capture some nice intuitions and validate some useful inferences relating actions with time.