Indian Journal of Science and Technology

The PDF file you selected should load here if your Web browser has a PDF reader plug-in installed (for example, a recent version of Adobe Acrobat Reader).

If you would like more information about how to print, save, and work with PDFs, Highwire Press provides a helpful Frequently Asked Questions about PDFs.

Alternatively, you can download the PDF file directly to your computer, from where it can be opened using a PDF reader. To download the PDF, click the Download link above.

Fullscreen Fullscreen Off


Background: Software agents are expected to work autonomously and deal with unfamiliar situations astutely. Achieving cent percent test case coverage for these agents has always been a problem due to limited resources. Also a high degree of dependability is expected from autonomous software agents. Formal verification of these systems can be done by specifying the possible actions of the agents to increase the confidence in the correctness of such systems. Methods: We have used social approach of agent communication where actions of the agents are described as social obligation between the participants. Formal specification of e-agents was done using μ-calculus as it is more expressive than Linear Temporal Logic (LTL). An algorithm has been given for syntactic conversion of μ-calculus formulas to TAPA model checker environment. Results: Using converstion algorithm syntactically modified μ-calculus formulas will be executed on TAPA model checker to verify the system being modelled for the specified properties. Application: The study will help to provide future directions for formal modelling of e-agents for their correct functioning.

Keywords

Agent Communication, Model Checking, μ-Calculus, μ TAPA Model Checker
User