Building a Symbolic Model Checker from Formal Language Description

The main limit towards practical model-checking is the combinatorial explosion of the number of states. Among numerous solutions proposed to tackle this problem, Decision Diagrams (DDs) have been proved efficient. They are however low-level data structures: translating a high-level model to them can be cumbersome. Indeed, little work towards their better usability has been undertaken. We propose an abstract mechanism for the manipulation of DDs, where system transitions are described in terms of rewrite rules. We describe how basic rewrite rules can be assembled through strategies, to describe complex transition relations (e.g. involving various levels of synchronization among parallel components). The strategies and rewrite rules offer a higher-level interface, where the nature of underlying DD is hidden, close to high-level languages used to model concurrent systems. We also describe specific strategies that we use to automatically translate high-level modeling languages (namely Petri Nets and imperative languages) to rewrite strategies, ultimately translated in terms of operations on DDs.