\input zb-basic
\input zb-ioport
\iteman{io-port 05665717}
\itemau{Trang, Doan Thu; Logan, Brian; Alechina, Natasha}
\itemti{Verifying dribble agents.}
\itemso{Baldoni, Matteo (ed.) et al., Declarative agent languages and technologies VII. 7th international workshop, DALT 2009, Budapest, Hungary, May 11, 2009. Revised selected and invited papers. Berlin: Springer (ISBN 978-3-642-11354-3/pbk). Lecture Notes in Computer Science 5948. Lecture Notes in Artificial Intelligence, 244-261 (2010).}
\itemab
Summary: 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.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-11355-0\_15}
\end