A refinement framework for autonomous agents

Li, Qin and Smith, Graeme (2013). A refinement framework for autonomous agents. In: Juliano Iyoda and Leonardo de Moura, Formal Methods: Foundations and Applications. 16th Brazilian Symposium: Proceedings. SBMF 2013: 16th Brazilian Symposium on Formal Methods, Brasilia, Brazil, (163-178). 29 September-4 October, 2013. doi:10.1007/978-3-642-41071-0_12


Author Li, Qin
Smith, Graeme
Title of paper A refinement framework for autonomous agents
Conference name SBMF 2013: 16th Brazilian Symposium on Formal Methods
Conference location Brasilia, Brazil
Conference dates 29 September-4 October, 2013
Proceedings title Formal Methods: Foundations and Applications. 16th Brazilian Symposium: Proceedings   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2013
Sub-type Fully published paper
DOI 10.1007/978-3-642-41071-0_12
ISBN 9783642410703
9783642410710
ISSN 0302-9743
1611-3349
Editor Juliano Iyoda
Leonardo de Moura
Volume 8195
Start page 163
End page 178
Total pages 16
Chapter number 12
Total chapters 16
Collection year 2014
Language eng
Formatted Abstract/Summary
An autonomous agent is one that is not only directed by its environment, but is also driven by internal motivation to achieve certain goals. The popular Belief-Desire-Intention (BDI) design paradigm allows such agents to adapt to environmental changes by calculating a new execution path to their current goal, or when necessary turning to another goal. In this paper we present an approach to modelling autonomous agents using an extension to Object-Z. This extension supports both data and action refinement, and includes the use of LTL formulas to describe an agent’s desire as a sequence of prioritised goals. It turns out, however, that the introduction of desire-driven behaviour is not monotonic with respect to refinement. We therefore introduce an additional refinement proof obligation to enable the use of simulation rules when checking refinement.
Keyword Autonomous agents
BDI agents
Refinement
Object-Z
Temporal logic
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 15 Oct 2013, 05:22:32 EST by Graeme Smith on behalf of School of Information Technol and Elec Engineering