Structural Symbolic CTL Model Checking of Asynchronous Systems

In previous work, we showed how structural information can be used to efficiently generate the state-space of asynchronous systems. Here, we apply these ideas to symbolic CTL model checking. Thanks to a Kronecker encoding of the transition relation, we detect and exploit event locality and apply better fixed-point iteration strategies, resulting in orders-of-magnitude reductions for both execution times and memory consumption in comparison to well-established tools such as NuSMV.

• Type: Conference
• Year: 2003
• Where: CAV
• Authors: Gianfranco Ciardo, Radu Siminiceanu
• Keywords: Asynchronous Systems, Better fixed-point Iteration, CAV 2003, Formal Methods, Symbolic Ctl Model