Timing diagram to Buchi automation translation Public
Downloadable Contentopen in viewer
We examined a discrepancy between direct translation of timing diagrams into Buchi automata and the translation using Linear Temporal Logic (LTL) as an intermediate representation and then using an existing LTL to Buchi algorithm. We improved the number of states generated to within a factor of two by using a newer LTL to Buchi algorithm called Wring. We examined which combination of Wring's optimization cause the improvement, and under what conditions Wring outperforms the direct translation.
- This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.
- Date created
- Resource type
- Rights statement
Permanent link to this page: https://digital.wpi.edu/show/8g84mq58g