Correctness Verification of E-Commerce Taxation Systems Using Mobile-Agent-Oriented Petri Nets

This paper shows how Mobile-Agent-oriented Petri nets (MAPNs) can be used to specify and analyze a mobile-agent-based e-commerce taxation system. Both the dynamical behavior of the system and the causality between events can be explicitly described by MAPNs. The functional correctness of the system, such as the reachability and the coverability, is formally verified by attaching agents' attributes to the tokens of the classical Petri nets. The application instance in this paper demonstrates that MAPNs can provide more information and be more helpful in the design and analysis of business processes based on mobile agents.