A reduction method of analyzing data-liveness and data-boundedness for a class of E-commerce business process nets

Abstract

E-commerce Business Process Nets (EBPNs for short) are a novel formal model of describing and verifying e-commerce business processes with multiple interactive parties. They can well reflect some behavior-security properties such as data-live and data-boundedness. However, the problem of effectively analyzing EBPNs remains largely open since data are considered in them. In this paper, a class of EBPNs called S-graph-Reducible EBPN (RENS for short) is defined. Some restrictions are set on the structure of a RENS and thus each RENS can be reduced to a marked S-graph. We prove that a RENS and the related marked S-graph are equivalent on behaviors. Thus, the properties of RENS such as data-liveness, data-boundedness, and reachability can be analyzed easily based on the methods applied in the marked S-graphs.