ACM Transactions on Embedded Computing Systems · 2013 · 15 citations · 50 references
EngineeringIndustrial EngineeringConcurrent SystemFormal VerificationOperations ResearchSystems EngineeringTrusted Operating SystemDesignDeadlock Control TheoryComputer EngineeringComplementary PlacesManufacturing SystemsSupervisory ControlComputer ScienceInteger ProgrammingDeadlock ProblemCloud ComputingAutomationProcess ControlProduction SchedulingFormal MethodsDeadlock Detection MethodScheduling (Production Processes)Concurrency TheoryIndustrial Informatics
In this article, an algorithm is proposed to design liveness-enforcing supervisors for systems of simple sequential processes with resources (S 3 PR) based on complementary places. Firstly, a mixed integer programming (MIP) based deadlock detection method is used to find unmarked strict minimal siphons from an infinite-capacity net. Next, the finite-capacity net, in which liveness can be enforced, is obtained by adding capacity function to the infinite-capacity net. Finally, complementary-place transformation is used to transform the finite-capacity net into an infinite-capacity net. This article focuses on adding a complementary place to each operation place that is related to unmarked siphons, deals with the deadlock problem from a new view point, and hence advances the deadlock control theory. Compared with the existing methods, the new policy is easier to implement for real industrial systems. More importantly, design of a complementary-place supervisor is very easy. Finally, in some cases, the new policy can obtain a structurally simpler supervisor with more permissive behavior than the existing methods do. A flexible manufacturing systems (FMS) example is used to compare the proposed policy with some other methods.
50
Petri nets: Properties, analysis and applications
T. Murata · Proceedings of the IEEE · 1989 · 10.5K citations
Feedback control of Petri nets based on place invariants
John Moody, Katerina Yamalidou, Michael Lemmon et al. · 2002 · 425 citations