Beta 1

Title Model Checking Jason Programs
Author Vester, Steen
Supervisor Villadsen, Jørgen (Algorithms and Logic, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Bachelor thesis
Year 2010
Abstract 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. 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.
Imprint Technical University of Denmark (DTU) : Kgs. Lyngby, Denmark
Series IMM-B.Sc.-2010-28
Original PDF bac10_28_net.pdf (0.67 MB)
Admin Creation date: 2010-06-30    Update date: 2010-06-30    Source: dtu    ID: 264329    Original MXD