Fully symbolic model checking of timed systems using difference decision diagrams

Citations of this article
Mendeley users who have this article in their library.


Current approaches for analyzing timed systems are based on an explicit enumeration of the discrete states and thus these techniques are only capable of analyzing systems with a handful of timers and a few thousand states. We address this limitation by describing how to analyze a timed system fully symbolically, i.e., by representing sets of discrete states and their associated timing information implicitly. We demonstrate the efficiency of the symbolic technique by computing the set of reachable states for a non-trivial timed system and compare the results with the state-of-the-art tools KRONOS and UPPAAL. With an implementation based on difference decision diagrams, the runtimes are several orders of magnitudes better. The key operation in obtaining these results is the ability to advance time symbolically. We show how to do this efficiently by essentially quantifying out a special variable z which is used to represent the constant zero. The symbolic manipulations given in this paper are sufficient to verify TCTL-formulae fully symbolically. ©1999 Published by Elesevier Science B. V.




Møeller, J., Lichtenberg, J., Andersen, H. R., & Hulgaard, H. (2001). Fully symbolic model checking of timed systems using difference decision diagrams. In Electronic Notes in Theoretical Computer Science (Vol. 23, pp. 88–107). Elsevier. https://doi.org/10.1016/S1571-0661(04)80671-6

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free