Symbolic Parametric Analysis of Embedded Systems with BDD-like Data-Structures
<|reference_start|>Symbolic Parametric Analysis of Embedded Systems with BDD-like Data-Structures: 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.<|reference_end|>
@article{wang2003symbolic,
    title={Symbolic Parametric Analysis of Embedded Systems with BDD-like
  Data-Structures},
    author={Farn Wang},
    journal={arXiv preprint arXiv:cs/0306113},
    year={2003},
    archivePrefix={arXiv},
    eprint={cs/0306113},
    primaryClass={cs.DS cs.LO}
}