Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/5821
 Title: Automata on Guarded Strings and Applications Authors: Kozen, Dexter Keywords: computer sciencetechnical report Issue Date: 25-Jan-2001 Publisher: Cornell University Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2001-1833 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. URI: http://hdl.handle.net/1813/5821 Appears in Collections: Computer Science Technical Reports

Files in This Item:

File Description SizeFormat