Model-Generation of a Fictitious Clock Real-Time Logic Using Sharing Trees

Laurent Ferier, Jean-Francois Raskin, Pierre-Yves Schobbens

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationSMC'99
Subtitle of host publicationFirst International Workshop on Symbolic Model Checking
EditorsA Cimatti, O Grumberg
Place of PublicationTrento
PublisherElsevier
Pages107-127
Number of pages21
Volume23-1
Publication statusPublished - 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.

Cite this