Speakers:

• Gaiyun Liu. Xidian University. Xidian University. Xi’an, China “Robust Supervisory Control of Automated Manufacturing Systems”
• Kamel Barkaoui. Conservatoire National des Arts et Métiers (Le Cnam- Paris) “Maximal persistent steps for reduced state space generation”
• ZhiWu Li. Xidian University. Xi’an, China “Maximally Permissive Petri Net Supervisor with Novel Structures”

Day: 21 de noviembre de 2016

Time: 12h

Location: Seminario (bloque 5, 2ª planta) del Instituto

Universitario de Investigación en Ingeniería de Aragón (I3A).

Edificio I+D+I – Campus Río Ebro. C/Mariano Esquillor s/n.

50018, Zaragoza

Abstracts and Bios:

• Gaiyun Liu received the BS and the first PhD degrees from Xidian University, Xi’an, China, in 2006 and 2011, respectively. She received the second PhD degree from Conservatoire National des Arts et Métiers (Le Cnam), Paris, France, in 2015. Since 2011, she has been with Xidian University, where she is currently an associate professor with the School of Electro-Mechanical Engineering. Her research interests include Petri net theory and applications and supervisory control of discrete event systems. She published 17 papers in international journals and conferences.
  
  Title: Robust Supervisory Control of Automated Manufacturing Systems
  
  Abstract: A variety of deadlock control policies based on Petri nets have been proposed for automated manufacturing systems (AMSs). Almost all of them assume that resources do not fail. Actually, resource failures are usually inevitable in real-world systems, which pose challenges in supervisory control of contemporary AMSs. When resources are unreliable, it is infeasible or impossible to apply the existing control strategies and failure-derived deadlocks in the disturbed system may be caused. Reanalysis of the disturbed system is usually necessary, which may lead to high cost of production. For a class of Petri nets (systems of simple sequential processes with resources, S3PR), this talk introduces a robust deadlock control policy in which the factor of resource failures is considered. Recovery subnets and monitors are designed for unreliable resources and strict minimal siphons that may be emptied, respectively. Normal and inhibitor arcs are used to connect monitors with recovery subnets in case of necessity. Then reanalysis of the original Petri net is avoided and a robust liveness-enforcing supervisor is derived.
  

• Kamel Barkaoui is full professor at the Department of Computer Science of Conservatoire National des Arts et Métiers (Le Cnam - Paris) since 2002. He holds a Ph.D in Computer Science (1988) and Habilitation à Diriger des Recherches (1998) from Université Paris 6 (UPMC). His research interests include formal methods for specification, verification, control and performance evaluation of concurrent and distributed systems. He published over 100 peer-reviewed papers in international journals and conferences, supervised 28 PhD theses, co-edited 10 books. He received the 1995 IEEE Int. Conf. on System Man and Cybernetics Outstanding Paper Award and Recipient of the Prime d’Excellence Scientifique and of the PEDR since 1998. He was PC co-chair of the 3rd International Colloquium on Theoretical Aspects of Computing (ICTAC2006), General co-chair of the 18th International Symposium on Formal Methods (FM2012) and General chair of the 35th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets2014) and of the 14th International Conference on Application of Concurrency to System Design (ACSD2014). He was a Guest Editor of Formal Aspects of Computing Journal (FACJ), of Journal of Systems and Software (JSS) and ACM Transactions on Embedded Computing Systems (TECS) and serves as Associate Editor for the International Journal of Critical Computer-Based Systems (IJCCBS). He is the founder and SC chair of the International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS).
  
  Title: Maximal persistent steps for reduced state space generation
  
  Abstract: The state explosion problem is the main obstacle for the formal verification of concurrent systems, as they are generally based on an interleaving semantics, where all possible firing orders of concurrent actions are exhaustively explored. The step graph method aims at attenuating the state explosion problem, by executing, in one step, the largest possible number of concurrent transitions. The idea is to represent, by a single path, the largest possible set of equivalent firing sequences of the model. All transitions of the sequences are represented in the path but the concurrent ones are grouped together in steps. However, even if all transitions within the same step are concurrent, their firing in one step may prevent enabledness of some conflicting transitions (deferred conflicts) that are enabled, when the transitions of the step are fired in specific orders. Consequently, some equivalent maximal firing sequences will not be represented in the step graph. The step graph method, proposed in the literature for Petri nets, handles such a problem by systematically excluding from every step transitions that are in weak conflict relation. In this talk we present some recent results that significantly alleviate this limitation. After introducing the notion of persistent firing steps, we propose a maximal persistent step graph (MPSG) method and show that all and only all non-equivalent maximal firing sequences of the model are represented in the MPSG. Afterwards, we establish a practical sufficient condition for a step to be persistent that yields a significant reduction of the state space, especially for large asynchronous concurrent systems.

• ZhiWu Li received the B.S., M.S., and Ph.D. degrees from Xidian University in 1989, 1992, and 1995, respectively. He joined Xidian University in 1992. His interests include discrete event systems and Pertri nets. He published two monographs in Springer and CRC Press and 70+ papers in Automatica and IEEE Transactions (mostly regular). His work was cited by engineers and researchers from more than 40 countries and areas, including prestigious RD institutes such as IBM, Volvo, HP, GE, GM, ABB. He serves (served) an Associate Editor of the IEEE Trans. Automation Science and Engineering, IEEE Trans. Systems, Man, and Cybernetics, Part A: Systems and Human Beings, IEEE Trans. Systems, Man, and Cybernetics: Systems, and Information Sciences (Elsevier). Dr. Li is a recipient of Alexander von Humboldt Research Grant and Research in Paris. He was selected in 2014, 2015, and 2016 Thomson Reuters Highly Cited Researchers in the category of Engineering. He is a Fellow of IEEE.
  
  Title: Maximally Permissive Petri Net Supervisor with Novel Structures
  
  Abstract: This talk introduces two classes of inhibitor arcs: interval inhibitor arcs and data inhibitor arcs that are used to design a maximally permissive liveness-enforcing supervisor for an automated manufacturing system modeled with Petri nets. The development of the novel inhibitor arcs is motivated by the fact that there usually does not exist an optimal supervisor represented by pure Petri nets when the legal space is non-convex. A significant result derived from this new net structure is that the pertinent approach can always lead to an optimal supervisor with only one control place for bounded Petri nets on the premise that such a supervisor exists.