Hierarchical set decision diagrams and regular models

Abstract. This paper presents algorithms and data structures that exploit a com-positional and hierarchical specification to enable more efficient symbolic model-checking. We encode the state space and transition relation using hierarchical Set Decision Diagrams (SDD) [9]. In SDD, arcs of the structure are labeled with sets, themselves stored as SDD. To exploit the hierarchy of SDD, a structured model representation is needed. We thus introduce a formalism integrating a simple notion of type and instance. Complex composite behaviors are obtained using a synchronization mechanism borrowed from process calculi. Using this relatively general framework, we in-vestigate how to capture similarities in regular and concurrent models. Experi-mental results are presented, showing that this approach can outperform in time and memory previous work in this area.