Revision on 'Maximally permissive deadlock prevention via an Invariant Controlled Method'

All current design approaches of maximally permissive supervisors assume that forbidden and legal markings are linearly separable. Based on that implicit assumption, Liu et al. propose a novel method of optimal control of a problematic siphon to synthesise maximally permissive controllers. However, there are counter examples for which we could not produce optimal solutions. This occurs when forbidden and legal markings are not linearly separable even though it rarely happens. Verifying linear separability involves solving a large set of linear inequalities and is quite time consuming. This paper aims to relieve this problem via enhancing our critical-siphon approach. Specifically, we propose to: (1) find an efficient method to detect linear inseparability; (2) construct best suboptimal control models; (3) find all lost legal markings; and (4) identify the linear equations that violate linear separability. Each above contribution is unique and pioneering.