Identification of labeled Petri nets from finite automata

Automata and Petri nets are two typical models of discrete event systems. The paper studies the problem of converting a finite automaton into a Petri net that satisfies the specified structural features. More specifically, we identify a labeled Petri net from a nondeterminstic finite automaton such that the reachability graph of the identified net is isomorphic to the given automaton, meaning that the Petri net models exactly the same dynamic system as the automaton. The identified net necessarily satisfies the specified structural requirements, such as the numbers of places and transitions, absence of self-loops, the exact structure of a part of the net, and so on. Since label Petri nets and nondeterminstic finite automata are generalizations of Petri nets and deterministic finite automata, respectively, the proposed approach can identify a larger spectrum of Petri nets and effectively handle the nondeterminstic cases in the given automaton. Four kinds of conditions are first extracted from the given automaton, namely deterministic enabling conditions, nondeterministic enabling conditions (i.e., multiple transitions with the same label are enabled simultaneously at a marking), transition disabling conditions, and marking inequality conditions. Then, an integer linear programming problem is formulated by characterizing these four kinds of conditions using integer linear constraints. A labeled Petri net satisfying the structural requirements is obtained by solving the integer linear programming problem. We also present two examples to show the possible applications of the proposed identification approach.