We propose a symbolic model checking procedure for timed systems that is based on operations on constraints. To accelerate the termination of the model checking procedure, we define history-dependent widening operators, again in terms of constraint-based operations. We show that these widenings are accurate, i.e., they don't lose precision even with respect to the test of boundedness properties. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Mukhopadhyay, S., & Podelski, A. (2001). Accurate widenings and boundedness properties of timed systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2244 LNCS, pp. 79–94). Springer Verlag. https://doi.org/10.1007/3-540-45575-2_10
Mendeley helps you to discover research relevant for your work.