The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.01 - January (2005 vol.31)
pp: 38-51
Farn Wang , IEEE Computer Society
ABSTRACT
We introduce a new BDD-like data structure called Hybrid-Restriction Diagrams (HRDs) for the representation and manipulation of linear hybrid automata (LHA) state-spaces and present algorithms for weakest precondition calculations. This permits us to reason about the valuations of parameters that make safety properties satisfied. Advantages of our approach include the ability to represent discrete state information and concave polyhedra in a unified scheme, as well as to save both memory consumptions and manipulation times when processing the same substructures in state-space representations. Our experimental results document its efficiency in practice.
INDEX TERMS
Data-structures, BDD, hybrid automata, verification, model-checking.
CITATION
Farn Wang, "Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures", IEEE Transactions on Software Engineering, vol.31, no. 1, pp. 38-51, January 2005, doi:10.1109/TSE.2005.13
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool