|
Authors: | Kai Lampka |
Group: | Computer Engineering |
Type: | Techreport |
Title: | Re-visiting Partitioned Symbolic State Graph Generation for high-level models |
Year: | 2009 |
Month: | August |
Pub-Key: | Lam09c |
Keywords: | Binary Decision Diagrams, symbolic reachability analysis |
Rep Nbr: | 308 |
Abstract: | Model checking techniques commonly require the mapping of high-level models such as (extended) Petri Nets to their underlying state/ transition systems. This paper introduces a two-staged, semi-symbolic procedure for generating Binary Decision Diagram (BDD)-based representations of high-level model's state/transition systems. Contrary to existing techniques the proposed scheme combines state counter- and activity-driven decomposition of models. This strategy limits explicit state graph exploration and encoding of detected states to a very small fraction of a high-level model's state space. Standard benchmark models show that the presented ideas achieve improvements up to two orders of magnitude. |
Location: | Gloriastr. 35, 8092 Zuerich |
Resources: | [BibTeX] [Paper as PDF] |