Paris Automata and Concurrency Theory Seminar

Venue: LACL, Université Paris Est Créteil

Speaker 1: (present) Burkhart Wolff, LMF

Title: A Comprehensive Formal Theory of Concurrency

► Abstract:

We report on a major formalisation project in Isabelle/HOL covering the theory of “Communicating Sequential Processes” (CSP). CSP, which has been developed in the 80ies and 90ies, comprises denotational, algebraic and operational facets of concurrency and is still considered as a kind of “gold standard” in the field of process-algebras and corresponding refinement techniques. HOL-CSP is a conservative extension of CSP and can cope both with infinite behaviour and infinite data.
Joint work with Safouan Taha, Benoit Ballenghien, Adrien Durier, and Benjamin Puyobro.

Speaker 2: (online) Catarina Faustino, Universidade do Minho, Portugal

Title: On the topology of Higher-Dimensional Automata

► Abstract:

As amply demonstrated in the literature, concepts and methods from algebraic topology can be profitably employed in concurrency theory. A powerful combinatorial-topological model for concurrent systems is given by higher-dimensional automata. The first question we address is how complex the topology of an HDA model of a concurrent system can be. I will show that for every connected polyhedron there exists a concurrent system whose HDA model has the same homotopy type as the polyhedron. The second contribution I will present concerns the homology language of an HDA, which is a graded submodule of an exterior algebra and provides information about the independence structure of the modeled concurrent system. We prove that the homology language is actually a graded subcoalgebra of the exterior algebra. Finally, we introduce a new concept of directed homology for preordered spaces, called the homology digraph. The main result here is a Künneth formula, which enables one to compute the homology digraph of a product from the homology digraphs of the components.