Worcester Polytechnic Institute Electronic Theses and Dissertations Collection

Title page for ETD etd-101210-193945

Document Typethesis
Author NameFeng, Yu
TitleDisjunction of Regular Timing Diagrams
DepartmentComputer Science
  • Kathi Fisler, Advisor
  • Dan Dougherty, Reader
  • Michael Gennert, Department Head
  • Keywords
  • Alloy
  • disjunction
  • model checking
  • temporal logic
  • timing diagrams
  • Date of Presentation/Defense2010-10-12
    Availability unrestricted


    Timing diagrams are used in industrial practice as a specification language of circuit components. They have been formalized for efficient use in model checking. This formalization is often more succinct and convenient than the use of temporal logic. We explore the relationship between timing diagrams and temporal logic formulas by showing that closure under disjunction does not hold for timing diagrams. We give an algorithm that returns a disjunction (if any) of two given timing diagrams. We also give algorithms that decide satisfiability of a timing diagram and return exact time separations between events in a timing diagram. An Alloy specification for timing diagrams with one waveform has also been built.

  • yfeng.pdf

  • Browse by Author | Browse by Department | Search all available ETDs

    [WPI] [Library] [Home] [Top]

    Questions? Email etd-questions@wpi.edu
    Maintained by webmaster@wpi.edu