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.

Creator

• Schudy, Warren J.
• Cooper, Peter Sidney

Publisher

• Worcester Polytechnic Institute

Identifier

• 03D129M

Advisor

• Dougherty, Daniel J.
• Fisler, Kathryn

Year

• 2003

Date created

• 2003-01-01

Resource type

• Major Qualifying Project

Major

• Computer Science
• Physics

Rights statement

• In Copyright