17 Search Results for "Pous, Damien"

Document
DOI: 10.4230/LIPIcs.CONCUR.2022.26
Completeness Theorems for Kleene Algebra with Top

Authors: Damien Pous and Jana Wagemaker

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant "top" for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. We recover that the two equational theories coincide if we slightly generalise the notion of relational model, allowing sub-algebras of relations where top is a greatest element but not necessarily the full relation. We use models of closed languages and reductions in order to prove our completeness results, which are relative to any axiomatisation of the algebra of regular events.
Cite as

Damien Pous and Jana Wagemaker. Completeness Theorems for Kleene Algebra with Top. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{pous_et_al:LIPIcs.CONCUR.2022.26,
  author =	{Pous, Damien and Wagemaker, Jana},
  title =	{{Completeness Theorems for Kleene Algebra with Top}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.26},
  URN =		{urn:nbn:de:0030-drops-170890},
  doi =		{10.4230/LIPIcs.CONCUR.2022.26},
  annote =	{Keywords: Kleene algebra, Hypotheses, Completeness, Closed languages}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.41
Graph Characterization of the Universal Theory of Relations

Authors: Amina Doumane

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
The equational theory of relations can be characterized using graphs and homomorphisms. This result, found independently by Freyd and Scedrov and by Andréka and Bredikhin, shows that the equational theory of relations is decidable. In this paper, we extend this characterization to the whole universal first-order theory of relations. Using our characterization, we show that the positive universal fragment is also decidable.
Cite as

Amina Doumane. Graph Characterization of the Universal Theory of Relations. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 41:1-41:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doumane:LIPIcs.MFCS.2021.41,
  author =	{Doumane, Amina},
  title =	{{Graph Characterization of the Universal Theory of Relations}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{41:1--41:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.41},
  URN =		{urn:nbn:de:0030-drops-144815},
  doi =		{10.4230/LIPIcs.MFCS.2021.41},
  annote =	{Keywords: Relation algebra, Graph homomorphism, Equational theories, First-order logic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.29
On the Logical Strength of Confluence and Normalisation for Cyclic Proofs

Authors: Anupam Das

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of "cyclic proof theory". We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying "coterm" rewriting system of CT within fragments of second-order arithmetic. We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as "coterm" models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity. A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms.
Cite as

Anupam Das. On the Logical Strength of Confluence and Normalisation for Cyclic Proofs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{das:LIPIcs.FSCD.2021.29,
  author =	{Das, Anupam},
  title =	{{On the Logical Strength of Confluence and Normalisation for Cyclic Proofs}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{29:1--29:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.29},
  URN =		{urn:nbn:de:0030-drops-142678},
  doi =		{10.4230/LIPIcs.FSCD.2021.29},
  annote =	{Keywords: confluence, normalisation, system T, circular proofs, reverse mathematics, type structures}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.29
Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms

Authors: Amina Doumane and Damien Pous

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We study the equational theories of composition and intersection on binary relations, with or without their associated neutral elements (identity and full relation). Without these constants, the equational theory coincides with that of semilattice-ordered semigroups. We show that the equational theory is no longer finitely based when adding one or the other constant, refuting a conjecture from the literature. Our proofs exploit a characterisation in terms of graphs and homomorphisms, which we show how to adapt in order to capture standard equational theories over the considered signatures.
Cite as

Amina Doumane and Damien Pous. Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{doumane_et_al:LIPIcs.CONCUR.2020.29,
  author =	{Doumane, Amina and Pous, Damien},
  title =	{{Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.29},
  URN =		{urn:nbn:de:0030-drops-128411},
  doi =		{10.4230/LIPIcs.CONCUR.2020.29},
  annote =	{Keywords: Relation algebra, graph homomorphisms, (in)equational theories}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.45
Cyclic Proofs and Jumping Automata

Authors: Denis Kuperberg, Laureline Pinault, and Damien Pous

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We consider a fragment of a cyclic sequent proof system for Kleene algebra, and we see it as a computational device for recognising languages of words. The starting proof system is linear and we show that it captures precisely the regular languages. When adding the standard contraction rule, the expressivity raises significantly; we characterise the corresponding class of languages using a new notion of multi-head finite automata, where heads can jump.
Cite as

Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs and Jumping Automata. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.FSTTCS.2019.45,
  author =	{Kuperberg, Denis and Pinault, Laureline and Pous, Damien},
  title =	{{Cyclic Proofs and Jumping Automata}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{45:1--45:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.45},
  URN =		{urn:nbn:de:0030-drops-116071},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.45},
  annote =	{Keywords: Cyclic proofs, regular languages, multi-head automata, transducers}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.4
Coinduction: Automata, Formal Proof, Companions (Invited Paper)

Authors: Damien Pous

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
Coinduction is a mathematical tool that is used pervasively in computer science: to program and reason about infinite data-structures, to give semantics to concurrent systems, to obtain automata algorithms. We present some of these applications in automata theory and in formalised mathematics. Then we discuss recent developments on the abstract theory of coinduction and its enhancements.
Cite as

Damien Pous. Coinduction: Automata, Formal Proof, Companions (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{pous:LIPIcs.CALCO.2019.4,
  author =	{Pous, Damien},
  title =	{{Coinduction: Automata, Formal Proof, Companions}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{4:1--4:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.4},
  URN =		{urn:nbn:de:0030-drops-114323},
  doi =		{10.4230/LIPIcs.CALCO.2019.4},
  annote =	{Keywords: Coinduction, Automata, Coalgebra, Formal proofs}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.8
A Certificate-Based Approach to Formally Verified Approximations

Authors: Florent Bréhard, Assia Mahboubi, and Damien Pous

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
We present a library to verify rigorous approximations of univariate functions on real numbers, with the Coq proof assistant. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem. We illustrate this technique on the case of operations of division and square root. This library features a collection of abstract structures that organise the specfication of rigorous approximations, and modularise the related proofs. Finally, we provide an implementation of verified Chebyshev approximations, and we discuss a few examples of computations.
Cite as

Florent Bréhard, Assia Mahboubi, and Damien Pous. A Certificate-Based Approach to Formally Verified Approximations. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brehard_et_al:LIPIcs.ITP.2019.8,
  author =	{Br\'{e}hard, Florent and Mahboubi, Assia and Pous, Damien},
  title =	{{A Certificate-Based Approach to Formally Verified Approximations}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.8},
  URN =		{urn:nbn:de:0030-drops-110638},
  doi =		{10.4230/LIPIcs.ITP.2019.8},
  annote =	{Keywords: approximation theory, Chebyshev polynomials, Banach fixed-point theorem, interval arithmetic, Coq}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.41
Kleene Algebra with Observations

Authors: Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.
Cite as

Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Kleene Algebra with Observations. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 41:1-41:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kappe_et_al:LIPIcs.CONCUR.2019.41,
  author =	{Kapp\'{e}, Tobias and Brunet, Paul and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio},
  title =	{{Kleene Algebra with Observations}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{41:1--41:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.41},
  URN =		{urn:nbn:de:0030-drops-109431},
  doi =		{10.4230/LIPIcs.CONCUR.2019.41},
  annote =	{Keywords: Concurrent Kleene algebra, Kleene algebra with tests, free model, axiomatisation, decision procedure}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.18
Completeness for Identity-free Kleene Lattices

Authors: Amina Doumane and Damien Pous

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete for the equational theory of their relational models. Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.
Cite as

Amina Doumane and Damien Pous. Completeness for Identity-free Kleene Lattices. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{doumane_et_al:LIPIcs.CONCUR.2018.18,
  author =	{Doumane, Amina and Pous, Damien},
  title =	{{Completeness for Identity-free Kleene Lattices}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.18},
  URN =		{urn:nbn:de:0030-drops-95564},
  doi =		{10.4230/LIPIcs.CONCUR.2018.18},
  annote =	{Keywords: Kleene algebra, Graph languages, Petri Automata, Kleene theorem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.19
Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices)

Authors: Anupam Das and Damien Pous

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We prove cut-elimination for a sequent-style proof system which is sound and complete for the equational theory of Kleene algebra, and where proofs are (potentially) non-wellfounded infinite trees. We extend these results to systems with meets and residuals, capturing `star-continuous' action lattices in a similar way. We recover the equational theory of all action lattices by restricting to regular proofs (with cut) - those proofs that are unfoldings of finite graphs.
Cite as

Anupam Das and Damien Pous. Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices). In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.CSL.2018.19,
  author =	{Das, Anupam and Pous, Damien},
  title =	{{Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices)}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.19},
  URN =		{urn:nbn:de:0030-drops-96869},
  doi =		{10.4230/LIPIcs.CSL.2018.19},
  annote =	{Keywords: Kleene algebra, proof theory, sequent system, non-wellfounded proofs}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.60
Treewidth-Two Graphs as a Free Algebra

Authors: Christian Doczkal and Damien Pous

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We give a new and elementary proof that the graphs of treewidth at most two can be seen as a free algebra. This result was originally established through an elaborate analysis of the structure of K_4-free graphs, ultimately reproving the well-known fact that the graphs of treewidth at most two are precisely those excluding K_4 as a minor. Our new proof is based on a confluent and terminating rewriting system for term-labeled graphs and does not involve graph minors anymore. The new strategy is simpler and robust in the sense that it can be adapted to subclasses of treewidth-two graphs, e.g., graphs without self-loops.
Cite as

Christian Doczkal and Damien Pous. Treewidth-Two Graphs as a Free Algebra. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 60:1-60:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{doczkal_et_al:LIPIcs.MFCS.2018.60,
  author =	{Doczkal, Christian and Pous, Damien},
  title =	{{Treewidth-Two Graphs as a Free Algebra}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{60:1--60:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.60},
  URN =		{urn:nbn:de:0030-drops-96429},
  doi =		{10.4230/LIPIcs.MFCS.2018.60},
  annote =	{Keywords: Treewidth, Universal Algebra, Rewriting}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.3
On the Positive Calculus of Relations with Transitive Closure

Authors: Damien Pous

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
Binary relations are such a basic object that they appear in many places in mathematics and computer science. For instance, when dealing with graphs, program semantics, or termination guarantees, binary relations are always used at some point. In this survey, we focus on the relations themselves, and we consider algebraic and algorithmic questions. On the algebraic side, we want to understand and characterise the laws governing the behaviour of the following standard operations on relations: union, intersection, composition, converse, and reflexive-transitive closure. On the algorithmic side, we look for decision procedures for equality or inequality of relations. After having formally defined the calculus of relations, we recall the existing results about two well-studied fragments of particular importance: Kleene algebras and allegories. Unifying those fragments yields a decidable theory whose axiomatisability remains an open problem.
Cite as

Damien Pous. On the Positive Calculus of Relations with Transitive Closure. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{pous:LIPIcs.STACS.2018.3,
  author =	{Pous, Damien},
  title =	{{On the Positive Calculus of Relations with Transitive Closure}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{3:1--3:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.3},
  URN =		{urn:nbn:de:0030-drops-85382},
  doi =		{10.4230/LIPIcs.STACS.2018.3},
  annote =	{Keywords: Relation Algebra, Kleene Algebra, Allegories, Automata, Graphs}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.76
K4-free Graphs as a Free Algebra

Authors: Enric Cosme Llópez and Damien Pous

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Graphs of treewidth at most two are the ones excluding the clique with four vertices as a minor. Equivalently, they are the graphs whose biconnected components are series-parallel. We turn those graphs into a free algebra, answering positively a question by Courcelle and Engelfriet, in the case of treewidth two. First we propose a syntax for denoting them: in addition to series and parallel compositions, it suffices to consider the neutral elements of those operations and a unary transpose operation. Then we give a finite equational presentation and we prove it complete: two terms from the syntax are congruent if and only if they denote the same graph.
Cite as

Enric Cosme Llópez and Damien Pous. K4-free Graphs as a Free Algebra. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 76:1-76:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cosmellopez_et_al:LIPIcs.MFCS.2017.76,
  author =	{Cosme Ll\'{o}pez, Enric and Pous, Damien},
  title =	{{K4-free Graphs as a Free Algebra}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{76:1--76:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.76},
  URN =		{urn:nbn:de:0030-drops-80883},
  doi =		{10.4230/LIPIcs.MFCS.2017.76},
  annote =	{Keywords: Universal Algebra, Graph theory, Axiomatisation, Tree decompositions, Graph minors}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.5
Monoidal Company for Accessible Functors

Authors: Henning Basold, Damien Pous, and Jurriaan Rot

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
Distributive laws between functors are a fundamental tool in the theory of coalgebras. In the context of coinduction in complete lattices, they correspond to the so-called compatible functions, which enable enhancements of the coinductive proof technique. Amongst these, the greatest compatible function, called the companion, has recently been shown to satisfy many good properties. Categorically, the companion of a functor corresponds to the final object in a category of distributive laws. We show that every accessible functor on a locally presentable category has a companion. Central to this and other constructions in the paper is the presentation of distributive laws as coalgebras for a certain functor. This functor itself has again, what we call, a second-order companion. We show how this companion interacts with the various monoidal structures on functor categories. In particular, both the first- and second-order companion give rise to monads. We use these results to obtain an abstract GSOS-like extension result for specifications involving the second-order companion.
Cite as

Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal Company for Accessible Functors. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{basold_et_al:LIPIcs.CALCO.2017.5,
  author =	{Basold, Henning and Pous, Damien and Rot, Jurriaan},
  title =	{{Monoidal Company for Accessible Functors}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.5},
  URN =		{urn:nbn:de:0030-drops-80379},
  doi =		{10.4230/LIPIcs.CALCO.2017.5},
  annote =	{Keywords: coalgebras, distributive laws, accessible functors, monoidal categories}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.28
On Decidability of Concurrent Kleene Algebra

Authors: Paul Brunet, Damien Pous, and Georg Struth

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Concurrent Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets. We use constructions on Petri nets to provide two decision procedures for such pomset languages motivated by the equational and the refinement theory of concurrent Kleene algebra. The contribution to the first problem lies in a much simpler algorithm and an EXPSPACE complexity bound. Decidability of the second, more interesting problem is new and, in fact, EXPSPACE-complete.
Cite as

Paul Brunet, Damien Pous, and Georg Struth. On Decidability of Concurrent Kleene Algebra. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{brunet_et_al:LIPIcs.CONCUR.2017.28,
  author =	{Brunet, Paul and Pous, Damien and Struth, Georg},
  title =	{{On Decidability of Concurrent Kleene Algebra}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.28},
  URN =		{urn:nbn:de:0030-drops-77881},
  doi =		{10.4230/LIPIcs.CONCUR.2017.28},
  annote =	{Keywords: Concurrent Kleene algebra, series-parallel pomsets, Petri nets}
}
  • Refine by Author
  • 14 Pous, Damien
  • 3 Brunet, Paul
  • 3 Doumane, Amina
  • 3 Rot, Jurriaan
  • 2 Das, Anupam
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Logic
  • 3 Theory of computation → Regular languages
  • 2 Mathematics of computing → Discrete mathematics
  • 2 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Proof theory
  • Show More...

  • Refine by Keyword
  • 4 Kleene algebra
  • 2 Automata
  • 2 Concurrent Kleene algebra
  • 2 Coq
  • 2 Relation algebra
  • Show More...

  • Refine by Type
  • 17 document

  • Refine by Publication Year
  • 4 2018
  • 4 2019
  • 3 2017
  • 2 2021
  • 1 2015
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact