Verifying Dribble Agents

Trang Doan, Brian Logan, Natasha Alechina

Research output: Chapter in Book/Report/Conference proceedingConference proceedingpeer-review

1 Citation (Scopus)


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.
Original languageEnglish
Title of host publicationDeclarative Agent Languages and Technologies VII
Subtitle of host publication7th International Workshop, DALT 2009, Budapest, Hungary, May 11, 2009. Revised Selected and Invited Papers
EditorsMatteo Baldoni, Jamal Bentahar, M. Birna van Riemsdijk, John Lloyd
PublisherSpringer Nature
Number of pages18
ISBN (Electronic)978-3-642-11355-0
ISBN (Print)978-3-642-11354-3
Publication statusPublished - 2009
Externally publishedYes
EventInternational Workshop on Declarative Agent Languages and Technologies - Budapest, Hungary
Duration: 11 May 200911 May 2009
Conference number: 7

Publication series

Name Lecture Notes in Computer Science


ConferenceInternational Workshop on Declarative Agent Languages and Technologies
Abbreviated titleDALT 2009


Dive into the research topics of 'Verifying Dribble Agents'. Together they form a unique fingerprint.

Cite this