Abstractions for Nonblocking Supervisory Control of Extended Finite Automata

Abstract—An abstraction method for Extended Finite Auto-mata (EFAs), i.e., finite automata extended with variables, using transition projection is presented in this work. A manufac-turing system modeled by EFAs is abstracted into subsystems that embody internal interacting dependencies. Synthesis and verification of subsystems are achieved through their model abstractions rather than their global model. Sufficient con-ditions are presented to guarantee that supervisors result in maximally permissive and nonblocking control. An examples demonstrate the computational effectiveness and practical usage of the approach. I