Search

Your search keyword '"Goubault, Eric"' showing total 15 results
Start Over Author "Goubault, Eric" Publisher hal ccsd
15 results on '"Goubault, Eric"'

1. Solving N-player dynamic routing games with congestion: a mean field approach

Author

Cabannes, Theophile, Lauriere, Mathieu, Perolat, Julien, Marinier, Raphael, Girgin, Sertan, Perrin, Sarah, Pietquin, Olivier, Bayen, Alexandre, Goubault, Eric, Elie, Romuald, Scool (Scool), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), and Perrin, Sarah

Subjects
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI], Networking and Internet Architecture (cs.NI), FOS: Computer and information sciences, [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], [INFO.INFO-NE] Computer Science [cs]/Neural and Evolutionary Computing [cs.NE], Dynamical Systems (math.DS), Systems and Control (eess.SY), [INFO.INFO-NE]Computer Science [cs]/Neural and Evolutionary Computing [cs.NE], Electrical Engineering and Systems Science - Systems and Control, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Computer Science - Networking and Internet Architecture, Optimization and Control (math.OC), [INFO.INFO-MA]Computer Science [cs]/Multiagent Systems [cs.MA], [INFO.INFO-GT] Computer Science [cs]/Computer Science and Game Theory [cs.GT], FOS: Mathematics, FOS: Electrical engineering, electronic engineering, information engineering, Computer Science - Multiagent Systems, [INFO.INFO-MA] Computer Science [cs]/Multiagent Systems [cs.MA], Mathematics - Dynamical Systems, Mathematics - Optimization and Control, Multiagent Systems (cs.MA)
Abstract

The recent emergence of navigational tools has changed traffic patterns and has now enabled new types of congestion-aware routing control like dynamic road pricing. Using the fundamental diagram of traffic flows - applied in macroscopic and mesoscopic traffic modeling - the article introduces a new N-player dynamic routing game with explicit congestion dynamics. The model is well-posed and can reproduce heterogeneous departure times and congestion spill back phenomena. However, as Nash equilibrium computations are PPAD-complete, solving the game becomes intractable for large but realistic numbers of vehicles N. Therefore, the corresponding mean field game is also introduced. Experiments were performed on several classical benchmark networks of the traffic community: the Pigou, Braess, and Sioux Falls networks with heterogeneous origin, destination and departure time tuples. The Pigou and the Braess examples reveal that the mean field approximation is generally very accurate and computationally efficient as soon as the number of vehicles exceeds a few dozen. On the Sioux Falls network (76 links, 100 time steps), this approach enables learning traffic dynamics with more than 14,000 vehicles.

Published
2021

2. Reasoning about Uncertainties in Discrete-Time Dynamical Systems using Polynomial Forms

Author

Sankaranarayanan, Sriram, Chou, Yi, Goubault, Eric, Putot, Sylvie, University of Colorado [Boulder], LIX, Ecole Polytechnique/CNRS, Institut Polytechnique de Paris, and Putot, Sylvie

Subjects
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI], [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
Abstract

International audience; In this paper, we propose polynomial forms to represent distributions of state variables over time for discrete-time stochastic dynamical systems. This problem arises in a variety of applications in areas ranging from biology to robotics. Our approach allows us to rigorously represent the probability distribution of state variables over time, and provide guaranteed bounds on the expectations, moments and probabilities of tail events involving the state variables. First, we recall ideas from interval arithmetic, and use them to rigorously represent the state variables at time t as a function of the initial state variables and noise symbols that model the random exogenous inputs encountered before time t. Next, we show how concentration of measure inequalities can be employed to prove rigorous bounds on the tail probabilities of these state variables. We demonstrate interesting applications that demonstrate how our approach can be useful in some situations to establish mathematically guaranteed bounds that are of a different nature from those obtained through simulations with pseudo-random numbers.

Published
2020

3. Algebraic coherent confluence and higher-dimensional globular Kleene algebras

Author

Calk, Cameron, Malbos, Philippe, Goubault, Eric, Struth, Georg, Institut Camille Jordan [Villeurbanne] (ICJ), École Centrale de Lyon (ECL), Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université Jean Monnet [Saint-Étienne] (UJM)-Institut National des Sciences Appliquées de Lyon (INSA Lyon), and Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Computer Science::Logic in Computer Science, confluence, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], Computer Science::Programming Languages, Modal Kleene algebras, higher-dimensional rewriting, M.S.C. 2010 -68Q65, 03B35, 18D05, Computer Science::Formal Languages and Automata Theory, coherence, [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT]
Abstract

We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent proofs by confluence. To this end, we introduce the structure of modal higher-dimensional globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We give a calculation of a coherent Church-Rosser theorem and Newman's lemma in higher-dimensional Kleene algebras. We interpret these results in the context of higher-dimensional rewriting systems described by polygraphs.

