9 Search Results for "Goubault, Éric"

Document
DOI: 10.4230/LIPIcs.CSL.2024.30
A Many-Sorted Epistemic Logic for Chromatic Hypergraphs

Authors: Éric Goubault, Roman Kniazev, and Jérémy Ledent

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We propose a many-sorted modal logic for reasoning about knowledge in multi-agent systems. Our logic introduces a clear distinction between participating agents and the environment. This allows to express local properties of agents and global properties of worlds in a uniform way, as well as to talk about the presence or absence of agents in a world. The logic subsumes the standard epistemic logic and is a conservative extension of it. The semantics is given in chromatic hypergraphs, a generalization of chromatic simplicial complexes, which were recently used to model knowledge in distributed systems. We show that the logic is sound and complete with respect to the intended semantics. We also show a further connection of chromatic hypergraphs with neighborhood frames.
Cite as

Éric Goubault, Roman Kniazev, and Jérémy Ledent. A Many-Sorted Epistemic Logic for Chromatic Hypergraphs. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.CSL.2024.30,
  author =	{Goubault, \'{E}ric and Kniazev, Roman and Ledent, J\'{e}r\'{e}my},
  title =	{{A Many-Sorted Epistemic Logic for Chromatic Hypergraphs}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.30},
  URN =		{urn:nbn:de:0030-drops-196730},
  doi =		{10.4230/LIPIcs.CSL.2024.30},
  annote =	{Keywords: Modal logics, epistemic logics, multi-agent systems, hypergraphs}
}
Document
DOI: 10.4230/LIPIcs.STACS.2022.33
A Simplicial Model for KB4_n: Epistemic Logic with Agents That May Die

Authors: Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum

Published in: LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)

