Logic and Computation introductory course:
Logics and Agent Programming Languages
Keywords: agent programming languages, logical models of agency, verificationAbstract:
To create a language for programming entities capable of intelligent behaviour (`agents'), researchers and developers must address deep questions such as: what are the basic constituent parts of an intelligent agent; how should the agent `think' (e.g., which deliberation strategy should it employ -- should it plan a precise sequence of actions in advance or should it adopt an abstract plans with gaps `to be filled-in later'); what relationship should there be between the agent's beliefs and its goals, etc. In seeking to address these questions, researchers have drawn heavily on formal models of agents and on agent logics, including epistemic logics, logics of action, dynamic logic, coalition logics etc. For example, the development of agent programming languages such as AgentSpeak were heavily influenced by the BDI (Beliefs, Desires and Intentions) logics developed to understand what an agent's behaviour should be. These interactions have resulted in an extremely fruitful cross fertilisation between work in logic and computation, and the application of logical techniques to address key practical issues such as the verification of agent programs (i.e., will an agent program meet the specification set out by its developers).
This course will address key topics in logics of agent programs including: the Belief Desire Intention model; overview of agent programming languages based on the BDI model; relationship between the operational semantics of BDI-based agent programming languages and logics for reasoning about agents' beliefs and intentions; verification of agent programs using model checking and theorem proving. The course assumes some exposure to modal logic, but no prior knowledge of agent programming languages is required.