Time, Knowledge, and Choice

Abstract. This article considers the link between theory and practice in agentoriented programming. We begin by rigorously defining a new formal specification language for autonomous agents. This language is the expressive branching time logic CTL   , enriched by the addition of two further modal connectives, for representing knowledge and seeing to it that (stit). These connectives are grounded: given a concrete semantics in terms of the states and actions of an agent. This grounding makes it possible to establish a precise relationship between the specification language and deterministic automata, and in particular, the automatic synthesis of agents from logical specifications becomes a possibility. This possibility, and the potential problems associated with it, are discussed at length. The paper closes with a summary of future research issues and directions.

• Type: Conference
• Year: 1995
• Where: ATAL
• Authors: Michael Wooldridge
• Keywords: ATAL 1995, Formal Specification Language, Intelligent Agents, Specification Language, Time Logic Ctl