Published
2020

4. The Directed Homotopy Hypothesis

Author

Dubut, Jérémy, Goubault, Eric, Goubault-Larrecq, Jean, Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), and Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)

Subjects
060201 languages & linguistics, 000 Computer science, knowledge, general works, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 06 humanities and the arts, 02 engineering and technology, Mathematics::Algebraic Topology, Mathematics::K-Theory and Homology, Mathematics::Category Theory, [MATH.MATH-AT]Mathematics [math]/Algebraic Topology [math.AT], 0602 languages and literature, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, ComputingMilieux_MISCELLANEOUS
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.

Published
2016

5. Bisimulations and unfolding in P-accessible categorical models

Author

Dubut, Jérémy, Goubault, Eric, Goubault-Larrecq, Jean, Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), and Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)

Subjects
000 Computer science, knowledge, general works, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Mathematics::Category Theory, Computer Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ComputingMilieux_MISCELLANEOUS
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.

Published
2016

6. Eigenvectors of Non-Linear Maps on the Cone of Positive Semidefinite Matrices Application to Stability Analysis

Author

Stott, Nikolas, Allamigeon, Xavier, Gaubert, Stéphane, Goubault, Eric, Putot, Sylvie, Max-plus algebras and mathematics of decision (MAXPLUS), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), and Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)

Subjects
ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, MathematicsofComputing_NUMERICALANALYSIS, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC]
Abstract

International audience; We show that the problem of synthesis of a common Lyapunov function for some classes of switched linear systems can be approached by solving an eigenproblem involving a nonlinear map on the cone of positive semidefinite matrices. This map involves the selection of a maximal lower bound of a family of matrices in this cone. We present some variants of the power algorithm, allowing one to solve the nonlinear eigenproblem in a scalable way.

Published
2015

7. Design of Fixed-Point Embedded Systems (defis) French ANR Project

Author

Ménard, Daniel, Rocher, Romuald, Sentieys, Olivier, Simon, Nicolas, Didier, Laurent-Stéphane, Hilaire, Thibault, Lopez, Benoît, Goubault, Eric, Putot, Sylvie, Vedrine, Franck, Najahi, Mohamed Amine, Revy, Guillaume, Fangain, Laurent, Samoyeau, Christian, Lemonnier, Fabrice, Clienti, Christophe, Revy, Guillaume, Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA), Energy Efficient Computing ArchItectures with Embedded Reconfigurable Resources (CAIRN), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-ARCHITECTURE (IRISA-D3), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Performance et Qualité des Algorithmes Numériques (PEQUAN), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Digits, Architectures et Logiciels Informatiques (DALI), Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier (LIRMM), Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Perpignan Via Domitia (UPVD), InPixal [Rennes], InPixal, Embedded System Lab (ESL), Thales Research and Technology, Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), and Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Université de Perpignan Via Domitia (UPVD)

Subjects
[INFO.INFO-TS]Computer Science [cs]/Signal and Image Processing, [INFO.INFO-TS] Computer Science [cs]/Signal and Image Processing, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, [INFO.INFO-AO] Computer Science [cs]/Computer Arithmetic, [SPI.SIGNAL]Engineering Sciences [physics]/Signal and Image processing, [SPI.SIGNAL] Engineering Sciences [physics]/Signal and Image processing
Abstract

International audience; Embedded applications are usually coming with stringent constraints in term of cost, energy consumption and real-time. Consequently, fixed-point arithmetic is mainstream for their implementation into embedded systems. Hence, the main objective of the french ANR project DEFIS is to provide a complete design flow for fixed-point refinement of complex applications. This tool flow is like the missing link between high-level application specification tools and low-level implementation.

Published
2012

8. The tropical double description method

Author

Allamigeon, Xavier, Gaubert, Stéphane, Goubault, Eric, Bureaux des transports, Ministère du Budget, des Comptes publics, de la fonction publique et de la Réforme de l'État, Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), EADS Innovation Works [Suresnes] (EADS IW), EADS - European Aeronautic Defense and Space, Max-plus algebras and mathematics of decision (MAXPLUS), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Inria Nancy Grand Est & Loria, Jean-Yves Marion and Thomas Schwentick, and Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))

Subjects
Computational Geometry (cs.CG), FOS: Computer and information sciences, F.2.2, G.2.2, Discrete Mathematics (cs.DM), algorithmics and combinatorics of tropical polyhedra, convexity in tropical algebra, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], [INFO.INFO-CG]Computer Science [cs]/Computational Geometry [cs.CG], ACM: G.: Mathematics of Computing/G.2: DISCRETE MATHEMATICS/G.2.2: Graph Theory, static analysis, ACM: F.: Theory of Computation/F.2: ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY/F.2.2: Nonnumerical Algorithms and Problems, computational geometry, Computer Science - Computational Geometry, discrete event systems, Computer Science - Discrete Mathematics
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., Comment: 12 pages, prepared for the Proceedings of the Symposium on Theoretical Aspects of Computer Science, 2010, Nancy, France

