Deciding Kleene Algebra Terms Equivalence in Coq
Ref: CISTER-TR-141205 Publication Date: May 2015
Deciding Kleene Algebra Terms Equivalence in Coq
Ref: CISTER-TR-141205 Publication Date: May 2015Abstract:
This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based in automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalisation of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.
David Pereira
Nelma MoreiraPublished in Journal of Logical and Algebraic Methods in Programming (JLAMP), Elsevier, Volume 84, Issue 3, pp 377-401.
DOI:10.1016/j.jlamp.2014.12.004.
ISSN: 2352-2208.
Record Date: 9, Dec, 2014