Formal Methods in Manufacturing Systems - Advances in Civil and Industrial Engineering
Latest Publications


TOTAL DOCUMENTS

17
(FIVE YEARS 0)

H-INDEX

2
(FIVE YEARS 0)

Published By IGI Global

9781466640344, 9781466640351

Author(s):  
Dmitry A. Zaitsev

Functional Petri nets and subnets are introduced and studied for the purpose of speed-up of Petri nets analysis with algebraic methods. The authors show that any functional subnet may be generated by a composition of minimal functional subnets. They propose two ways to decompose a Petri net: via logical equations solution and with an ad-hoc algorithm, whose complexity is polynomial. Then properties of functional subnets are studied. The authors show that linear invariants of a Petri net may be computed from invariants of its functional subnets; similar results also hold for the fundamental equation of Petri nets. A technique for Petri nets analysis using composition of functional subnets is also introduced and studied. The authors show that composition-based calculation of invariants and solutions of fundamental equation provides a significant speed-up of computations. For an additional speed-up, they propose a sequential composition of functional subnets. Sequential composition is formalised in the terms of graph theory and was named the optimal collapse of a weighted graph. At last, the authors apply the introduced technique to the analysis of Petri net models of such well-known networking protocols as ECMA, TCP, BGP.


Author(s):  
Mingming Yan

This chapter focuses on the deadlock prevention problems in Flexible Manufacturing Systems (FMS), and the major target is to design more excellent controllers that lead to a more permissive supervisor by adding a smaller number of monitors and arcs than the existing ones in the literature for the design of liveness-enforcing Petri net supervisors. The authors distinguish siphons in a Petri net model by elementary and dependent ones. For each elementary siphon, a monitor is added to the plant model such that it is invariant-controlled without generating emptiable control-induced siphons, and the controllability of a dependent siphon is ensured by changing the control depth variables of its related elementary siphons. Hence, a structurally simple Petri net supervisor is achieved. Based on the previous work, this chapter explores two optimized deadlock prevention approaches based on elementary siphons that can achieve the same control purpose and have more excellent performance.


Author(s):  
Wujie Chao ◽  
Yongmei Gan ◽  
W. M. Wonham ◽  
Zhaoan Wang

Much research has been addressed to nonblocking supervisory control of Discrete-Event Systems (DES) such as Flexible Manufacturing Systems (FMS), and a variety of approaches have been developed. One especially powerful approach, due to Chuan Ma, is based on DES representation by means of State Tree Structures (STS). Using STS, this chapter develops nonblocking supervisory control of a well-known benchmark FMS example taken from the literature, for which the description was given originally as a Petri net. The authors straightforwardly obtain the optimal (maximally permissive) and nonblocking supervisory control, and display the control logic for each (controllable) event transparently as a binary decision diagram.


Author(s):  
Shaoyong Li

By modifying the objective function and adding new constraints to a Mixed Integer Programming (MIP) method proposed by Park and Reveliotis, this chapter presents a Revised MIP (RMIP) method to directly solve siphons, called smart siphons, with the minimal cardinality as well as the minimal number of resource places. Accordingly, a proper Control Place (CP) is added for each smart siphon in order to achieve the desired control. Both efficiency and practicality of this method are proved through a theoretical proof and several examples.


Author(s):  
Anikó Costa ◽  
Paulo E. S. Barbosa ◽  
Filipe Moutinho ◽  
Fernando Pereira ◽  
Franklin Ramalho ◽  
...  

Model-based development for embedded system design has been used to accommodate the increase in system’s complexity. Several modeling formalisms proved to be well matched for usage within this area. The goal of this chapter is to present a model-based development methodology for embedded systems design. One of the main aims of this methodology is to contribute for usage of Petri nets as a system specification language within model-based development of embedded systems integrating MDA (Model-Driven Architecture) proposals as a reference for the development flow. Distributed execution of the initial developed platform-independent models is achieved through model partitioning into platform-specific sub-modules. System model decomposition is obtained through a net splitting operation. Two types of implementation platforms are considered: compliant and non-compliant with zero time delay for communication between modules (in other words, compliant or not with synchronous paradigm). Using a model-checking framework, properties associated to the execution of the distributed models in both types of platforms are compared with the execution of the initial model.


