ABSTRACT
This chapter discusses Finite State Automata (FSA) modelling framework for a systematic investigation of the behavioural problem of deadlock avoidance in flexibly automated production systems. It introduces a notion of optimality in the context of resource allocation system (RAS) deadlock avoidance that is defined on the basis of maximal permissiveness. The chapter presents a formal approach for the investigation of the deadlock avoidance problems that is based on the abstracting notion of the RAS, and the further representation of the RAS dynamics in the FSA modelling framework. The analysis enables a rigorous characterization of the concepts of deadlock and deadlock avoidance policies (DAP). It led to a notion of optimality for the sought DAPs, in the form of maximal permissiveness. However, the deployment of the maximally permissive DAP is an NP-Hard problem for many practical RAS instantiations.
