Billington, Jonathan3; Gallasch, Guy E3; Kristensen, Lars Michael2; Mailund5
1 Bioinformatics Research Centre (BiRC), Faculty of Science, Aarhus University, Aarhus University2 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University3 unknown4 Bioinformatics Research Centre (BiRC), Science and Technology, Aarhus University5 Bioinformatics Research Centre (BiRC), Science and Technology, Aarhus University
State space exploration is one of the main approaches to computer-aided verification and analysis of finite-state systems, and can be used to reason about a wide range of properties during the design phase of a system, including desired and undesired terminal states. Several state space reduction methods have been developed to alleviate the state explosion problem inherent in methods based on state space exploration. In this paper we develop algorithms for combining two of these methods: the sweep-line method and the equivalence reduction method. The algorithms allow terminal states of the system to be reported on-the-fly during the state space exploration. We demonstrate the usefulness of the algorithms by applying them to an industrial case study. These experimental results show that the combined methods achieves a better reduction of the state space than when either methods are used in isolation.
I E E E Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans, 2004, Vol 34, Issue 1, p. 23-37