Kleene Algebra with Tests Dexter Kozen Cornell University Workshop on Logic & Computation Nelson, NZ, January 2004 These Lectures 1. Tutorial on KA and KAT • model theory • complexity, deductive completeness • relation to Hoare logic 2. Practical applications • compiler optimization • scheme equivalence • static analysis 3. Theoretical applications • automata on guarded strings & BDDs • algebraic version of Parikh’s theorem • representation • dynamic model theory Kleene Algebra (KA) is the algebra of regular expressions pq + qp p q p p*q {pq,qp} {q,pq,p 2q,p3q, …} q (p + q)* = (p*q)*p* q p p,q {all strings over p,q} (0 + 1(01*0)*1)* {multiples of 3 in binary} q (pq)*p = p(qp)* {p,pqp,pqpqp,} 0 1 0 1 0 p 1 Standard Interpretation Regular sets over A+B AB A* 1 0 = = = = = AB {xy | x A, y B} Un0 An = A0 A1 A2 {} p interpreted as {p} ... Binary Relations R, S binary relations on a set X R+S = R S RS = R ° S = {(u,v) | w (u,w) R, (w,v) S} R* = reflexive transitive closure of R = Un0 Rn = R R1 R2 1 0 = identity relation = {(u,u) | u X} = Applications • Automata and formal languages regular expressions • Program logic and verification Dynamic Logic program analysis protocol verification compiler optimization • Algorithms shortest paths connectivity computational geometry Prehistory • Definition, relation to finite automata Kleene 56 • No purely equational axiomatization Redko 64 • Axiomatization of equational theory Salomaa 66 • Algebraic theory Conway 71 • Equational theory PSPACE complete (Stock+1)Meyer 74 Axioms of KA [K91] • K is an idempotent semiring under +, ·, 0, 1 (p + q) + r = p + (q + r) p+q=q+p p+p=p p+0=p (pq)r = p(qr) p1 = 1p = p p0 = 0p = 0 p(q + r) = pq + pr (p + q)r = pr + qr • p*q = least x such that q + px x • qp* = least x such that q + xp x def xy x+y=y Succinctly stated, A Kleene algebra is an idempotent semiring such that • p*q is the least fixpoint of x.(q + px) • qp* is the least fixpoint of x.(q + xp) This is a universal Horn axiomatization • p*q = least x such that q + px x q + p(p*q) p*q q + px x p*q x • qp* = least x such that q + xp x q + p(qp*) qp* q + px x qp* x Every system of linear inequalities a11x1 + ... + an1xn + b1 x1 . . . an1x1 + ... + annxn + bn xn has a unique least solution Alternative Characterizations of * Complete semirings (quantales) i I pi = supremum of {pi | i I} with respect to *-continuity pq*r = sup pqnr n0 • infinitary • same equational theory Eq(KA) = Eq(KA*) Some Useful Properties 1 + pp* = 1 + p*p = p* p*p* = p** = p* (pq)*p = p(qp)* sliding (p*q)*p* = (p + q)* denesting px = xq p*x = xq* bisimulation qp = 0 (p + q)* = p*q* loop distribution qp = pq (p + q)* = (pq)*(p* + q*) Proof of the Sliding Rule (ab)*a a(ba)* a + aba(ba)* = a(1 + ba(ba)*) = a(ba)* distributivity 1 + pp* = p*. a + aba(ba)* a(ba)* (ab)*a a(ba)* q + px x p*q x The reverse inequality is symmetric. Completeness and Complexity • Deductively complete for the equational theory of regular sets of strings and relational models [K 94] • Complexity: Equational theory is PSPACEcomplete [Meyer+Stockmeyer 74] • Hoare theory (Horn theory with premises p = 0) is PSPACE-complete [Cohen 93] • Horn theory is 11-complete for starcontinuous & relational models [Hardin+K 03] Matrices over a KA a b c d a b c d def 0= e f g h + · e f g h 0 0 0 0 a b * def = c d a+e b+f c+g d+h def = ae+bg af+bh ce+dg cf+dh def = def 1= 1 0 0 1 (a+bd*c)* (a+bd*c)*bd* (d+ca*b)*ca* (d+ca*b)* Matrices over a KA a b * def = cd (a+bd*c)* (a+bd*c)*bd* (d+ca*b)*ca* (d+ca*b)* b d a c Matrices over a KA • Representation of finite automata • Construction of regular expressions • Solution of linear equations over a KA • Connectivity and shortest path algorithms Solution of Linear Inequalities a11x1 + ... + an1xn + b1 x1 . . . an1x1 + ... + annxn + bn xn a11 ... an1 . . . an1 ... ann x1 . . . xn + b1 . . . bn x1 . . . xn Shortest Paths The min,+ algebra R+ {} r + s = min r,s rs =r+s r* =0 0 = 1 =0 = .9 1.4 3.2 0 1.4 3.2 0 .9 0 * 0 1.4 2.3 = 0 .9 0 Other Models Convex polyhedra [Iwano & Steiglitz 90] AB = {ax + by | x A, y B} A A* = convex hull of A B Other Models Convex polyhedra [Iwano & Steiglitz 90] AB = {ax + by | x A, y B} A A* = convex hull of A B Hoare Logic C. A. R. “Sir Tony” Hoare, 1969 • The first formal system for verification of well-structured programs • Initiated the field of program correctness • Inspiration of hundred of technical articles, books, book chapters, surveys • Turing Award 1980, knighted in 1999 Partial Correctness Assertions {b}p{c} postcondition program precondition ‘‘If b holds in the current state, and if p is executed starting in the current state, then if p halts, c will be true of the halting state.’’ Rules of Hoare Logic {b[x/e]} x:=e {b} {b}p{c}, {c}q{d} {b}pq{d} {bc}p{d}, {bc}q{d} {c}if b then p else q{d} {bc}p{c} {c}while b do p{bc} b’ b, {b}p{c}, c c’ {b’}p{c’} assignment rule composition rule conditional rule while rule weakening rule Dynamic Logic [Pratt 76] <p>b “Starting from the current state, it is possible for p to halt in a state satisfying b.” [p]b “Starting from the current state, it is necessary that if p halts, it does so in a state satisfying b.” DL subsumes HL {b}p{c} b [p]c Propositional Dynamic Logic (PDL) [Fischer & Ladner 1979] propositional modal logic + Kleene algebra Syntax • program operators ; + * • propositional operators 0 1 • mixed operators <p>b [p]b b? Semantics • binary relations (input/output) While programs in PDL [Fischer & Ladner 79] if b then p else q b?;p + b?;q while b do p (b?;p)*;b? Results about PDL • complete deductive system [Segerberg 77, Gabbay 77, Parikh 78] b [p*](b [p]b) • EXPTIME-complete [Pratt 78] [p*]b For many applications in CS (simple program manipulations, safety analysis, local optimizations) don’t need the full power of PDL—equational reasoning suffices BUT need tests to model conventional programming constructs (if-then-else, while-do, ) Kleene Algebra with Tests (KAT) (K, B, +, ·, *, ¯, 0, 1) • (K, +, ·, *, 0, 1) is a Kleene algebra • (B, +, ·, ¯, 0, 1) is a Boolean algebra •BK • p,q,r, range over K • a,b,c, range over B Kleene Algebra with Tests (KAT) +, ·, 0, 1 serve double duty • applied to programs, denote choice, composition, fail, and skip, resp. • applied to tests, denote disjunction, conjunction, falsity, and truth, resp. • these usages do not conflict! bc = b c b+c=bc Models • Relational models K = binary relations on a set X B = subsets of the identity relation • Trace models K = sets of traces u0p0u1p1u2 … un-1pn-1un B = sets of traces of length 0 • Language-theoretic models K = regular sets of guarded strings over B = atoms of a finite free Boolean algebra Guarded Strings [Kaplan 69] P atomic programs B atomic tests , , atoms (minimal nonzero elements) of the free Boolean algebra on generators B e.g. if B = {b1,...,b6}, then b1b2b3b4b5b6 is an atom guarded strings A+B = AB AB A* 1 0 = = = = 0p01p12p23 n-1pn-1n {xy | x A, y B} Un0 An {atoms} Theorem [K & Smith 96] The family of regular sets of guarded strings over P,B is the free KAT on generators P,B. Corollary KAT is complete over relational models. Eq(GS) = Eq(KAT) = Eq(KAT*) = Eq(REL) Completeness and Complexity • Deductively complete for the equational theory of regular sets of guarded strings and relational models [K+Smith 96] • Complexity: Equational theory is PSPACEcomplete [K+S 96, Cohen+K+S 97] • Hoare theory (Horn formulas with premises of form p=0) is PSPACE-complete [K+S 96] 1 • Full Horn theory is still 1-complete Matrices over a KAT The n x n matrices over a KAT (K,B) forms a KAT (K’,B’) B’ = diagonal matrices over B Modeling Programs same as in PDL [Fischer & Ladner 79] p;q pq if b then p else q bp + bq while b do p (bp)*b Propositional Hoare Logic (PHL) Hoare Logic without the assignment rule {b[x/t]} x := t {b} Is a given rule {b1}p1{c1}, ..., {bn}pn{cn} {b}p{c} • a logical consequence of the composition, conditional, while, and weakening rules? • relationally valid? KAT subsumes PHL {b}p{c} is modeled by any of the following equivalent equations & inequalities: • bp pc • bp pc • bp = bpc • bpc = 0 {b}p{c}, {c}q{d} {b}pq{d} {bc}p{d}, {bc}q{d} {c}if b then p else q{d} {bc}p{c} {c}while b do p{bc} composition rule conditional rule while rule {b}p{c}, {c}q{d} {b}pq{d} composition rule bpc = 0 cqd = 0 bpqd = 0 {bc}p{d}, {bc}q{d} {c}if b then p else q{d} conditional rule bcpd = 0 bcqd = 0 c(bp+bq)d = 0 {bc}p{c} {c}while b do p{bc} while rule bcpc = 0 c(bp)*b bc = 0 Theorem These are all theorems of KAT Completeness Theorem [K 99] All relationally valid rules of the form {b1}p1{c1}, ..., {bn}pn{cn} {b}p{c} are derivable in KAT (not so for PHL) Counterexample {c}if b then p else p{c} {c}p{c} is trivially unprovable in Hoare Logic, but c(bp + bp)c = 0 cpc = 0 is easily provable in KAT Hoare formulas p1 = 0 p2 = 0 ... pn = 0 q = r Theorem KAT is complete for the Hoare theory of relational algebras ... not for the Horn theory! Counterexample: p 1 p2 = p Complexity Theorem [Berstel 79] It is undecidable whether a given equation holds under a given set of commutativity conditions in all *continuous Kleene algebras Theorem [K 99] 0 ... 2 -complete ... Horn Theories Theorem [K 99, K + Hardin 03] The universal Horn theories of KA*, KAT*, 1 REL are 1 -complete Q: Is there a natural example of a sentence in H(KA*) H(KA)? Q: Is H(REL) finitely axiomatizable relative to H(KA*)? Q: What is the complexity of H(KA)? Complexity of KAT and PHL Theorem [Cohen 94] The Hoare theory of KA (Horn formulas with premises p = 0) is PSPACE-complete Theorem [Cohen, Kozen & Smith 96] The Hoare theory of KAT is PSPACE-complete Theorem PHL is PSPACE-complete Schematic KAT (SKAT) x := s ; y := t = y := t[x/s] ; x := s y FV(s) x := s ; y := t = x := s ; y := t[x/s] x FV(s) x := s ; x := t = x := t[x/s] b[x/t] ; x := t x := x = 1 = x := t ; b Special Cases x := s ; y := t y := t ; x := s (x Var(t), y Var(s)) b ; x := t (x Var(b)) x := s ; x = s (x Var(s)) x := t ; b x := s x = s x = s ; x := s Relation to Hoare Assignment Rule [x/t] ; x := t = x := t ; is equivalent to {[x/t]} x := t {} {[x/t]} x := t {} Relation to Hoare Assignment Rule [x/t] ; x := t = x := t ; cp = pb is equivalent to {[x/t]} x := t {} cpb = 0 {[x/t]} x := t {} cpb = 0 cp = pb cpb + cpb = 0 Interpreted Reasoning = 1 where is any property of the domain of computation, typically an instantiated universal first-order property

Descargar
# On Hoare Logic and Kleene Algebra with Tests