Published
2010

9. Space Software Validation using Abstract Interpretation

Author

Bouissou, Olivier, Conquet, Eric, Cousot, Patrick, Cousot, Radhia, Feret, Jérôme, Ghorbal, Khalil, Goubault, Eric, Lesens, David, Mauborgne, Laurent, Miné, Antoine, Putot, Sylvie, Rival, Xavier, Turin, Michel, Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), European Space Research and Technology Centre (ESTEC), Agence Spatiale Européenne = European Space Agency (ESA), Laboratoire d'informatique de l'école normale supérieure (LIENS), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Abstract Interpretation and Static Analysis (ABSTRACTION), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Astrium Space Transportation (AST), ASTRIUM, GTI6, ESA contract ITI19783, EUROSPACE, Laboratoire d'Intégration des Systèmes et des Technologies (LIST), European Space Agency (ESA), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Inria Paris-Rocquencourt, Feret, Jérôme, École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS), Département d'informatique de l'École normale supérieure (DI-ENS), and Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris)

Subjects
[INFO.INFO-OH] Computer Science [cs]/Other [cs.OH], Space software, Static Analysis, Validation, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Abstract interpretation
Abstract

International audience; This paper reports the results of an ESA funded project on the use of abstract interpretation to validate critical real-time embedded space software. Abstract interpretation is industrially used since several years, especially for the validation of the Ariane 5 launcher. However, the limitations of the tools used so far prevented a wider deployment. Astrium Space Transportation, CEA, and ENS have analyzed the performances of two recent tools on a case study extracted from the safety software of the ATV: * ASTRÉE, developed by ENS and CNRS, to check for run-time errors, * FLUCTUAT, developed by CEA, to analyse the accuracy of numerical computations. The conclusion of the study is that the performance of this new generation of tools has dramatically increased (no false alarms and fine analysis of numerical precision).

Published
2009

10. Components of the Fundamental Category II

Author

Goubault, Eric, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), and Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))

Subjects
fundamental category, Mathematics::Category Theory, dihomotopy, [MATH.MATH-AT]Mathematics [math]/Algebraic Topology [math.AT], category of components, po-space, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC]
Abstract

International audience; In this article we carry on the study of the fundamental category of a partially ordered topological space, as arising in e.g. concurrency theory, initiated in [APCS 12/1, 2004]. The ``algebra'' of dipaths modulo dihomotopy (the fundamental category) of such a po-space is essentially finite in a number of situations. We give new definitions of the component category that are more tractable than the one of [APCS 12/1, 2004], as well as give definitions of future and past component categories, related to the past and future models of [Grandis 2003]. The component category is defined as a category of fractions, but it can be shown to be equivalent to a quotient category, much easier to portray. A van Kampen theorem is known to be available on fundamental categories [Grandis 2001, Goubault 2001], we show in this paper a similar theorem for component categories (conjectured in [APCS 12/1, 2004]). This proves useful for inductively computing the component category in some circumstances, for instance, in the case of simple PV mutual exclusion models [CONCUR 2005], corresponding to partially ordered subspaces of R^n minus isothetic hyperrectangles. In this last case again, we conjecture (and give some hints) that component categories enjoy some nice adjunction relations directly with the fundamental category.

Published
2007

11. Algebraic Topology and Concurrency

Author

Goubault, Eric, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), and Laboratoire d'Intégration des Systèmes et des Technologies (LIST)

Subjects
Higher-dimensional automata, Partially ordered space, [MATH.MATH-AT]Mathematics [math]/Algebraic Topology [math.AT], Concurrency, Partial order, Computer Science::Programming Languages, Homotopy, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Cubical set
Abstract

International audience; We show in this article that some concepts from homotopy theory, in algebraic topology, are relevant for studying concurrent programs. We exhibit a natural semantics of semaphore programs, based on partially ordered topological spaces, which are studied up to “elastic deformation” or homotopy, giving information about important properties of the program, such as deadlocks, unreachables, serializability, essential schedules, etc. In fact, it is not quite ordinary homotopy that has to be used, but rather a “directed homotopy” that does not reverse the flow of time. We show some of the essential differences between ordinary and directed homotopy through examples. We also relate the topological view to a combinatorial view of concurrent programs closer to transition systems, through the notion of a cubical set. Finally we apply some of these concepts to the proof of the safeness of a two-phase protocol, well-known and used in concurrent database theory. We end up with a list of problems from both a mathematical and a computer-scientific point of view.

Published
2006

12. Components of the fundamental category

Author

Goubault, Eric, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), and Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))

