Show simple item record

dc.contributor.authorKozen, Dexteren_US
dc.description.abstractGuarded 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.en_US
dc.format.extent237833 bytes
dc.format.extent244621 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleAutomata on Guarded Strings and Applicationsen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record