Title: Automatic Proof Generation in Kleene Algebra with Tests
Speaker: James Worthington
Mathematics Department
Malott Hall
Cornell University
Ithaca, NY 14850
USA
worthing@math.cornell.edu
Kleene algebra (KA) is the algebra of regular events. Familiar examples of
Kleene algebras include regular sets, relation algebras, and trace algebras. A
Kleene algebra with tests (KAT) is a Kleene algebra with an embedded Boolean
subalgebra. The addition tests allows one to encode while programs as KAT
terms, thus the equational theory of KAT allows one to reason about
(propositional) program equivalence. More complicated
statements about programs can be expressed in the Hoare theory of KAT, which
suffices to encode Propositional Hoare Logic.
In our paper, we prove the following results. First, there is a PSPACE
transducer which takes equations of Kleene Algebra as input
and outputs proofs of them in an algebraic proof system based on a form of
bisimulation. Second, we give a feasible reduction
from the equational theory of KAT to the equational theory of KA. Combined with
the fact that the Hoare theory of KAT reduces efficiently to the equational
theory of KAT, this yields an algorithm capable of generating proofs of a large
class of statements about programs.
Our result has applications to areas such as Proof-Carrying Code, where it is
necessary that a formal proof be produced. There are two traditional
approaches to the equational theory of KA: interactive protocols for generating
proofs and the decision procedure of Stockmeyer and Meyer to determine finite
automata equivalence. Each has its own drawbacks: interactive protocols are by
definition not automatic, and the output of a decision procedure is just one
bit, and therefore not efficiently verifiable. Our method, which is completely
automatic and outputs a proof, combines the best features of each.