Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs

  • Dirk Beyer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


For the formal specification and verification of real-time systems we use the modular formalism Cottbus Timed Automata (CTA), which is an extension of timed automata [AD94]. Matrix-based algorithms for the reachability analysis of timed automata are implemented in tools like Kronos, Uppaal, HyTech and Rabbit. A new BDD-based version of Rabbit, which supports also refinement checking, is now available.


Formal verification Real-time systems Timed Automata 


  1. [AD94]
    Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. [Bey01]
    Dirk Beyer. Improvements in BDD-based reachability analysis of timed automata. In Proc. FME2001, LNCS 2021, pages 318–343. Springer-Verlag, 2001.Google Scholar
  3. [BMPY97]
    M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress on the symbolic verification of timed automata. In Proc. CAV’97, LNCS 1254, pages 179–190. 1997.Google Scholar
  4. [BN01]
    Dirk Beyer and Andreas Noack. Efficient verification of timed automata using BDDs. In Proc. Formal Methods for Industrial Critical Systems. to appear, 2001.Google Scholar
  5. [BR98]
    Dirk Beyer and Heinrich Rust. Modeling a production cell as a distributed real-time system with Cottbus Timed Automata. Proc. FBT’98, pages 148–159. Shaker, 1998.Google Scholar
  6. [BR01]
    Dirk Beyer and Heinrich Rust. Cottbus Timed Automata: Formal definition and semantics. In Proc. FSCBS 2001, pages 75–87, 2001.Google Scholar
  7. [DHWT92]
    David L. Dill, Alan J. Hu, and Howard Wong-Toi. Checking for language inclusion using simulation preorders. In Proc. CAV’91, LNCS 575, pages 255–265. 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Dirk Beyer
    • 1
  1. 1.Software Systems Engineering Research GroupTechnical University CottbusGermany

Personalised recommendations