Journal
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS
Volume 34, Issue 1, Pages 23-37Publisher
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TSMCA.2003.820582
Keywords
colored Petri nets; deadlock analysis algorithms; equivalence reduction; reduction techniques for state space exploration; sweep-line method
Ask authors/readers for more resources
State-space exploration is one of the main approaches to computer-aided verification and analysis of finite-state systems. It is used to reason about a wide range of properties during the design phase of a system, including system deadlocks. Unfortunately, state-space exploration needs to handle huge state spaces for most practical systems. Several state-space reduction methods have been developed to tackle this problem., In this paper, we develop algor algorrithms for combining,two of these methods: state equivalence class reduction and the sweep-line. The algorithms allow deadlocks to be detected by recording terminal states of the system on-the-fly during state-space exploration. We derive expressions for the complexity of the algorithms and demonstrate their usefulness with an industrial case study. Our results show that the combined method achieves at least a six-fold reduction of the state space for interesting parameter values compared with either method used in isolation while still proving the desired system property of the terminal states. The runtime performance of the combined method is almost the same, as that of the equivalence class method over the chosen parameter range. Moreover, the improvement in space reduction increases with increased parameter values.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available