Progressive events in supervisory control and compositional verification
Ware, S., & Malik, R. (2014). Progressive events in supervisory control and compositional verification. Control Theory and Technology, 12(3), 317–329. http://doi.org/10.1007/s11768-014-4097-8
Permanent Research Commons link: https://hdl.handle.net/10289/9358
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.
© 2014 South China University of Technology, Academy of Mathematics and Systems Science, CAS, and Springer-Verlag Berlin Heidelberg