Liveness-Enforcing Supervision of Sequential Resource Allocation Systems

As many contemporary technological applications move to more extensively automated operational modes, there is an emerging need for controlling the operation of these systems not only for efficiency but also for behavioral correctness. This need is prominent, for instance, in flexibly automated production systems, where the removal of the human element from the production shop-floor necessitates the a priori resolution in the provided control logic of many facets that in the past had been left to the jurisdiction of the present human intelligence. Similar needs arise in the context of automated railway and/or monorail transportation systems, and also in the automated workflow management and business transaction systems, that have been enabled by the recent IT developments.

In this talk, we propose the notion of the Resource Allocation System (RAS) as a pertinent abstraction that allows the combined modeling of the time-based as well as the logical dynamics of the aforementioned applications, and we proceed to the study of the liveness and the liveness-enforcing supervision of these systems through formal frameworks provided by (qualitative) Discrete Event Systems theory. A main position of the talk is that, while the classical Ramadge & Wonham Supervisory Control framework provides a straightforward characterization of the addressed problem and its optimal (i.e., maximally permissive) solution, the practical implementation of the derived results can be potentially constrained by their non-polynomial complexity with respect to the compact representation(s) of the underlying RAS. Hence, a significant part of the talk will be spent on (i) the identification of cases admitting optimal liveness-enforcing supervision of polynomial complexity, and (ii) the synthesis of effective and computationally efficient (although suboptimal) solutions for the remaining cases.