Subjects
lr-system, fundamental category, category of fractions, weakly invertible morphism, Mathematics::Category Theory, dihomotopy, [MATH.MATH-AT]Mathematics [math]/Algebraic Topology [math.AT], component, pure system, po-space, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], invertible morphism
Abstract

International audience; In this article we study the fundamental category (Goubault and Raussen, 2002; Goubault, 2000) of a partially ordered topological space (Nachbin, 1965; Johnstone, 1982), as arising in, e.g., concurrency theory (Fajstrup et al., 1999). The ldquoalgebrardquo of dipaths modulo dihomotopy (the fundamental category) of such a po-space is essentially finite in a number of situations: We define a component category of a category of fractions with respect to a suitable system, which contains all relevant information. Furthermore, some of these simpler invariants are conjectured to also satisfy some form of a van Kampen theorem, as the fundamental category does (Goubault, 2002; Grandis, 2001). We end up by giving some hints about how to carry out some computations in simple cases.

Published
2004

13. Some geometric perspectives on concurrency theory

Author

Goubault, Eric, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), and Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))

Subjects
omega category, fundamental category, dihomotopy, [MATH.MATH-AT]Mathematics [math]/Algebraic Topology [math.AT], cubical set, po-space, van Kampen, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], concurrency theory
Abstract

International audience; Concurrency, i.e., the domain in computer science which deals with parallel (asynchronous) computations, has very strong links with algebraic topology; this is what we are developing in this paper, giving a survey of ``geometric'' models for concurrency. We show that the properties we want to prove on concurrent systems are stable under some form of deformation, which is almost homotopy. In fact, as the ``direction'' of time matters, we have to allow deformation only as long as we do not reverse the direction of time. This calls for a new homotopy theory: ``directed'' or di-homotopy. We develop some of the geometric intuition behind this theory and give some hints about the algebraic objects one can associate with it (in particular homology groups). For some historic as well as for some deeper reasons, the theory is at a stage where there is a nice blend between cubical, omega-categorical and topological techniques.

Published
2003

14. Order-theoretic, geometric and combinatorial models of intuitionistic S4 proofs

Author

Goubault-Larrecq, Jean, Goubault, Eric, Formal Specifications and Program Validation (COQ), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), GIE Dyade, CEA- Saclay (CEA), Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Département d'Architectures, Conception et Logiciels Embarqués-LETI (DACLE-LETI), Commissariat à l'énergie atomique et aux énergies alternatives - Laboratoire d'Electronique et de Technologie de l'Information (CEA-LETI), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Grenoble Alpes (UGA), and Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])

Subjects
Mathematics::Category Theory, Computer Science::Logic in Computer Science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; We propose a few models of proof terms for the intuitionistic modal propositional logic S4. Some of them are based on partial orders, or cpos, or dcpos, some of them on a suitable category of topological spaces and continuous maps. A structure that emerges from these interpretations is that of augmented simplicial sets. This leads to so-called combinatorial models, where simplices play an important role: the point is that the simplicial structure interprets the 2 modality, and that the category of augmented simplicial sets is itself already a model of intuitionistic propositional S4 proof terms. In fact, this category is an elementary topos, and is therefore a prime candidate to interpret all proof terms for intuitionistic S4 set theory. Finally, we suggest that geometric-like realizations functors provide a recipe to build other models of intuitionistic propositional S4 proof terms

Published
1999

15. Certification of a Numerical Result: Use of Interval Arithmetic and Multiple Precision

Author

Nguyen, Hong Diep, Revol, Nathalie, Computer arithmetic (ARENAIRE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), Fainekos, Georgios and Goubault, Eric and Putot, Sylvie, ANR-06-BLAN-0257,EVA-Flo,Evaluation et Validation Automatique pour le calcul Flottant(2006), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)

Subjects
ACM: G.: Mathematics of Computing/G.4: MATHEMATICAL SOFTWARE/G.4.6: Reliability and robustness, ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.8: Validation, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, error bound, iterative refinement, ACM: G.: Mathematics of Computing/G.1: NUMERICAL ANALYSIS/G.1.3: Numerical Linear Algebra, multiple precision, interval arithmetic
Abstract

International audience; Using floating-point arithmetic to solve a numerical problem yields a computed result, which is an approximation of the exact solution because of roundoff errors. In this paper, we present an approach to certify the computed solution. Here, "certify" means computing a guaranteed enclosure of the error between the computed, approximate, result and the exact, unknown result. We discuss an iterative refinement method: classically, such methods aim at computing an approximation of the error and they add it to the previous result to improve its accuracy. We add two ingredients: interval arithmetic is used to get an enclosure of the error instead of an approximation, and multiple precision is used to reach higher accuracy. We exemplify this approach on the certification of the solution of a linear system.

Published
2010

Catalog

Books, media, physical & digital resources
See catalog results