Advanced selfloop removal in compositional nonblocking verification of discrete event systems
Malik, R. (2015). Advanced selfloop removal in compositional nonblocking verification of discrete event systems. In Proceeding of IEEE International Conference on Automation Science and Engineering, Gothenburg, Sweden, 24-28 August, 2015 (pp. 819–824). USA: IEEE. http://doi.org/10.1109/CoASE.2015.7294182
Permanent Research Commons link: http://hdl.handle.net/10289/10254
This paper investigates possible improvements of abstraction to simplify finite-state machines during compositional nonblocking verification of large discrete event systems. Current methods to simplify finite-state machines depend on the absence of transitions from the states to be simplified, and selfloop transitions, i.e., transitions with the same source and target state, are a common culprit that prevents simplification. Some methods to remove such selfloops are known, but they require events that appear on selfloops in the entire finitestate machine to be simplified. The methods described in this paper improve on this, because they allow for the removal of individual selfloop transitions from a finite-state machine while preserving conflict equivalence. This makes it possible to remove more transitions, thus reducing the computational effort of compositional nonblocking verification. Two abstraction rules are proposed, and experimental results show the potential of improvement over previously used methods.
This is an author’s accepted version of an article published in the Proceeding of IEEE International Conference on Automation Science and Engineering. ©2015 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.