Abstract
The standard semantics of multi-agent epistemic logic S5_n is based on Kripke models whose accessibility relations are reflexive, symmetric and transitive. This one dimensional structure contains implicit higher-dimensional information beyond pairwise interactions, that we formalized as pure simplicial models in a previous work in Information and Computation 2021 [Éric Goubault et al., 2021]. Here we extend the theory to encompass simplicial models that are not necessarily pure. The corresponding class of Kripke models are those where the accessibility relation is symmetric and transitive, but might not be reflexive. Such models correspond to the epistemic logic KB4_n. Impure simplicial models arise in situations where two possible worlds may not have the same set of agents. We illustrate it with distributed computing examples of synchronous systems where processes may crash.
Cite as

Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum. A Simplicial Model for KB4_n: Epistemic Logic with Agents That May Die. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.STACS.2022.33,
  author =	{Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Rajsbaum, Sergio},
  title =	{{A Simplicial Model for KB4\underlinen: Epistemic Logic with Agents That May Die}},
  booktitle =	{39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-222-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{219},
  editor =	{Berenbrink, Petra and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.33},
  URN =		{urn:nbn:de:0030-drops-158434},
  doi =		{10.4230/LIPIcs.STACS.2022.33},
  annote =	{Keywords: Epistemic logic, Simplicial complexes, Distributed computing}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2021.4
Borel Sets in Reverse Mathematics (Invited Talk)

Authors: Linda Westrick

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
We present what is known about the reverse mathematical strength of weak theorems involving Borel sets.
Cite as

Linda Westrick. Borel Sets in Reverse Mathematics (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{westrick:LIPIcs.CSL.2021.4,
  author =	{Westrick, Linda},
  title =	{{Borel Sets in Reverse Mathematics}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.4},
  URN =		{urn:nbn:de:0030-drops-134387},
  doi =		{10.4230/LIPIcs.CSL.2021.4},
  annote =	{Keywords: Borel sets, reverse mathematics, measure, category}
}
Document
DOI: 10.4230/LIPIcs.DISC.2019.21
Wait-Free Solvability of Equality Negation Tasks

Authors: Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum

Published in: LIPIcs, Volume 146, 33rd International Symposium on Distributed Computing (DISC 2019)

Abstract
We introduce a family of tasks for n processes, as a generalization of the two process equality negation task of Lo and Hadzilacos (SICOMP 2000). Each process starts the computation with a private input value taken from a finite set of possible inputs. After communicating with the other processes using immediate snapshots, the process must decide on a binary output value, 0 or 1. The specification of the task is the following: in an execution, if the set of input values is large enough, the processes should agree on the same output; if the set of inputs is small enough, the processes should disagree; and in-between these two cases, any output is allowed. Formally, this specification depends on two threshold parameters k and l, with k<l, indicating when the cardinality of the set of inputs becomes "small" or "large", respectively. We study the solvability of this task depending on those two parameters. First, we show that the task is solvable whenever k+2 <= l. For the remaining cases (l = k+1), we use various combinatorial topology techniques to obtain two impossibility results: the task is unsolvable if either k <= n/2 or n-k is odd. The remaining cases are still open.
Cite as

Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum. Wait-Free Solvability of Equality Negation Tasks. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.DISC.2019.21,
  author =	{Goubault, \'{E}ric and Lazi\'{c}, Marijana and Ledent, J\'{e}r\'{e}my and Rajsbaum, Sergio},
  title =	{{Wait-Free Solvability of Equality Negation Tasks}},
  booktitle =	{33rd International Symposium on Distributed Computing (DISC 2019)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-126-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{146},
  editor =	{Suomela, Jukka},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2019.21},
  URN =		{urn:nbn:de:0030-drops-113288},
  doi =		{10.4230/LIPIcs.DISC.2019.21},
  annote =	{Keywords: Equality negation, distributed computability, combinatorial topology}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2018.28
Concurrent Specifications Beyond Linearizability

Authors: Éric Goubault, Jérémy Ledent, and Samuel Mimram

Published in: LIPIcs, Volume 125, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018)

Abstract
With the advent of parallel architectures, distributed programs are used intensively and the question of how to formally specify the behaviors expected from such programs becomes crucial. A very general way to specify concurrent objects is to simply give the set of all the execution traces that we consider correct for the object. In many cases, one is only interested in studying a subclass of these concurrent specifications, and more convenient tools such as linearizability can be used to describe them. In this paper, what we call a concurrent specification will be a set of execution traces that moreover satisfies a number of axioms. As we argue, these are actually the only concurrent specifications of interest: we prove that, in a reasonable computational model, every program satisfies all of our axioms. Restricting to this class of concurrent specifications allows us to formally relate our concurrent specifications with the ones obtained by linearizability, as well as its more recent variants (set- and interval-linearizability).
Cite as

Éric Goubault, Jérémy Ledent, and Samuel Mimram. Concurrent Specifications Beyond Linearizability. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.OPODIS.2018.28,
  author =	{Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Mimram, Samuel},
  title =	{{Concurrent Specifications Beyond Linearizability}},
  booktitle =	{22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-098-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{125},
  editor =	{Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.28},
  URN =		{urn:nbn:de:0030-drops-100888},
  doi =		{10.4230/LIPIcs.OPODIS.2018.28},
  annote =	{Keywords: concurrent specification, concurrent object, linearizability}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2018.50
Brief Announcement: On the Impossibility of Detecting Concurrency

Authors: Éric Goubault, Jérémy Ledent, and Samuel Mimram

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
We identify a general principle of distributed computing: one cannot force two processes running in parallel to see each other. This principle is formally stated in the context of asynchronous processes communicating through shared objects, using trace-based semantics. We prove that it holds in a reasonable computational model, and then study the class of concurrent specifications which satisfy this property. This allows us to derive a Galois connection theorem for different variants of linearizability.
Cite as

Éric Goubault, Jérémy Ledent, and Samuel Mimram. Brief Announcement: On the Impossibility of Detecting Concurrency. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 50:1-50:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{goubault_et_al:LIPIcs.DISC.2018.50,
  author =	{Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Mimram, Samuel},
  title =	{{Brief Announcement: On the Impossibility of Detecting Concurrency}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{50:1--50:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.50},
  URN =		{urn:nbn:de:0030-drops-98392},
  doi =		{10.4230/LIPIcs.DISC.2018.50},
  annote =	{Keywords: concurrent specification, concurrent object, linearizability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.9
The Directed Homotopy Hypothesis

Authors: Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be "equivalent" to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g., for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be "equivalent" to a weak form of topologically enriched categories, still very close to (infinite,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.
Cite as

Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. The Directed Homotopy Hypothesis. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dubut_et_al:LIPIcs.CSL.2016.9,
  author =	{Dubut, J\'{e}r\'{e}my and Goubault, Eric and Goubault-Larrecq, Jean},
  title =	{{The Directed Homotopy Hypothesis}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.9},
  URN =		{urn:nbn:de:0030-drops-65492},
  doi =		{10.4230/LIPIcs.CSL.2016.9},
  annote =	{Keywords: directed algebraic topology, partially enriched categories, homotopy hypothesis, geometric models for concurrency, higher category theory}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.25
Bisimulations and Unfolding in P-Accessible Categorical Models

Authors: Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
In this paper, we propose a categorical framework for bisimulations and unfoldings that unifies the classical approach from Joyal and al. via open maps and unfoldings. This is based on a notion of categories accessible with respect to a subcategory of path shapes, i.e., for which one can define a nice notion of trees as glueing of paths. We prove that transitions systems and pre sheaf models are a particular case of our framework. We also prove that in our framework, several characterizations of bisimulation coincide, in particular an "operational one" akin to the standard definition in transition systems. Also, accessibility is preserved by coreflexions. We then design a notion of unfolding, which has good properties in the accessible case: its is a right adjoint and is a universal covering, i.e., initial among the morphisms that have the unique lifting property with respect to path shapes. As an application, we prove that the universal covering of a groupoid, a standard construction in algebraic topology, coincides with an unfolding, when the category of path shapes is well chosen.
Cite as

Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. Bisimulations and Unfolding in P-Accessible Categorical Models. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 25:1-25:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dubut_et_al:LIPIcs.CONCUR.2016.25,
  author =	{Dubut, J\'{e}r\'{e}my and Goubault, Eric and Goubault-Larrecq, Jean},
  title =	{{Bisimulations and Unfolding in P-Accessible Categorical Models}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{25:1--25:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.25},
  URN =		{urn:nbn:de:0030-drops-61555},
  doi =		{10.4230/LIPIcs.CONCUR.2016.25},
  annote =	{Keywords: categorical models, bisimulation, coreflexions, unfolding, universal covering}
}
Document
DOI: 10.4230/LIPIcs.STACS.2010.2443
The Tropical Double Description Method

Authors: Xavier Allamigeon, Stéphane Gaubert, and Éric Goubault

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
We develop a tropical analogue of the classical double description method allowing one to compute an internal representation (in terms of vertices) of a polyhedron defined externally (by inequalities). The heart of the tropical algorithm is a characterization of the extreme points of a polyhedron in terms of a system of constraints which define it. We show that checking the extremality of a point reduces to checking whether there is only one minimal strongly connected component in an hypergraph. The latter problem can be solved in almost linear time, which allows us to eliminate quickly redundant generators. We report extensive tests (including benchmarks from an application to static analysis) showing that the method outperforms experimentally the previous ones by orders of magnitude. The present tools also lead to worst case bounds which improve the ones provided by previous methods.
Cite as

Xavier Allamigeon, Stéphane Gaubert, and Éric Goubault. The Tropical Double Description Method. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 47-58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{allamigeon_et_al:LIPIcs.STACS.2010.2443,
  author =	{Allamigeon, Xavier and Gaubert, St\'{e}phane and Goubault, \'{E}ric},
  title =	{{The Tropical Double Description Method}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{47--58},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2443},
  URN =		{urn:nbn:de:0030-drops-24435},
  doi =		{10.4230/LIPIcs.STACS.2010.2443},
  annote =	{Keywords: Convexity in tropical algebra, algorithmics and combinatorics of tropical polyhedra, computational geometry, discrete event systems, static analysis}
}
  • Refine by Author
  • 6 Goubault, Éric
  • 5 Ledent, Jérémy
  • 2 Dubut, Jérémy
  • 2 Goubault, Eric
  • 2 Goubault-Larrecq, Jean
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Concurrency
  • 2 Theory of computation → Modal and temporal logics
  • 1 Theory of computation → Constructive mathematics

  • Refine by Keyword
  • 2 concurrent object
  • 2 concurrent specification
  • 2 linearizability
  • 1 Borel sets
  • 1 Convexity in tropical algebra
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 2 2016
  • 2 2019
  • 1 2010
  • 1 2018
  • 1 2021
  • 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