| 摘要: |
| This paper investigates some limitations of the nonblocking property when used for supervisor synthesis in discrete event
systems. It is shown that there are cases where synthesis with the nonblocking property gives undesired results. To address
such cases, the paper introduces progressive events as a means to specify more precisely how a synthesised supervisor should
complete its tasks. The nonblocking property is modified to take progressive events into account, and appropriate methods for
verification and synthesis are proposed. Experiments show that progressive events can be used in the analysis of industrial-scale
systems, and can expose issues that remain undetected by standard nonblocking verification. |
| 关键词: Model validation in design methods Controller constraints and structure Computational issues |
| DOI： |
| Received:July 04, 2014Revised:July 13, 2014 |
| 基金项目: |
|
| Progressive events in supervisory control and compositional verification |
| S. Ware,R. Malik |
| (School of Electronic and Electrical Engineering, Nanyang Technological University;Department of Computer Science, University of Waikato, Hamilton, New Zealand) |
| Abstract: |
| This paper investigates some limitations of the nonblocking property when used for supervisor synthesis in discrete event
systems. It is shown that there are cases where synthesis with the nonblocking property gives undesired results. To address
such cases, the paper introduces progressive events as a means to specify more precisely how a synthesised supervisor should
complete its tasks. The nonblocking property is modified to take progressive events into account, and appropriate methods for
verification and synthesis are proposed. Experiments show that progressive events can be used in the analysis of industrial-scale
systems, and can expose issues that remain undetected by standard nonblocking verification. |
| Key words: Model validation in design methods Controller constraints and structure Computational issues |
