Abstract
In this paper, we present a comprehensive modeling technique for bounded Petri net systems (BPNSs) in the framework of the semi‐tensor product (STP) of matrices. The two dynamic properties of BPNSs, namely, reachability and controllability, are investigated systematacially. First, the dynamics of a bounded Petri net system (BPNS), by resorting to the STP of matrices, are expressed in the form of a discrete‐time bilinear equation, which is called the marking evolution equation (MEE) of BPNSs. Second, controllability and transition‐marking adjacency matrix (TMAM) of BPNSs are defined, respectively. Further, several necessary and sufficient conditions for reachability and controllability of BPNSs are given in terms of the MEE and TMAM. Third, an efficient algorithm to verify reachability property of BPNSs, in this paper, is provided, as well as its computational complexity. Finally, an example is presented to illustrate the theoretical results in this paper. The main contribution of this paper is the presentation of a precise mathematical model for BPNSs. The main advantage of the proposed approach is that not only it can be applied to verify whether or not any given marking is reachable from the other in state space, but also it is very convenient to find all firing sequences between any two reachable markings.