Click on a search word OR use the drop-down choices to search for a paper.
2007
Leduc, Ryan J; Dai, Pengcheng; Song, Raoguang
SQRL Report No. 46 “Synthesis Method for Hierarchical Interface-Based Supervisory Control.” Technical Report
2007.
Abstract | Links | BibTeX | Tags: automata, discrete-event systems, formal methods, hierarchical systems, interfaces, supervisory control, synthesis
@techreport{LeducDaiSong2007,
title = {SQRL Report No. 46 “Synthesis Method for Hierarchical Interface-Based Supervisory Control.”},
author = {Ryan J Leduc and Pengcheng Dai and Raoguang Song},
url = {http://www.cas.mcmaster.ca/sqrl/papers/SQRLreport46.pdf},
year = {2007},
date = {2007-08-15},
abstract = {Hierarchical Interface-Based Supervisory Control (HISC) decomposes a discrete-event system (DES) into a high-level subsystem which communicates with n >= 1 low-level subsystems, through separate interfaces. It provides a set of local conditions that can be used to verify global conditions such as nonblocking and controllability such that the complete system model never needs to be constructed.
Currently, a designer must create the supervisors himself and then verify that they satisfy the HISC conditions. In this paper, we develop a synthesis method that can take advantage of the HISC structure. We replace the supervisor for each level by a corresponding specification DES. We then construct for each level a maximally permissive supervisor that satisfies the corresponding HISC conditions.
We define a set of language based fixpoint operators and show that they compute the required level-wise supremal languages. We then discuss the complexity of our algorithms and show that they potentially offer significant savings over the monolithic approach. We also briefly discuss a symbolic HISC verification and synthesis method using Binary Decision Diagrams, that we have also developed.
A large manufacturing system example (worst case state space on the order of 10^30) extended from the AIP example is briefly discussed. The example showed that we can now handle a given level with a statespace as large as 10^15 states, using less than 160MB of memory. This represents a significant improvement in the size of systems that can be handled by the HISC approach. A software tool for synthesis and verification of HISC systems using our approach was also developed.},
keywords = {automata, discrete-event systems, formal methods, hierarchical systems, interfaces, supervisory control, synthesis},
pubstate = {published},
tppubtype = {techreport}
}
Hierarchical Interface-Based Supervisory Control (HISC) decomposes a discrete-event system (DES) into a high-level subsystem which communicates with n >= 1 low-level subsystems, through separate interfaces. It provides a set of local conditions that can be used to verify global conditions such as nonblocking and controllability such that the complete system model never needs to be constructed.
Currently, a designer must create the supervisors himself and then verify that they satisfy the HISC conditions. In this paper, we develop a synthesis method that can take advantage of the HISC structure. We replace the supervisor for each level by a corresponding specification DES. We then construct for each level a maximally permissive supervisor that satisfies the corresponding HISC conditions.
We define a set of language based fixpoint operators and show that they compute the required level-wise supremal languages. We then discuss the complexity of our algorithms and show that they potentially offer significant savings over the monolithic approach. We also briefly discuss a symbolic HISC verification and synthesis method using Binary Decision Diagrams, that we have also developed.
A large manufacturing system example (worst case state space on the order of 10^30) extended from the AIP example is briefly discussed. The example showed that we can now handle a given level with a statespace as large as 10^15 states, using less than 160MB of memory. This represents a significant improvement in the size of systems that can be handled by the HISC approach. A software tool for synthesis and verification of HISC systems using our approach was also developed.
Currently, a designer must create the supervisors himself and then verify that they satisfy the HISC conditions. In this paper, we develop a synthesis method that can take advantage of the HISC structure. We replace the supervisor for each level by a corresponding specification DES. We then construct for each level a maximally permissive supervisor that satisfies the corresponding HISC conditions.
We define a set of language based fixpoint operators and show that they compute the required level-wise supremal languages. We then discuss the complexity of our algorithms and show that they potentially offer significant savings over the monolithic approach. We also briefly discuss a symbolic HISC verification and synthesis method using Binary Decision Diagrams, that we have also developed.
A large manufacturing system example (worst case state space on the order of 10^30) extended from the AIP example is briefly discussed. The example showed that we can now handle a given level with a statespace as large as 10^15 states, using less than 160MB of memory. This represents a significant improvement in the size of systems that can be handled by the HISC approach. A software tool for synthesis and verification of HISC systems using our approach was also developed.