Verifying Dribble Agents

Trang Doan; Brian Logan; Natasha Alechina

doi:10.1007/978-3-642-11355-0_15

Verifying Dribble Agents

Trang Doan, Brian Logan, Natasha Alechina

University of Nottingham

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

1 Citation (Scopus)

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.

Original language	English
Title of host publication	Declarative Agent Languages and Technologies VII
Subtitle of host publication	7th International Workshop, DALT 2009, Budapest, Hungary, May 11, 2009. Revised Selected and Invited Papers
Editors	Matteo Baldoni, Jamal Bentahar, M. Birna van Riemsdijk, John Lloyd
Publisher	Springer Nature
Pages	244-261
Number of pages	18
ISBN (Electronic)	978-3-642-11355-0
ISBN (Print)	978-3-642-11354-3
DOIs	https://doi.org/10.1007/978-3-642-11355-0_15
Publication status	Published - 2009
Externally published	Yes
Event	International Workshop on Declarative Agent Languages and Technologies - Budapest, Hungary Duration: 11 May 2009 → 11 May 2009 Conference number: 7

Publication series

Name	Lecture Notes in Computer Science
Volume	5948

Conference

Conference	International Workshop on Declarative Agent Languages and Technologies
Abbreviated title	DALT 2009
Country/Territory	Hungary
City	Budapest
Period	11/05/09 → 11/05/09

Access to Document

10.1007/978-3-642-11355-0_15

Cite this

Doan, T., Logan, B., & Alechina, N. (2009). Verifying Dribble Agents. In M. Baldoni, J. Bentahar, M. B. van Riemsdijk, & J. Lloyd (Eds.), Declarative Agent Languages and Technologies VII: 7th International Workshop, DALT 2009, Budapest, Hungary, May 11, 2009. Revised Selected and Invited Papers (pp. 244-261). ( Lecture Notes in Computer Science ; Vol. 5948). Springer Nature. https://doi.org/10.1007/978-3-642-11355-0_15

Verifying Dribble Agents. / Doan, Trang; Logan, Brian; Alechina, Natasha.
Declarative Agent Languages and Technologies VII: 7th International Workshop, DALT 2009, Budapest, Hungary, May 11, 2009. Revised Selected and Invited Papers. ed. / Matteo Baldoni; Jamal Bentahar; M. Birna van Riemsdijk; John Lloyd. Springer Nature, 2009. p. 244-261 ( Lecture Notes in Computer Science ; Vol. 5948).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

Doan, T, Logan, B & Alechina, N 2009, Verifying Dribble Agents. in M Baldoni, J Bentahar, MB van Riemsdijk & J Lloyd (eds), Declarative Agent Languages and Technologies VII: 7th International Workshop, DALT 2009, Budapest, Hungary, May 11, 2009. Revised Selected and Invited Papers. Lecture Notes in Computer Science , vol. 5948, Springer Nature, pp. 244-261, International Workshop on Declarative Agent Languages and Technologies, Budapest, Hungary, 11/05/09. https://doi.org/10.1007/978-3-642-11355-0_15

Doan T, Logan B, Alechina N. Verifying Dribble Agents. In Baldoni M, Bentahar J, van Riemsdijk MB, Lloyd J, editors, Declarative Agent Languages and Technologies VII: 7th International Workshop, DALT 2009, Budapest, Hungary, May 11, 2009. Revised Selected and Invited Papers. Springer Nature. 2009. p. 244-261. ( Lecture Notes in Computer Science ). doi: 10.1007/978-3-642-11355-0_15

Doan, Trang ; Logan, Brian ; Alechina, Natasha. / Verifying Dribble Agents. Declarative Agent Languages and Technologies VII: 7th International Workshop, DALT 2009, Budapest, Hungary, May 11, 2009. Revised Selected and Invited Papers. editor / Matteo Baldoni ; Jamal Bentahar ; M. Birna van Riemsdijk ; John Lloyd. Springer Nature, 2009. pp. 244-261 ( Lecture Notes in Computer Science ).

@inproceedings{8912bcb14c434b9e972d6edfa3e31e54,

title = "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.",

author = "Trang Doan and Brian Logan and Natasha Alechina",

year = "2009",

doi = "10.1007/978-3-642-11355-0_15",

language = "English",

isbn = "978-3-642-11354-3",

series = " Lecture Notes in Computer Science ",

publisher = "Springer Nature",

pages = "244--261",

editor = "Baldoni, {Matteo } and Bentahar, {Jamal } and {van Riemsdijk}, {M. Birna } and { Lloyd}, John",

booktitle = "Declarative Agent Languages and Technologies VII",

address = "United Kingdom",

note = "International Workshop on Declarative Agent Languages and Technologies, DALT 2009 ; Conference date: 11-05-2009 Through 11-05-2009",

}

TY - GEN

T1 - Verifying Dribble Agents

AU - Doan, Trang

AU - Logan, Brian

AU - Alechina, Natasha

N1 - Conference code: 7

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-11355-0_15

DO - 10.1007/978-3-642-11355-0_15

M3 - Conference proceeding

SN - 978-3-642-11354-3

T3 - Lecture Notes in Computer Science

SP - 244

EP - 261

BT - Declarative Agent Languages and Technologies VII

A2 - Baldoni, Matteo

A2 - Bentahar, Jamal

A2 - van Riemsdijk, M. Birna

A2 - Lloyd, John

PB - Springer Nature

T2 - International Workshop on Declarative Agent Languages and Technologies

Y2 - 11 May 2009 through 11 May 2009

ER -

Verifying Dribble Agents

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this