||Model Checking Jason Programs
||Villadsen, Jørgen (Algorithms and Logic, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
||Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
||Agent-Oriented Programming (AOP) is a relatively new paradigm used for developing multi-agent systems. Within this paradigm agents are often described
using the Belief-Desire-Intention model (BDI).
This report focuses on developing a system for verification of programs written in
Jason, which is a Java-based interpreter for an extended version of the language
AgentSpeak is build around the BDI model and is a high level programming
language for developing intelligent agents. This is done with concepts like beliefs,
goals and plans.
When describing the properties to be verified we use an extension of the branching-
time temporal logic CTL (Computation Tree Logic) which makes it possible to
reason about BDI properties over time.
A formal semantics for the language will be used to make a procedure that
generates transitions systems representing the programs to be verified. Then a
model checking algorithm will be applied to these transition systems to verify
that some given program properties holds in all possible states of the programs.
||Technical University of Denmark (DTU) : Kgs. Lyngby, Denmark
Creation date: 2010-06-30
Update date: 2010-06-30