Abstract
A new data-structure called RED(Region-Encoding Diagram) for the fully symbolic model-checking of real-time software systems is proposed. RED is a BDD-like data-structure for the encoding of regions [2]. Unlike DBM which records differences between pairs of clock readings, REDonly uses one auxiliary binary variable for each clock. Thus the number of variables used in REDis always linear to the number of clocks declared in the input system description. Experiment has been carried out to compare REDwith previous technologies. © Springer-Verlag Berlin Heidelberg 2000.
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Cite
CITATION STYLE
Wang, F. (2000). Efficient data structure for fully symbolic verification of real-time software systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1785 LNCS, pp. 157–171). Springer Verlag. https://doi.org/10.1007/3-540-46419-0_12
Readers over time
Readers' Seniority
Readers' Discipline
