 |
|
|||
| 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] |
