Symbolic Parametric Analysis of Embedded Systems with BDD-like Data-Structures
数据结构与算法
2007-05-23 v2 计算机科学中的逻辑
摘要
We use dense variable-ordering to define HRD (Hybrid-Restriction Diagram), a new BDD-like data-structure for the representation and manipulation of state-spaces of linear hybrid automata. We present and discuss various manipulation algorithms for HRD, including the basic set-oriented operations, weakest precondition calculation, and normalization. We implemented the ideas and experimented to see their performance. Finally, we have also developed a pruning technique for state-space exploration based on parameter valuation space characterization. The technique showed good promise in our experiment.
引用
@article{arxiv.cs/0306113,
title = {Symbolic Parametric Analysis of Embedded Systems with BDD-like Data-Structures},
author = {Farn Wang},
journal= {arXiv preprint arXiv:cs/0306113},
year = {2007}
}
备注
11 pages, 1 figure