Improving approximate reachability by dynamic interleavings of projections-based algorithms

Finding the set of reachable states of a digital control circuit has important applications in synthesis, analysis and verification of digital control systems. The literature contains a wide range of reachability analysis algorithms, including exact and approximate ones, with complementary or even incomparable strengths. Given a problem instance, it is practically impossible to statically identify the algorithm that would offer the best trade-off between performance and synthesis/verification objectives. In this paper, we focus on projections-based approximate reachability analysis algorithms and show that dynamically interleaving these algorithms can outperform not only the individual algorithms, but also other state-of-the-art tools. We demonstrate the effectiveness of our idea by a set of experiments.