Data Structure Choices for On-the-Fly Model Checking of Real-Time Systems

Design and Implementation of Formal Tools and Systems 2011.

计算机科学;

Peter Fontana ; Rance Cleaveland

Others  :  http://ceur-ws.org/Vol-832/paper_12.pdf
PID  :  33671

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

This paper studies the performance of sparse-matrix-based data structures to represent clock zones (con- vex sets of clock values) in an on-the-fly predicate equation system model checker for timed automata. We analyze the impact of replacing the dense difference bound matrix (DBM) with both the linked-list CRDZone and array-list CRDArray data structure. From analysis on the paired- example-by-example differences in time performance, we infer the DBM is either competitive with or slightly faster than the CRDZone, and both perform faster than the CRDArray. Using similar analysis on space performance, we infer the CRDZone takes the least space, and the DBM takes less space than the CRDArray.