arXiv subjects

Emmanuel Haucourt

Publications and source records attributed to Emmanuel Haucourt.

7 recordsLinked to original sources

arXiv2025

Non-Hausdorff manifolds over locally ordered spaces via sheaf theory

Locally ordered spaces can be used as topological models of concurrent programs: the local order models the irreversibility of time during execution. Under certain conditions, one can even work with locally ordered manifolds. In this paper, we build the universal euclidean local order over every locally ordered space; in categorical terms, the subcategory of euclidean local orders is coreflective in the category of locally ordered spaces. Our construction is based on a well-known correspondance between sheaves and \'etale bundles. This is a far reaching generalization of a result about realizations of graph products. We particularize the construction to locally ordered realization of precubical sets, and show that it admits a purely combinatorial description. With the same proof techniques, we show that, unlike for the topological realization, there is a unique (up to symmetry) precubical set whose locally ordered realization is isomorphic to $\mathbb{R}^n$.

math.AT↗

arXiv2024

Strict refinement property of connected loop-free categories

In this paper we study the strict refinement property for connected partial ordersalso known as Hashimoto's Theorem. This property implies that any isomorphismbetween products of irreducible structures is determined is uniquely determinedas a product of isomorphisms between the factors. This refinement implies asort of smallest possible decomposition for such structures. After a brief recallof the necessary notion we prove that Hashimoto's theorem can be extendedto connected loop-free categories, i.e. categories with no non-trivial morphismsendomorphisms. A special case of such categories is the category of connectedcomponents, for concurrent programs without loops.

math.CT↗

arXiv2021

Non-existing and ill-behaved coequalizers of locally ordered spaces

Categories of locally ordered spaces are especially well-adapted to the realization of most precubical sets, though their colimits are not so easy to determine (in comparison with colimits in the category of d-spaces for example). We use the plural here, as the notion of a locally ordered space vary from an author to another, only differing according to seemingly anodyne technical details. As we explain in this article, these differences have dramatic consequences on colimits. In particular, we show that most categories of locally ordered spaces are not cocomplete, thus answering a question that was neglected so far. The strategy is the following: given a directed loop γ on a locally ordered space X, we try to identify the image of γ with a single point. If it were taken in the category of d-spaces, such an identification would be likely to create a vortex, while locally ordered spaces have no vortices. Concretely, the antisymmetry of local orders gets more points to be identified than in a mere topological quotient. However, the effect of this phenomenon is in some sense limited to the neighbourhood of (the image of) γ. So the existence and the nature of the corresponding coequalizer strongly depends on the topology around the image of γ. As an extreme example, if the latter forms a connected component, the coequalizer exists and its underlying space matches with the topological coequalizer.

math.GN↗

arXiv2014

The Boolean Algebra of Cubical Areas as a Tensor Product in the Category of Semilattices with Zero

In this paper we describe a model of concurrency together with an algebraic structure reflecting the parallel composition. For the sake of simplicity we restrict to linear concurrent programs i.e. the ones with no loops nor branching. Such programs are given a semantics using cubical areas. Such a semantics is said to be geometric. The collection of all these cubical areas enjoys a structure of tensor product in the category of semi-lattice with zero. These results naturally extend to fully fledged concurrent programs up to some technical tricks.

cs.LO↗

arXiv2012

Trace Spaces: an Efficient New Technique for State-Space Reduction

State-space reduction techniques, used primarily in model-checkers, all rely on the idea that some actions are independent, hence could be taken in any (respective) order while put in parallel, without changing the semantics. It is thus not necessary to consider all execution paths in the interleaving semantics of a concurrent program, but rather some equivalence classes. The purpose of this paper is to describe a new algorithm to compute such equivalence classes, and a representative per class, which is based on ideas originating in algebraic topology. We introduce a geometric semantics of concurrent languages, where programs are interpreted as directed topological spaces, and study its properties in order to devise an algorithm for computing dihomotopy classes of execution paths. In particular, our algorithm is able to compute a control-flow graph for concurrent programs, possibly containing loops, which is "as reduced as possible" in the sense that it generates traces modulo equivalence. A preliminary implementation was achieved, showing promising results towards efficient methods to analyze concurrent programs, with very promising results compared to partial-order reduction techniques.

cs.DC↗

arXiv2011

Covering space theory for directed topology

The state space of a machine admits the structure of time. For example, the geometric realization of a precubical set, a generalization of an unlabeled asynchronous transition system, admits a "local preorder" encoding control flow. In the case where time does not loop, the "locally preordered" state space splits into causally distinct components. The set of such components often gives a computable invariant of machine behavior. In the general case, no such meaningful partition could exist. However, as we show in this note, the locally preordered geometric realization of a precubical set admits a "locally monotone" covering from a state space in which time does not loop. Thus we hope to extend geometric techniques in static program analysis to looping processes.

math.AT↗

arXiv2010

A Geometric Approach to the Problem of Unique Decomposition of Processes

This paper proposes a geometric solution to the problem of prime decomposability of concurrent processes first explored by R. Milner and F. Moller in [MM93]. Concurrent programs are given a geometric semantics using cubical areas, for which a unique factorization theorem is proved. An effective factorization method which is correct and complete with respect to the geometric semantics is derived from the factorization theorem. This algorithm is implemented in the static analyzer ALCOOL.

cs.LO↗