Verifying Dribble Agents

Abstract. We describe a model-checking based approach to verification of programs written in the agent programming language Dribble. We define a logic (an extension of the branching time temporal logic CTL) which describes transition systems corresponding to a Dribble program, and show how to express properties of the agent program in the logic and how to encode transition systems as an input to a model-checker. We prove soundness and completeness of the logic and a correspondence between the operational semantics of Dribble and the models of the logic.

• Type: Conference
• Year: 2009
• Where: DALT
• Authors: Doan Thu Trang, Brian Logan, Natasha Alechina
• Keywords: DALT 2009, Logic, Programming Language Dribble, Temporal Logic Ctl