Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Automata on Guarded Strings and Applications
Authors: Kozen, Dexter
Keywords: computer science
technical report
Issue Date: 25-Jan-2001
Publisher: Cornell University
Abstract: Guarded strings are like ordinary strings over a finite alphabet P, except that atoms of the free Boolean algebra on a set of atomic tests B alternate with the symbols of P. The regular sets of guarded strings play the same role in Kleene algebra with tests as the regular sets of ordinary strings do in Kleene algebra. In this paper we develop the elementary theory of finite automata on guarded strings, a generalization of the theory of finite automata on ordinary strings. We give several basic constructions, including determinization, state minimization, and an analog of Kleene's theorem. We then use these results to verify a conjecture on the complexity of a complete Gentzen-style sequent calculus for \partial correctness. We also show that a basic result of the theory of Boolean decision diagrams (BDDs), namely that minimal ordered BDDs are unique, is a special case of the Myhill-Nerode theorem for a class of automata on guarded strings.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
2001-1833.pdf232.26 kBAdobe PDFView/Open
2001-1833.ps238.89 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us