Projects per year
Abstract
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.
Original language | English |
---|---|
Title of host publication | SMC'99 |
Subtitle of host publication | First International Workshop on Symbolic Model Checking |
Editors | A Cimatti, O Grumberg |
Place of Publication | Trento |
Publisher | Elsevier |
Pages | 107-127 |
Number of pages | 21 |
Volume | 23-1 |
Publication status | Published - 1999 |
Keywords
- sharing trees
- model generation
- model checking
- abstract interpretation
- fictitious clock
- real time
- temporal logic
Fingerprint
Dive into the research topics of 'Model-Generation of a Fictitious Clock Real-Time Logic Using Sharing Trees'. Together they form a unique fingerprint.Projects
- 1 Finished