Re-visiting Partitioned Symbolic State Graph Generation for high-level models

Abstract

Modeling formalisms allow one to compactly describe complexsystems. But, once it comes to the actual analysis the high-level descriptions are commonly required to be transformed into flat statetransition systems (ST-systems), e.g. for asserting system properties by means of model checking techniques. Decision Diagrams and their algorithms are well accepted for carrying out the above mentioned transformation. This paper introduces a combined procedure for efficientlyconstructing a Binary Decision Diagram (BDD) which represents the ST-system underlying a high-level model such as a Petri net, UML state chart, set of reactive modules, etc.. The proposed scheme is independent of the model description method, as it combines state enumeration with symbolic, i. e., BDD-based, state space construction techniques. In contrast to existing techniques it exploits state-counter and activity-driven decomposition of high-level models, as this severely reduces the number of state enumerations and softens the hill climbing problem commonly attached to the incremental construction of BDDs. As shown in an empirical evaluation, the proposed technique has the potential not only for outperforming other combined approaches, but is also competitive w. r. t. other fully symbolic state space construction techniques.