Deciding Kleene Algebras in Coq

Thomas Braibant; Damien Pous

doi:10.2168/LMCS-8(1:16)2012

Thomas Braibant ; Damien Pous - Deciding Kleene Algebras in Coq

lmcs:1043 - Logical Methods in Computer Science, March 2, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:16)2012

Deciding Kleene Algebras in CoqArticle

Authors: Thomas Braibant ; Damien Pous

We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations instantaneously and properly scales to larger expressions. The decision procedure is proved correct and complete: correctness is established w.r.t. any model by formalising Kozen's initiality theorem; a counter-example is returned when the given equation does not hold. The correctness proof is challenging: it involves both a precise analysis of the underlying automata algorithms and a lot of algebraic reasoning. In particular, we have to formalise the theory of matrices over a Kleene algebra. We build on the recent addition of firstorder typeclasses in Coq in order to work efficiently with the involved algebraic structures.

https://doi.org/10.2168/LMCS-8(1:16)2012

Source: arXiv.org:1105.4537

Volume: Volume 8, Issue 1

Published on: March 2, 2012

Imported on: May 16, 2011

Keywords: Computer Science - Logic in Computer Science,Computer Science - Symbolic Computation,F 1.1, F 3.1, F.4.1, F.4.3, D 2.4

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

17 Documents citing this article

ZhengPu Shi;GuoJun Xie;Gang Chen, 2023, CoqMatrix: Formal matrix library with multiple models in Coq, Journal of Systems Architecture, 143, pp. 102986, 10.1016/j.sysarc.2023.102986.

Tej Chajed;Joseph Tassarotti;M. Frans Kaashoek;Nickolai Zeldovich, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Argosy: verifying layered storage systems with recovery refinement, 2019, Phoenix AZ USA, 10.1145/3314221.3314585.

Maximiliano Cristiá;Gianfranco Rossi, Lecture notes in computer science, A Set Solver for Finite Set Relation Algebra, pp. 333-349, 2018, 10.1007/978-3-030-02149-8_20.

Sylvain Boulmé;Alexandre Maréchal, 2018, Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra, 62, 4, pp. 505-530, 10.1007/s10817-018-9492-2, https://hal.archives-ouvertes.fr/hal-01133865.

Rudolf Berghammer;Insa Stucke;Michael Winter, 2017, Using relation-algebraic means and tool support for investigating and computing bipartitions, Journal of Logical and Algebraic Methods in Programming, 90, pp. 102-124, 10.1016/j.jlamp.2017.04.001, https://doi.org/10.1016/j.jlamp.2017.04.001.

Jurriaan Rot;Marcello Bonsangue;Jan Rutten, 2015, Proving language inclusion and equivalence by coinduction, Information and Computation, 246, pp. 62-76, 10.1016/j.ic.2015.11.009, https://doi.org/10.1016/j.ic.2015.11.009.

Lawrence C. Paulson, arXiv (Cornell University), A Formalisation of Finite Automata Using Hereditarily Finite Sets, pp. 231-245, 2015, 10.1007/978-3-319-21401-6_15, http://arxiv.org/abs/1505.01662.

Nate Foster;Dexter Kozen;Mae Milano;Alexandra Silva;Laure Thompson, 2015, A Coalgebraic Decision Procedure for NetKAT, Data Archiving and Networked Services (DANS), 50, 1, pp. 343-355, 10.1145/2775051.2677011, https://hdl.handle.net/2066/129979.

Paul Brunet;Damien Pous, 2015, Algorithms for Kleene algebra with converse, Journal of Logical and Algebraic Methods in Programming, 85, 4, pp. 574-594, 10.1016/j.jlamp.2015.07.005, https://doi.org/10.1016/j.jlamp.2015.07.005.

Sabine Broda;Sílvia Cavadas;Miguel Ferreira;Nelma Moreira, Open Repository of the University of Porto (University of Porto), Deciding Synchronous Kleene Algebra with Derivatives, pp. 49-62, 2015, 10.1007/978-3-319-22360-5_5, https://hdl.handle.net/10216/90793.

Nate Foster;Dexter Kozen;Mae Milano;Alexandra Silva;Laure Thompson, Data Archiving and Networked Services (DANS), A Coalgebraic Decision Procedure for NetKAT, 9, pp. 343-355, 2014, Mumbai India, 10.1145/2676726.2677011, https://hdl.handle.net/2066/129979.

Alasdair Armstrong;Georg Struth;Tjark Weber, Lecture notes in computer science, Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL, pp. 197-212, 2013, 10.1007/978-3-642-39634-2_16.

Christian Doczkal;Jan-Oliver Kaiser;Gert Smolka, Lecture notes in computer science, A Constructive Theory of Regular Languages in Coq, pp. 82-97, 2013, 10.1007/978-3-319-03545-1_6.

Damien Pous, arXiv (Cornell University), Kleene Algebra with Tests and Coq Tools for while Programs, pp. 180-196, 2013, 10.1007/978-3-642-39634-2_15, https://arxiv.org/abs/1302.1737.

Jurriaan Rot;Marcello Bonsangue;Jan Rutten, CWI's Institutional Repository (Centrum Wiskunde & Informatica), Coinductive Proof Techniques for Language Equivalence, pp. 480-492, 2013, 10.1007/978-3-642-37064-9_42, https://ir.cwi.nl/pub/22128.

Wolfram Kahl, Lecture notes in computer science, Towards Certifiable Implementation of Graph Transformation via Relation Categories, pp. 82-97, 2012, 10.1007/978-3-642-33314-9_6.

Damien Pous, Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic, pp. 484-498, 2010, 10.1007/978-3-642-15205-4_37, https://hal.science/hal-00421158.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1781 times.

This article's PDF has been downloaded 576 times.