We present a method to perform symbolic state space generation for languages with existing enumerative state generators. The method is largely independent from the chosen modelling language. We validated this on three different types of languages and tools: state-based languages (PROMELA), action-based process algebras (muCRL, mCRL2), and discrete abstractions of ODEs (Maple). Only little information about the combinatorial structure of the underlying model checking problem need to be provided. The key enabling data structure is the "PINS" dependency matrix. Moreover, it can be provided gradually (more precise information yield better results). Second, in addition to symbolic reachability, the same PINS matrix contains enough information to enable new optimizations in state space generation (transition caching), again independent from the chosen modelling language. We have also based existing optimizations, like (recursive) state collapsing, on top of PINS and hint at how to support partial order reduction techniques. Third, PINS allows interfacing of existing state generators to, e.g., distributed reachability tools. Thus, besides the stated novelties, the method we propose also significantly reduces the complexity of building modular yet still efficient model checking tools. Our experiments show that we can match or even outperform existing tools by reusing their own state generators, which we have linked into an implementation of our ideas.
|Place of Publication||Enschede|
|Publisher||Centre for Telematics and Information Technology (CTIT)|
|Number of pages||8|
|Publication status||Published - 5 Jun 2009|
|Name||CTIT Technical Report Series|
|Publisher||University of Twente, Centre for Telematics and Information Technology|
- Model Checking
- State Space Exploration
- EC Grant Agreement nr.: FP6/043235
- Symbolic reachability
Blom, S., van de Pol, J. C., & Weber, M. (2009). Bridging the Gap between Enumerative and Symbolic Model Checkers. (CTIT Technical Report Series; No. TR-CTIT-09-30). Enschede: Centre for Telematics and Information Technology (CTIT).