400
IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, VOL. 16, NO. 4, AUGUST 2000
Behavior Relations in Synthesis Process of Petri Net Models
Huaiqing Wang, Changjun Jiang, and Shaoyi Liao
Abstract—System synthesis is one of the most important issues in automatic control. In a synthesis process, local system properties must be preserved in the global system. Most of the previous researches focuses on such properties as liveness, reachability, reversibility, and so forth. However, little has been done on system behaviors, that is, the language of firing sequences. In this paper, we study the behavior of systems using the Petri net model synthesis, with self-loop inhibitor, as well as synchronization operations. A new system behavior property, behavior invariance, is defined. Self-loop and inhibitor operations are transformed into synchronization operations, under which a set of preservation conditions for behavior invariance are obtained. The theoretical foundation for the preservation of system behavior properties is presented and proved, and the applicability of the theory to real-world automation systems demonstrated. An example for modeling a superelevated conveyor is discussed, illustrating the usefulness of the proposed theory in modeling and analyzing the behavior invariance of such a conveyor. Index Terms—Behavior modeling, Petri nets, system analysis, system synthesis.
I. INTRODUCTION NTIL recently, Petri nets (PN’s) have been the de-facto choice of a tool for modeling discrete concurrent systems. The reasons are as follows. 1) A PN depicts systems lively and directly with a net graph and flow marking to express system dynamic properties. 2) Many common and important phenomena, such as concurrence, conflicts, synchronization, and nonsynchronization, can be expressed in a concise and unambiguous fashion. 3) A PN itself has a theoretical basis which provides a powerful method to analyze and verify system models. 4) A PN is suitable for modeling different system aspects, such as logic, time, and stochastic. Therefore, PN has found extensive applications to system modeling and analyzing in many research areas. With the rapid increase of system complexity, however, the numbers of structures and states involved in the PN system models are becoming prohibitively large. This enormous complexity has resulted in
U
Manuscript received October 15, 1998; revised April 13, 1999 and November 16, 1999. This paper was recommended for publication by Associate Editor M. Zhou and Editor N. Viswanadham upon evaluation of the reviewers’ comments. This work was supported by the Hong Kong Government under Grant 9040451 and Grant 7000840 and the PRC Natural Science Foundation Project under Grant 69973029. The authors are with the Department of Information Systems, City University of Hong Kong, Kowloon, Hong Kong (e-mail: iswang@cityu.edu.hk; isliao@cityu.edu.hk). Publisher Item Identifier S 1042-296X(00)06948-2.
serious problems in the system analysis, simulation, and evaluation, which have been dealt with by many researchers. Brand and Kopainski [1] proposed some principles and engineering specifications of PN modeling for concurrent logical control systems. Suzuki and Murata [4] described the hierarchical design methods for complex systems and discussed their liveness, boundedness, reversibility, and fairness properties. Some authors proposed system combination design methods. For example, Jun and DiCesare [9], [10], Chao et al. [11], and Krogh and Holloway [12] described synthesis approaches in which the common places or paths are merged. The invariance of the resulting net is determined from the subnets so that they can be used in the net analysis. These approaches can in fact guarantee the safety and liveness of the resulting net. Zhou et al. [13], [14] proposed a hybrid modeling approach based on the hierarchical and combination methods. A PN model is introduced in [5], which defines a set of basic subnets, termed elementary control tasks (ECT). Such a model is sufficiently general to the design of logic controllers, and the subnets can be used to model subsystems through a number of operations including self-loops, inhibitor arcs, and synchronization. The conditions for the preservation of properties, such as liveness, reachability, and reversibility, of PN’s after above operations are discussed in [5]–[8]. In the study of the dynamics of automatic control systems, reachability graphs of PN’s are a commonly used tool. Unfortunately, the size of a conventional reachability graph increases exponentially with the net size. To deal with this difficulty, divide-conquer methods have been proposed [15], [16], in which the hierarchical reachability graph of the synchronous composition net is obtained by reducing and combining the reachability graphs of the subnets. It is clear that the application restriction of such methods is less stringent than that described in [5]–[8]. However, they are only applicable to synchronous composition. System synthesis is an important issue in automatic control problems. In a synthesis process, preservation of local system properties in the global system is essential. Most researches in this area have so far focused on such properties as liveness, reachability, and reversibility. Little work has been done on the study of system behaviors, namely, language of firing sequences. In this paper, we will investigate system behaviors in the synthesis of PN models by using operations of self-loops, inhibitor, as well as synchronization. We will transform self-loops and inhibitor operations into synchronization operations. It will be shown that, after transformation, application of the composition state-space generation methods [15], [16] to modeling and analyzing system properties becomes easier. A new system behavior property, behavior invariance, will be
1042–296X/00$10.00 ? 2000 IEEE
WANG et al.: BEHAVIOR RELATIONS IN SYNTHESIS PROCESS OF PN MODELS
401
defined. The meaning of behavior invariance is that all the firing sequences of subsystems are preserved in their composition system. In other words, the projection of all firing sequences of the composition system on each subsystem is identical to all firing sequences of the corresponding subsystem. A set of preservation conditions for behavior invariance will be obtained under the performed operations. Finally, the usefulness of the results for dynamic analysis of PN model in synthesis process will be demonstrated. In the synthesis processes, it is an essential requirement to keep the system behavior invariant. That is, the projection of the behavior of the composition system on subsystems should be the same as the behavior of its subsystems. On the other hand, in the control processes, it is an essential requirement to restrict the behavior of subsystems (with connective operations), in order to avoid some “bad behaviors” of some subsystems. In other words, the projection of the behavior of the composition system on subsystems should belong to the behavior of the subsystems. In this paper, we shall only discuss behavior invariance in the synthesis processes. This paper is organized as follows. Section II describes the basic concepts and terminology for PN’s. Section III presents the formulas of the language for the three types of connection operations. Section IV studies the behavior invariance for the connection operations. In Section V, a practical example is given to demonstrate the application of the proposed behavior theory to the analysis of logical concurrent systems. The final section concludes the paper. II. BASIC CONCEPTS AND TERMINOLOGY A triplet 1) 2) 3) For is called a net iff: ; ; . , and are called the pre-set and
then marking is said to be reachable from , or , where denoted is called a transition sequence from to . And is called the set of all reachable . markings from , then Let is called the language of and is the behavior of the system . III. LANGUAGE FORMULAS OF CONNECTION OPERATIONS For convenience, three connection operations of PN are formally defined as follows. , be two Definition 1: Let , and . Set , PN’s, such that: ; 1) ; 2) 3) (there is a self-loop and )}; between if , then is called a 4) and , while O is used self-loops connection net of to represent the self-loop operations, denoted as . , Definition 2: Let , and . Set be two PN’s, , such that: ; 1) ; 2) 3) (there is an inhibitor arc and )}; between if , then is called 4) and , while is an inhibitor arc connection net of used to represent the inhibitor arc operations, denoted as . , be two Definition 3: Let , . Set , such PN’s, that: ; 1) ; 2) ; 3) if , then is called 4) and , while $ is a synchronous connection net of used to represent the synchronous operations, denoted as . In the following discussions, we first discuss the preservation relation of $ for the language. The preservation relations of O and for the language will be discussed later. . 1) Set Definition 4: Let be a finite alphabet, , such that , and is the remnant substring after deleting each element in from . is called a projection mapping from to . 2) Set , such that , and . is called an extension mapping from to , where “*” is a closed operation of the language.
the post-set of , respectively. is called a PN iff: is a net; 1) (set of nonnegative integers) is called an 2) initial marking of (or ); and 3) the following firing rules apply. is a marking of , and is said to be a) -enabled (denoted as if . b) can be fired from if is -enabled (denoted as ). Firing from results in a new marking (denoted as ), for , we have if if otherwise. If , such that and markings
402
IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, VOL. 16, NO. 4, AUGUST 2000
Definition 5: Let be a finite alphabet, , , be the languages on and , respectively. Set and and , then and are called the projection language of from to , and the extension language of from to , respectively. In order to simplify the complexity of the system design and analysis, a set of operations on PN’s need to be studied. Then, the languages of firing sequences of PN’s have some relationship with the languages before such operations. Such relationships are called behavior relations of PN’s. Three important operations will be discussed as follows. , Theorem 1: Let , then be two PN’s, and . , denoted Proof: . Set ( is an empty string). Since , consider the following three cases. , such that Case 1: If
Fig. 1. The synchronous composition example.
then set Case 2: If
. , such that
then set Case 3: If
. , such that
then set Similar processes will also applied to and can be obtained such that nally, is a substring of
. . Fi-
Thus
This gives
Based on the descriptions in the above, we have . Hence, Theorem 1 is proved. Example 1: Two PN’s and are shown in Fig. 1(a) and (b), respectively. Their synchronous compois shown in Fig. 1(c). Obviously, sition net , , and . It is easy to verify that Theorem 1 is satisfied. In order to study the language relations of the self-loop operations, O, as described in Definition 1, we first transform the operations from O to $, and then apply Theorem 1 to $. Thus, a self-loop extension net can be defined as follows. , , Definition 6: Let O . If be two PN’s, and , if , such that , set ; , such that: ; 1) ; 2) ; 3) if , then is called a self-loop 4) or 2. extending net of , be two Theorem 2: Let , denoted , and PN’s, then , such that
Or equivalently, Proof:
then , such that . Thus, we have . Since , . Since there exists a self-loop between and , where , we have . Therefore, the following formation in is obtained from Definition 6: , denoted ,
which leads to
The following formula can be proved through a reversal of the above procedure:
WANG et al.: BEHAVIOR RELATIONS IN SYNTHESIS PROCESS OF PN MODELS
403
Definition 7: Let , , be two ECT PN’s, and the inhibitor arcs’ set be ; . is a placed set of reachability from . , . Set ; , such that: 1) 2) 3) ; ; , where is called set of multi-self-loops; ; 4) 5) the following firing rules apply. a) For the nonmulti-self-loop part in a multi-self-loop net, the conventional firing rules as given in (3.1) and (3.2) of Definition 1 should be abided. b) For the multi-self-loop part in a multi-self-loop net, , , , than if is enabled under state iff: i) ii)
Fig. 2. The self-loop extension example.
if .
;
thus
The theorem is proved. Corollary 1: Let O two PN’s, . Proof: By Definitions 1, 3, 6, we have , hence
, , then O
, be
Thus, is called a multi-self-loop net of . , , be two Theorem 3: Let , and ECT PN’s, be a multi-self-loop net of , then . , we only need to Proof: In order to prove show the equivalence between the role of any inhibitor in and , that of a correlative multi- self-loop in . Since are ECT PN’s, they are safe finite states automata. Therefore, if and only if a , such that and . For , , such that: and 1) 2) if and only if if and only if ; .
(By Theorem 1). Example 2: Two PN’s are shown in Fig. 2(a) O is shown and (b). Their self-loop connective net , in in Fig. 2(c), show their self-loop extension net Fig. 2(d) and (e). , , It is clear that , and . . Thus, , that is Corollary 1 is true. In order to study the language formulas of the inhibitor operation, , as in Definition 2, we first transform the operations from to O, and then transform O to $ by applying Theorem 2. A conclusion given in [6] will be used in proving our Theorem 3, that is, an ECT PN is a strongly connected state machine ) whose initial marking is such that only one place ( is marked (unitary marking). Thus, a multi-self-loop net is introduced as follows.
Thus, the role of any inhibitor in is equivalent to that of a cor. relative multi-self-loop in . Hence, we have Definition 8: Let , , be two , and ; be a multiECT PN’s, , such that: self-loop net of . Set 1) 2) 3) ; 4) ; , are called a multi-self-loop extended net of then . , , Theorem 4: Let , be two ECT PN’s, be a multi-self-loop net of , and be two multi-self-loop extended nets of , then , denoted , if , and , such that , ; , ; ; ; ;
404
IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, VOL. 16, NO. 4, AUGUST 2000
, the behavior invariance. Lemma 1: Let two ECT PN’s,
, it is said that
satisfies , be , then
, where
O
. The proof of this lemma is straightforward. , Theorem 5: Let . Then PN’s, and iff Proof: , such that , , for , such that
, .
, be two , , . Since , . Thus
have . Let Since that Theorem 1, we have . Obviously, Thus, . That is . Let , denoted
, hence . Similarly, we . Hence . , , such .1 From
Fig. 3.
The multi-self-loop extended example.
, then , . The proof is omitted as is similar to Theorem 2. , , be two Corollary 2: Let and , ECT PN’s, , be two multi-self-loop extended nets of , then
Proof: From Definitions 2, 3, and 8, we know that . Hence
Example 3: Two PN’s are shown in Fig. 3(a) and (b), respectively, their connective net in Fig. 3(c) by inhibitor arc, the multi-self-loop net of in Fig. 3(d), and the multi-self-loop extended net of in Fig. 3(e) and Fig. 3(f). It is easy , , to see , and . . Thus, IV. BEHAVIOR INVARIANCE OF CONNECTION OPERATIONS In the synthesis processes, it is an essential requirement to keep the system behavior, namely, the language of firing sequences, invariant. In other words, the projection of the behavior of the composition system on subsystems should be the same as the behavior of the subsystems. This behavior invariance of the three connection operations is discussed in the following. , , be Definition 9: Let , where O . If two ECT PN’s,
, . . In the same way, we have . Therefore, , . On the other hand, it is obvious that, , . Hence , Definition 10 [7]: Let , , be to a transition two ECT PN’s, the set of connections from of is said to be the connection bundle (CB) from to . A particular oriented graph, called net-graph, was introduced in [7]. The aim was to synthetically describe the connection bundles between the ECT’s of a net. To each ECT a node was associated in the net-graph, while to each connection bundle one directional arc is drawn. In other words, to each self-loop or each to another ECT , a group of inhibitor arcs from an ECT to is associated in the net-graph. For directional arc from and , two directional arcs each synchronization between to , and the other from to . are drawn, one from the , are shown in Fig. 4(a) Example 4: Two PN’s is shown in and (b) respectively. Their connective net Fig. 4(c), and its net-graph in Fig. 4(d). , , be two Theorem 6: Let , where O . If no live ECT PN’s, and loops exist in the net-graph of , then satisfies the behavior invariance. Proof: Since no loops exist in the net-graph of , it can be to node assumed all connection bundles are from node in the net-graph of . Or, equivalently, is controlled by while is free. Therefore, we have (1) Now, we will prove that , for
1
. First, and
is the shuffling sequence of and .
WANG et al.: BEHAVIOR RELATIONS IN SYNTHESIS PROCESS OF PN MODELS
405
Fig. 5. The super-elevated conveyor.
Fig. 4. The connective operations of nets.
, since
, where is a controlled transition by , are live and is free, we have
in
Fig. 6.
The node controller (SCU) of the conveyor.
denoted ,and thus Lemma 1,
, where . Hence, , . On the other hand, from . Therefore, we have (2)
It is concluded from (1) and (2) that Theorem 6 is true. Theorem 7: Let , be two (ECT) live PN’s. O , , O satisfies the 1) If behavior invariance. , , satisfies 2) If the behavior invariance. Proof: O (from the given condition) (from Theorem 2) Thus, O satisfies the behavior invariance. Statement (2) can be shown in the same way. V. APPLICATION As this paper is focused on behavior invariance, an automatic control system discussed in Ferrarini’s paper [7] is now analyzed using our theory. Example 5: Consider a control problem of a super-elevated conveyor with multiple feed-lines. The process is sketched in
Fig. 4. The conveyor is basically composed of power-driven rollers, approximately 5 m from the ground. The materials are sent to the conveyor from four separate production lines by four ). The actual transfer of materials from elevators ( the elevators to the conveyor’s rollers is performed with corre). Because of the pressponding transfer devices ( ence of the transfer devices, the roller conveyor is divided into ). At the end of each lump, there is a four lumps ( blocking device ( , omitted in Fig. 5 for clarity) to prevent the objects from travelling on the conveyor so as to avoid interference with the objects from the elevators. Each elevator has one power driven slide carrying one object at a time. To reduce the rise and fall time, the motors of the elevators may be operated at two speeds (slow or fast mode), so that the rise and fall motion is performed following a slowfastslow sequence. Fig. 6 shows the PN model example described by Ferrarini, while Fig. 7 is our model for the same example in which the operation transform of O, , and $ is performed. Obviously, we have O O (3) Therefore, the following analysis can be made. The net-graph of system is shown in Fig. 8. Since
from Theorem 5, we have O
406
IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, VOL. 16, NO. 4, AUGUST 2000
2) A new system property, behavior invariance, has been defined. A set of preservation conditions for the behavior invariance have been obtained under operations O, , and as stated in Theorems 5, 6, and 7, respectively. The applicability of the theory to the real world automation systems has been demonstrated in an example in which a super-elevated conveyor system is modeled and analyzed, and the system behavior properties are well preserved by using the proposed method. REFERENCES
[1] K. P. Brand and J. Kopainski, “Principles and engineering process control with Petri nets,” IEEE Trans. Automat. Contr., vol. 33, no. 2, pp. 138–149, 1988. [2] Y. Narahari and N. Viswanadham, “A Petri net approach to the modeling and analysis of flexible manufacturing systems,” Ann. Oper. Res., vol. 3, pp. 449–472, 1985. [3] K. S. Valvanis, “On the hierarchical analysis and simulation of flexible manufacturing system with extended Petri nets,” IEEE Trans. Syst., Man, Cybern., vol. 20, no. 1, pp. 94–100, 1990. [4] I. Suzuki and T. Murata, “A method for stepwise refinements and abstractions of Petri nets,” J. Comput. Syst. Sci., vol. 27, pp. 51–76, 1983. [5] L. Ferrarini, “An incremental approach to logical controller design with Petri nets,” IEEE Trans. Syst., Man, Cybern., vol. 22, no. 3, pp. 461–473, 1992. , “On the reachability and reversibility problem in a class of Petri [6] nets,” IEEE Trans. Syst., Man, Cybern., vol. 24, no. 10, pp. 1474–1482, 1994. [7] L. Ferrarini, M. Narduzzi, and M. T. Solet, “A new approach to modular liveness analysis conceived for large logic controllers’ design,” IEEE Trans. Robot. Automat., vol. 10, pp. 169–184, Apr. 1994. [8] L. Ferrarini and M. Trioni, “Modeling shared resources with generalized synchronization within a Petri net bottom-up approach,” IEEE Trans. Syst., Man, Cybern., vol. 26, no. 4, pp. 653–659, 1996. [9] M. D. Jun and F. DiCesare, “Synthesis using resource control nets for modeling share-resource systems,” IEEE Trans. Robot. Automat., vol. 11, no. 3, pp. 317–327, 1995. [10] M. D. Jun, “A Petri net synthesis theory for modeling flexible manufacturing systems,” IEEE Trans. Syst., Man, Cybern., vol. 27, no. 2, pp. 169–183, 1997. [11] D. Y. Chao, M. C. Zhou, and D. T. Wang, “Extending knitting technique to Petri net synthesis of automated manufacturing systems,” Comput. J., vol. 37, no. 1, pp. 67–76, 1994. [12] B. H. Krogh and L. E. Holloway, “Synthesis of feedback control logic for discrete manufacturing systems,” Automatica, vol. 27, no. 4, pp. 641–651, 1991. [13] M. C. Zhou and F. DiCesare, “Parallel and sequential mutual exclusions for Petri net models,” IEEE Trans. Robot. Automat., vol. 6, pp. 515–527, Apr. 1990. [14] M. C. Zhou, F. DiCesare, and A. Desrochers, “Hybrid methodology for synthesis of Petri nets models for manufacturing systems,” IEEE Trans. Robot. Automat., vol. 8, pp. 350–361, June 1992. [15] M. Notomi and T. Murata, “Hierarchical reachability graph of bounded Petri nets for concurrent-software analysis,” IEEE Trans. Software Eng., vol. 20, no. 5, pp. 325–336, 1994. [16] A. Valmari, “Compositional State Space Generation,” in Lecture Notes in Computer Science. New York: Springer-Verlag, 1993, vol. 674, pp. 527–457.
Fig. 7. Our transform process model.
Fig. 8.
The net-graph of system.
and from Theorem 7, the operation O corresponding to and satisfies the behavior invariance. It is obvious that there are no other loops in the net-graph of and . Also, this system except an only loop between are live. From Theorem 6, operation O corand , as well as operation , also satresponding to isfy the behavior invariance. Therefore, the behaviors, i.e., the language of the firing sequences, of subsystems have not been changed in the subsystem connections.
VI. CONCLUSIONS The firing sequence language of PN’s is a powerful tool in the system behavior representation. The properties of this language in system composition processes have been discussed. The main points of this paper can be summarized as follows. 1) In order to study the language relations of the self-loops operations, O, as described in Definition 1, we first transform the operations from O to , and then apply Theorem 1 to . In order to study the language relations of the inhibitor operation, , as described in Definition 2, we need to transform the operations from to O first, and then apply Theorem 2 to transform O to . Having performed these two transforms, it is easy to apply the generation method of composition state space [15], [16] to model and analyze the system properties, such as reachablity, liveness, etc.
Huaiqing Wang received the Ph.D. degree in computer science from the University of Manchester, Manchester, U.K., in 1987. He is an Associate Professor at the Department of Information Systems, City University of Hong Kong. He specializes in research and development of intelligent systems, web-based intelligent agents and their ebusiness applications, such as multi-agent supported financial monitoring systems, intelligent agent-based knowledge management systems, modeling, and intelligent web-based educational systems.
WANG et al.: BEHAVIOR RELATIONS IN SYNTHESIS PROCESS OF PN MODELS
407
Changjun Jiang received the Ph.D. degree in computer science from the Institute of Automation, Chinese Academy of Science. He is a Professor at the Department of Computer Science and Engineering, Shanghai Tongji University, China. His research areas include Petri nets, concurrent systems, model checking, and fuzzy reasoning.
Stephen Liao received the Ph.D. degree in information systems from Aix Marseillelll University in 1993. He is an Assistant Professor in the Department of Information Systems, City University of Hong Kong. His research areas include object-oriented modeling, systems and technology, user profiling in e-business, and data mining techniques and applications.