Sciweavers

Share
ATVA
2009
Springer

Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation

10 years 1 months ago
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...
Yang Zhao, Gianfranco Ciardo
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ATVA
Authors Yang Zhao, Gianfranco Ciardo
Comments (0)
books