Author(s):  
Renyuan Zhang ◽  
Yongmei Gan ◽  
W. M. Wonham ◽  
Zhaoan Wang

In recent years, a great deal of research has been focused on preventing deadlock in Flexible Manufacturing Systems. Policies based largely on Petri net models have been presented in the literature. Recently, a quite different approach has been developed based on supervisory control theory, and it has been adapted to solve the nonblocking maximally permissive control problem in various resource allocation systems, such as an Automatic Guided Vehicle system and a Production Cell. In this chapter, the authors obtain the corresponding control policy for a Flexible Manufacturing System, and from it derive an equivalent distributed control using the recent theory of supervisor localization.


Author(s):  
Meng Qin

Many deadlock prevention policies on the basis of Petri nets dealing with deadlock problems in flexible manufacturing systems exist. However, most of them do not consider uncontrollable and unobservable transitions. This chapter solves deadlock problems in Petri nets with uncontrollable and unobservable transitions. A sufficient condition is developed to decide whether an existing deadlock prevention policy is still applicable in a Petri net with uncontrollable and unobservable transitions, when the policy itself is developed under the assumption that all the transitions are controllable and observable. Moreover, the author develops a deadlock prevention policy to design liveness-enforcing supervisors for a class of Petri nets with partial observability and controllability of transitions. Furthermore, a sufficient condition to decide the existence of a monitor to enforce a liveness constraint is developed.


Author(s):  
Anrong Wang ◽  
MengChu Zhou

Deadlocks should be eliminated in resource allocation systems such as flexible manufacturing systems. An iterative deadlock control policy is usually considered to be a natural solution with reasonable computational cost for a large-scale system where direct methods would be prohibitively expensive (and in some cases impossible) even with the best available computing power. This chapter reviews the existing iterative deadlock prevention policies for discrete event systems that are modeled with Petri nets. A number of technical problems in the existing iterative deadlock control approaches are formulated and discussed. Their solutions are illustrated through case studies. The authors conclude that the suitability, effectiveness, and efficiency of an iterative deadlock control approach are sensitive to specific examples and no general algorithm is found in the literature, which works well for all cases.


Author(s):  
Daniel Yuh Chao

The authors developed a theory to show that exactly one monitor is required for the set of siphons in the family of 2-compound siphons and how to assign its initial markings. This avoids redundant monitors and the unnecessary associated computational burden. Neither reachability graph nor minimal siphon needs to be computed to achieve polynomial complexity—essential for large systems. This chapter redevelops the theory more formally and further applies this approach to two well-known S3PR to obtain a controller full or near maximally permissive, where Weighted Control (WC) arcs are nevertheless necessary to keep the controlled model maximally permissive. However, optimal control for siphons involving WC arcs are still under research. As many as possible for simpler structures are desired to reduce WC arcs. In addition, fast computation is important for dynamic reconfiguration situations. The authors develop a single theorem to identify the condition where WC places cannot be replaced by Ordinary Control (OC) arcs, while others can be replaced.


Author(s):  
Yi-Sheng Huang ◽  
Yen-Liang Pan

Deadlock prevention, deadlock detection, and deadlock avoidance strategies are used to solve the deadlock problems of Flexible Manufacturing Systems (FMS). The theory of regions has been recognized as the unique method for obtaining maximally permissive controllers in the existing literature. All legal and live maximal behavior of a Petri net model can be preserved by using a Marking/Transition-Separation Instance (MTSI). However, obtaining all sets of MTSIs is an extremely time consuming problem. This work proposes Crucial Marking/Transition-Separation Instances (CMTSIs) that allow designers to employ few MTSIs to deal with deadlocks. The advantage of the proposed policy is that a maximally permissive controller can be obtained with drastically reduced computation. Experimental results, by varying the markings of given net structures, indicate that it is the most efficient policy to obtain optimal controllers among existing methods based on the theory of regions.


Sign in / Sign up

Export Citation Format

Share Document