Show simple item record

dc.contributor.advisor Vardi, Moshe Y.
dc.creatorFogarty, Seth
dc.date.accessioned 2011-07-25T01:39:26Z
dc.date.available 2011-07-25T01:39:26Z
dc.date.issued 2009
dc.identifier.urihttp://hdl.handle.net/1911/61915
dc.description.abstract We compare tools for complementing nondeterministic Buchi automata with a recent termination-analysis algorithm. Complementation of Buchi automata is a well-explored problem in program verification. Early solutions using a Ramsey-based combinatorial argument have been supplanted by rank-based constructions with exponentially better bounds. In 2001 Lee et al. presented the size-change termination (SCT) problem, along with both a reduction to Buchi automata and a Ramsey-based algorithm This algorithm strongly resembles the initial complementation constructions for Buchi automata. This leads us to wonder if theoretical gains in efficiency are mirrored in empirical performance. We prove the SCT algorithm is a specialized realization of the Ramsey-based complementation construction. Doing so allows us to generalize SCT solvers to handle Buchi automata. We experimentally demonstrate that, surprisingly, Ramsey-based approaches are superior over the domain of SCT problems, while rank-based approaches dominate automata universality tests. This reveals several interesting properties of the problem spaces and both approaches.
dc.format.mimetype application/pdf
dc.language.iso eng
dc.subjectComputer science
Applied sciences
dc.title Buchi containment and size-change termination
dc.type.genre Thesis
dc.type.material Text
thesis.degree.department Computer Science
thesis.degree.discipline Engineering
thesis.degree.grantor Rice University
thesis.degree.level Masters
thesis.degree.name Master of Science
dc.identifier.citation Fogarty, Seth. "Buchi containment and size-change termination." (2009) Master’s Thesis, Rice University. http://hdl.handle.net/1911/61915.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record