Verifying Dribble Agents

14 years 4 days ago
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.
Doan Thu Trang, Brian Logan, Natasha Alechina
Added 24 Jul 2010
Updated 24 Jul 2010
Type Conference
Year 2009
Where DALT
Authors Doan Thu Trang, Brian Logan, Natasha Alechina
Comments (0)