Algebras of relations: from algorithms to formal proofs
Algebras of relations appear naturally in many contexts, in computer science as well as in mathematics. They constitute a framework well suited to the semantics of imperative programs. Kleene algebras are a starting point: these algebras enjoy very strong decidability properties, and a complete axiomatisation. The goal of this thesis was to export known results from Kleene algebra to some of its extensions. We first considered a known extension: Kleene algebras with converse. Decidability of these algebras was already known, but the algorithm witnessing this result was too complicated to be practical. We proposed a simpler algorithm, which is more efficient, and whose correctness is easier to establish. It allowed us to prove that this problem lies in the complexity class PSpace-complete. Then we studied Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we established the equivalence between equality in Kleene allegories and the equality of certain sets of graphs. We then developed a new automaton model (so-called Petri automata), based on Petri nets. We proved the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provided an algorithm performing this comparison. This algorithm uses exponential space. However, we proved that the problem of comparing Petri automata lies in the class ExpSpace- complete. Finally, we studied Nominal Kleene algebras. We realised that existing descriptions of these algebra were not suited to relational semantics of programming languages. We thus modified them accordingly, and doing so uncovered several natural variations of this model. We then studied formally the bridges one could build between these variations, and between the existing model and our new version of it. This study was conducted using the proof assistant Coq.
@phdthesis{thesis,
title = "Algebras of relations: from algorithms to formal proofs",
author = "{Paul Brunet}",
year = 2016,
school = "Université de Lyon",
}
Links
| Manuscript on HAL |
Related talks | ||
|
ICALP
in Patras,
July 2019.
|
More | |
|
Highlights
in Berlin,
September 2018.
|
More | |
|
MOVE
in Marseille,
March 2017.
|
More | |
|
PACE
in Shanghai,
November 2016.
|
More | |
|
Highlights
in Brussels,
September 2016.
|
More | |
|
MFCS
in Krakow,
August 2016.
|
More | |
|
Inter'Actions
in Lyon,
May 2016
(in French)
.
|
More | |
|
LiCS
in Kyoto,
July 2015.
|
More | |
|
Rapido
in Paris,
June 2015.
|
More | |
|
Midlands Graduate School
in Sheffield,
April 2015.
|
More | |
|
JFLA
in Val d'Ajol,
January 2015
(in French)
.
|
More | |
|
LAC
in Chambéry,
November 2014.
|
More | |
|
RAMiCS
in Marienstatt,
April 2014.
|
More | |
|
GeoCal
in Bordeaux,
March 2014.
|
More | |
|
PACE
in Lyon,
February 2014.
|
More | |
|
Internship defence
in Paris,
September 2013
(Internship defence, in French)
.
|
More | |
|
PiCoq
in Lyon,
June 2013.
|
More | |
Related papers | ||
|
Bracket Algebra, a nominal theory of interleaved scopes
(2019)
with Alexandra Silva and Daniela Petrişan. |
More | |
|
A Kleene theorem for nominal automata
(in ICALP 2019)
with Alexandra Silva. |
More | |
|
Petri automata
(in LMCS 2017)
with Damien Pous. |
More | |
|
Cardinalities of finite relations in Coq
(in ITP 2016)
with Insa Stucke and Damien Pous. |
More | |
|
Algorithms for Kleene algebra with converse
(in JLAMP 2016)
with Damien Pous. |
More | |
|
A formal exploration of nominal Kleene algebra
(in MFCS 2016)
with Damien Pous. |
More | |
|
Petri automata for Kleene allegories
(in LICS 2015)
with Damien Pous. |
More | |
|
Decidability of identity-free relational Kleene lattices
(in JFLA 2015)
with Damien Pous. |
More | |
|
Kleene algebra with converse
(in RAMICS 2014)
with Damien Pous. |
More | |