Loading...
Thumbnail Image
Item

Framework and proofs for synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction

Abstract
This working paper presents an algorithm that combines modular synthesis for extended finite-state machines (EFSM) with abstraction of variables by symbolic manipulation, in order to compute least restrictive controllable supervisors. Given a modular EFSM system consisting of several components, the proposed algorithm synthesises a separate supervisor for each specification component. To synthesise each supervisor, the algorithm iteratively selects components (plants and variables) from a synchronous composition until a least restrictive controllable solution is obtained. This improves on previous results of the authors where abstraction is only performed by the selection of components and not variables. The working paper explains the theory of EFSM synthesis and abstraction and includes formal proofs of all results. An example of a flexible manufacturing system illustrates how the proposed algorithm works to compute a modular supervisor.
Type
Working Paper
Type of thesis
Series
Computer Science Working Papers
Citation
Malik, R., & Teixeira, M. (2018). Framework and proofs for synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction (Working paper No. 03/2018). Hamilton, New Zealand: Department of Computer Science, The University of Waikato.
Date
2018
Publisher
Department of Computer Science, The University of Waikato
Degree
Supervisors
Rights
© 2018 The Authors