Analysis of Sequential Systems

  • Christoph Meinel
  • Thorsten Theobald


The design of increasingly complex electronic systems makes it more and more difficult to verify their correct behavior. At the same time it becomes more and more important that the systems work correctly, as nowadays human lives seriously depend on them, e.g., in traffic or in medicine.


Image Computation Finite State Machine Transition Relation Switching Function Sequential System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. The analysis of sequential systems using symbolic OBDD techniques was established primarily by Coudert, Berthet, and Madre [CBM89] as well as by Burch, Clarke, Long, McMillan, and Dill [BCL+94]. The constrain operator and the restrict operator also go back to Coudert, Berthet, and Madre. A survey article on implicit set representations can be found in [CM95].Google Scholar
  2. The partitioning technique for image computation based on a transition relation is due to [BCL+94]. The presented heuristic for the arrangement of the partitions was proposed by Geist and Beer [GB94].Google Scholar
  3. Our presentation of reachability analysis follows the one in [Som96a].Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Christoph Meinel
    • 1
  • Thorsten Theobald
    • 2
  1. 1.University of TrierTrierGermany
  2. 2.Technical University MünchenMünchenGermany

Personalised recommendations