Checking timed büchi automata emptiness efficiently

  • Tripakis S
  • Yovine S
  • Bouajjani A
  • 14


    Mendeley users who have this article in their library.
  • 55


    Citations of this article.


This paper presents an on-the-fly and symbolic technique for efficiently checking timed automata emptiness. It is symbolic because it uses the simulation graph (instead of the region graph). It is on-the-fly because the simulation graph is generated during the test for emptiness. We have implemented a verification tool called Profounder based on this technique. To our knowledge, Profounder is the only available tool for checking emptiness of timed Büchi automata. To illustrate the practical interest of our approach, we show the performances of the tool on a non-trivial case study. © 2005 Springer Science+Business Media, Inc.

Author-supplied keywords

  • On-the fly verification
  • Symbolic model-checking
  • Timed automata
  • Verification tools

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Get full text


  • Stavros Tripakis

  • Sergio Yovine

  • Ahmed Bouajjani

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free