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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Ciardo, G., & Siminiceanu, R. (2003). Structural symbolic CTL model checking of asynchronous systems. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2725, 40–53. https://doi.org/10.1007/978-3-540-45069-6_4
Mendeley helps you to discover research relevant for your work.