Model-checking agent refinement

We present a proof-technique for reducing the nondeterminbstract agent specifications in a BDI framework by means of refinement. We implement the operational semantics of agent specifications in rewrite systems such that we can automatically check if refinement between (fair) executions of agents holds. Categories and Subject Descriptors: I.6.5 Model Development: Modeling methodologies General Terms: Languages, Theory, Verification.

• Type: Conference
• Year: 2008
• Where: ATAL
• Authors: Lacramioara Astefanoaei, Frank S. de Boer
• Keywords: Agent Specifications, ATAL 2008, BDI Framework, Intelligent Agents, Nondeterminbstract Agent Specifications