TR-IIS-05-003    Fulltext

Proving ∀µ -Calculus Properties with SAT-Based Model Checking

Bow-Yaw Wang


In this paper, we present a complete bounded model checking algorithm for the universal fragment of µ-calculus. The new algorithm checks the completeness of bounded proof of each property on the fly and does not depend on prior knowledge of the completeness thresholds. The key is to combine both local and bounded model checking techniques and use SAT solvers to perform local model checking on finite Kripke structures. Our proof-theoretic approach works for any property in the pecification logic and is more general than previous work on specific properties. We report experimental results to compare our algorithm with the conventional BDD-based algorithm.