Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation

Abstract. The saturation state-space generation algorithm has demonstrated clear improvements over state-of-the-art symbolic methods for asynchronous systems. This work is motivated by efficiently applying saturation to CTL model checking. First, we introduce a new “constrained saturation” algorithm which constrains state exploration to a set of states satisfying given properties. This algorithm avoids the expensive afterthe-fact intersection operations and retains the advantages of saturation, namely, exploiting event locality and benefiting from recursive local fixpoint computations. Then, we employ constrained saturation to build the set of states satisfying EU and EG properties for asynchronous systems. The new algorithm can achieve orders-of-magnitude reduction in runtime and memory consumption with respect to methods based on breath-first search, and even with a previously-proposed hybrid approach that alternates between “safe” saturation and “unsafe” breadth-firs...

• Type: Conference
• Year: 2009
• Where: ATVA
• Authors: Yang Zhao, Gianfranco Ciardo
• Keywords: Algorithm, ATVA 2009, Constrained Saturation, Hardware, Saturation State-space Generation