# Deciding Kleene Algebras in Coq

@article{Braibant2012DecidingKA, title={Deciding Kleene Algebras in Coq}, author={Thomas Braibant and Damien Pous}, journal={Log. Methods Comput. Sci.}, year={2012}, volume={8} }

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… Expand

#### Figures, Tables, and Topics from this paper

#### 36 Citations

Algorithms for Kleene algebra with converse

- Mathematics, Computer Science
- J. Log. Algebraic Methods Program.
- 2016

This work shows that deciding this equational theory generated by all algebras of binary relations with operations of union, composition, converse and reflexive transitive closure is PSpace -complete, by providing a PSpace algorithm. Expand

Deciding Synchronous Kleene Algebra with Derivatives

- Mathematics, Computer Science
- CIAA
- 2015

Using the notion of partial derivatives, a new decision procedure for equivalence between SKA terms is presented and the results are extended for SKAT considering automata with transitions labeled by Boolean expressions instead of atoms. Expand

Derivative Based Methods for Deciding SKA and SKAT

- 2014

Synchronous Kleene algebra (SKA) is a decidable framework that combines Kleene algebra (KA) with a synchrony model of concurrency. Elements of SKA can be seen as processes taking place within a fixed… Expand

Proving language inclusion and equivalence by coinduction

- Computer Science, Mathematics
- Inf. Comput.
- 2016

General conditions on language operations for which bisimulation-up-to is sound are given, giving new proofs of clas- sical results such as Arden’s rule and involving the regular operations of union, concatenation and Kleene star as well as language equations with complement and intersection. Expand

Coinductive Proof Techniques for Language Equivalence

- Computer Science
- LATA
- 2013

A general format of behavioural differential equations is defined, in which one can define operations on languages for which bisimulation-up-to is a sound proof technique, and extended to incorporate language complement and intersection. Expand

Algebras of Relations : from algorithms to formal proofs. (Algèbres de relations : des algorithmes aux preuves formelles)

- Mathematics, Computer Science
- 2016

An original automaton model was developed, based on Petri nets, and the equivalence between the original problem and comparing these automata was proved, and it was proved that the problem of comparing Petri automata lies in the class ExpSpace-complete. Expand

Formal analysis of concurrent programs

- Computer Science, Mathematics
- 2015

Extensions of Kleene algebras are used to develop algeBRas for rely-guarantee style reasoning about concurrent programs, which yields a rapid, lightweight approach for the construction of verification and refinement tools. Expand

Kleene Algebra Completeness

- 2014

This paper gives a new presentation of Kozen’s proof of Kleene algebra completeness featured in his article A completeness theorem for Kleene algebras and the algebra of regular events. A few new… Expand

Two-Way Automata in Coq Christian Doczkal Gert Smolka

- 2016

We formally verify translations from two-way automata to one-way automata based on results from the literature. Following Vardi, we obtain a simple reduction from nondeterministic two-way automata to… Expand

A Constructive Theory of Regular Languages in Coq

- Computer Science
- CPP
- 2013

A formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect is presented, which establishes the usual closure properties, gives a minimization algorithm for DFAs, and proves that minimal DFAs are unique up to state renaming. Expand

#### References

SHOWING 1-10 OF 83 REFERENCES

An Efficient Coq Tactic for Deciding Kleene Algebras

- Mathematics, Computer Science
- ITP
- 2010

A reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant relies on a careful implementation of efficient finite automata algorithms, so that it solves casual equations almost instantaneously. Expand

Calculating Church-Rosser Proofs in Kleene Algebra

- Mathematics, Computer Science
- RelMiCS
- 2001

We present simple calculational proofs of Church-Rosser theorems for equational theories, quasiorderings and nonsymmetric transitive relations in Kleene algebra. We also calculate the abstract part… Expand

The Complexity of Kleene Algebra with Tests

- Mathematics
- 1996

Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety… Expand

Automated Reasoning in Kleene Algebra

- Mathematics, Computer Science
- CADE
- 2007

It is demonstrated that off-the-shelf automated proof and counterexample search is an interesting alternative if combined with the right domain model and Kleene algebras might therefore provide light-weight formal methods with heavy-weight automation. Expand

Proving Equalities in a Commutative Ring Done Right in Coq

- Mathematics, Computer Science
- TPHOLs
- 2005

A new implementation of a reflexive tactic which solves equalities in a ring structure inside the Coq system is presented, which shows that such reflective methods can be effectively used in symbolic computation. Expand

Kleene Algebra with Tests: Completeness and Decidability

- Mathematics, Computer Science
- CSL
- 1996

The completeness of the equational theory of Kleene algebras with tests and *-continuous Kleene algebra with tests over language-theoretic and relational models is proved. Expand

Fast Reflexive Arithmetic Tactics the Linear Case and Beyond

- Computer Science
- TYPES
- 2006

This paper shows how to design efficient and lightweight reflexive tactics for a hierarchy of quantifier-free fragments of integer arithmetics that can cope with a wide class of linear and non-linear goals. Expand

Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic

- Mathematics, Computer Science
- CSL
- 2010

We prove "untyping" theorems: in some typed theories (semirings, Kleene algebras, residuated lattices, involutive residuated lattices), typed equations can be derived from the underlying untyped… Expand

A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events

- Mathematics, Computer Science
- Inf. Comput.
- 1994

A finitary axiomatization of the algebra of regular events involving only equations and equational implications that is sound for all interpretations over Kleene algebras is given. Axioms for Kleene… Expand

RALL: Machine-Supported Proofs for Relation Algebra

- Computer Science
- CADE
- 1997

A theorem proving system for abstract relation algebra called RALL (=Relation-Algebraic Language and Logic), based on the generic theorem prover Isabelle, which is an advanced case study for Isabelle/HOL and a quite mature proof assistant for research on the relational calculus. Expand