Symbolic Parametric Analysis of Embedded Systems with BDD-like Data-Structures

TL;DR

This paper introduces HRD, a BDD-like data-structure for linear hybrid automata, along with algorithms for manipulation and a pruning technique for efficient state-space exploration, demonstrating promising experimental results.

Contribution

The paper presents HRD, a novel data-structure for hybrid automata analysis, with algorithms and a pruning method that improve state-space exploration efficiency.

Findings

HRD effectively represents hybrid automata state-spaces

Algorithms for HRD enable efficient set operations and precondition calculations

Pruning technique improves exploration performance in experiments

Abstract

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.