Formal Specification and Verification of Real-Time Multi-Agent Systems using Timed-Arc Petri Nets

Abstract

In this study we have formally specified and verified the actions of communicating real-time software agents (RTAgents). Software agents are expected to work autonomously and deal with unfamiliar situations astutely. Achieving cent percent test cases coverage for these agents has always been a problem due to limited resources. Also a high degree of dependability and predictability is expected from real-time software agents. In this research we have used Timed-Arc Petri Net's for formal specification and verification. Formal specification of e-agents has been done in the past using Linear Temporal Logic (LTL) but we believe that Timed-Arc Petri Net's being more visually expressive provides a richer framework for such formalism. A case study of Stock Market System (SMS) based on Real Time Multi Agent System framework (RTMAS) using Timed-Arc Petri Net's is taken to illustrate the proposed modeling approach. The model was verified used AF, AG, EG, and EF fragments of Timed Computational Tree Logic (TCTL) via translations to timed automata.