What
The (i)Po(m)set Project is a research project
at the crossroads of
concurrency theory, automata theory, algebra, and geometry.
You are at the page of its former online seminar.
How
The (i)Po(m)set Project Online Seminar was organized by
Uli Fahrenberg,
Christian Johansen,
Jérémy Ledent,
and Krzysztof Ziemiański
and took place regularly for a bit more than a year on zoom.
The seminar is closed and has been replaced by the
Paris Automata and Concurrency Theory Seminar.
Seminar Talks, in Reverse Chronological Order
Friday 28 June 2024 11:00 CEST
Ichiro Hasuo,
National Institute of Informatics, Tokyo, Japan:
Compositional Probabilistic Model Checking with String Diagrams of MDPs
We present a compositional model checking algorithm for Markov
decision processes, in which they are composed in the categorical
graphical language of string diagrams. The algorithm computes
optimal expected rewards. Our theoretical development of the
algorithm is supported by category theory, while what we call
decomposition equalities for expected rewards act as a key
enabler. Experimental evaluation demonstrates its performance
advantages. The talk is based on the following papers:
Friday 14 June 2024 11:00 CEST
Clovis Eberhart,
National Institute of Informatics, Tokyo, Japan:
Category theory for compositional verification
We present a recent line of work on open games, which describe
compositional frameworks for games, in particular parity games and
Markov decision processes. This is done by adding open ends that
form interfaces along which two games can be composed. By finding
adequate syntactic and semantic categories, we can then write
algorithms that can leverage compositionality to compute faster
solutions when there are repeated sub-games.
Here, we show the categorical machinery at work in the definition
of open parity games (OPGs) and related categories, as well as
some particularities that arise in the case of open Markov
decision processes (OMDPs). Our goal is to understand our main
results and why they are relevant. We also show that it is
possible to derive efficient algorithms from category theory.
Friday 31 May 2024 11:00 CEST
Michał Gajda,
Migamake Pte Ltd, Singapore:
Decomposition of countable semigroups and simplex languages
Krohn-Rhodes decomposition theorem for finite semigroups facilitates
many other results.
It has been so far generalized to residually finite semigroups.
We use the definition of archimedean semigroups together with
generalization of multiples to propose a further generalization
to decompose any countable semigroups.
We then examine the behaviour of this generalization, by characterizing
languages corresponding to arbitrary countable semigroups,
and proposing a geometric generalization of regular expressions that
provides a useful computable characterization of many such languages.
The work includes a definition of Countable HDA proposed by Krzysztof Ziemiański.
Friday 17 May 2024 11:00 CEST
Anca Muscholl,
LaBRI, Université Bordeaux, France:
On partial-order and automata techniques for analysing communication
Message-passing is a key synchronization feature for concurrent programming and distributed systems.
In this model, processes running asynchronously synchronize by exchanging messages over unbounded channels.
The usual semantics is based on peer-to-peer communication, which is very popular for reasoning about
telecommunication protocols. More recently, mailbox communication received increased attention because
of its usage in multi-thread programming, as provided by languages like Rust or Erlang.
This talk will first survey results on verification and synthesis for peer-to-peer communication.
In a second part we will discuss recent work on mailbox communication and related research perspectives.
Friday 5 April 2024 11:00 CEST
Fabio Gadducci,
Università di Pisa, Italy:
The algebraic view of concatenable net processes
Deterministic net processes characterise the concurrent computations
of a Petri net. Making them concatenable, i.e.equipping them with
suitable interfaces, allows for a neat axiomatisation of their
sequential and parallel composition. The talk presents recent
results concerning non-deterministic net processes and their
characterisation via dioidal categories.
Friday 15 March 2024 11:00 CET
Paul-André Melliès,
CNRS, Université Paris Cité, INRIA, France:
The rabbit calculus: convolution products on double categories and categorification of rule algebra
Reporting on recent joint work with Nicolas Behr and Noam
Zeilberger, I will describe the rabbit calculus, a convolution
product over preasheaves of double categories motivated by term and
graph rewriting theory. As I will explain, the convolution product
generalizes to every double category the usual Day tensor product of
presheaves of monoidal categories. One interesting aspect of the
construction is that this convolution product is in general only
oplax associative. For that reason, several classes of double
categories will be identified for which the convolution product is
not just oplax associative, but fully associative. This includes in
particular framed bicategories on the one hand, and double
categories of term and graph rewriting theories on the other. For
the latter, we establish a formula which justifies the view that the
convolution product categorifies the rule algebra product, and
captures the basic intuitions of causality in rewriting theory.
Slides
Friday 1 March 2024 11:00 CET
Henning Basold,
Universiteit Leiden, The Netherlands:
Towards higher coalgebra: the enriched case
There is an intricate link between concurrent systems and homotopy
theory, which has been exploited in the analysis of
higher-dimensional automata and distributed algorithms. The link
between computation and homotopy theory goes even further and my
long-term goal is to develop a general theory of higher coalgebras
in the context of (∞, n)-category theory for n ∈ {1,2}, which
provides an abstract account of this link. (∞, 1)-categories have
various models, among them topologically and simplicially enriched
categories. These are quite rigid models but they lend themselves to
concrete computations (see Lurie's Higher Topos Theory).
In this talk, I will first present some results on coalgebras that
arise from general enrichment, in particular we will look at
distributive laws, modal logic and effectful computations. We will
then go into the concrete case of topologically-enriched categories
to develop some homotopy theory of coalgebras in this concrete
setting. Particularly, we will focus on investigating modal logic
that is invariant under homotopy.
Slides;
Slides, annotated
Friday 16 February 2024 11:00 CET
Uli Fahrenberg,
LRE, Rennes/Paris, France:
Generating posets with interfaces
I will give an update on the algebra and combinatorics of gluing-parallel posets with interfaces.
These have been introduced some years ago as a common generalization of series-parallel posets and interval orders.
Their algebra and combinatorics turn out to be quite complicated, and progress has been slow.
I will talk a bit about algebra, but mostly about combinatorics, including forbidden substructures,
criteria for gluing decomposition, and a generalization of gluing-parallel posets which looks to have better combinatorial properties.
Friday 19 January 2024 11:00 CET
Thomas Kahl,
Universidade do Minho, Braga, Portugal:
Weak equivalence of higher-dimensional automata
I will introduce a coarse notion of equivalence for
higher-dimensional automata, called weak equivalence. Weak
equivalence focuses mainly on a traditional trace language and a
more recent homology language, which captures the overall
independence structure of an HDA. I also plan to show a software
tool that computes HDA models of concurrent systems written in the
Promela language.
Friday 12 January 2024 10:30 CET
Mikołaj Bojańczyk,
University of Warsaw, Poland:
About recognisability of graph languages
(i)Po(m)set Project Christmas Seminar, Postponed
I will give a tutorial about which graph languages are called
‶recognisable” or ‶regular”. I will explain how concepts like
tree-width and clique-width appear. I will try to be general enough
to cover variants of graphs such as partially ordered multisets.
Friday 1 December 2023 11:00 CET
Roman Kniazev,
IRIF, Paris, France:
Simplicial models for epistemic logic (sprinkled with concurrency)
I will present the fundamentals of simplicial models for epistemic
logic. Epistemic logic, a flavor of modal logic that deals with
knowledge, has found successful applications in the study of
distributed systems, particularly for showing (un)solvability of
specific distributed tasks. Simultaneously, topological models of
distributed systems, based on simplicial complexes, have
demonstrated similar results.
I'll establish the connection between these two approaches and
demonstrate how to employ simplicial sets instead of simplicial
complexes to capture intriguing phenomena in multi-agent epistemic
logic. The talk will conclude with a construction that links these
simplicial models with HDAs.
The presentation is based on joint work with Eric Goubault, Jérémy
Ledent and Sergio Rajsbaum
(
https://arxiv.org/abs/2303.14976)
and my PhD thesis.
Friday 17 November 2023 11:00 CET
Amar Hadzihasanovic,
TalTech, Tallinn, Estonia:
The homotopy posets of a category
I will present two invariants which, to a category C, associate
functors pi_0(C/-), pi_1(C/-) defined on C with values in the
category of pointed posets. These generalise the pi_0 and pi_1 of a
groupoid in the sense that, if C is a groupoid and x an object in C,
pi_0(C/x) and pi_1(C/x) are discrete posets isomorphic,
respectively, to the set of connected components of C and to the
underlying set of the group of automorphisms of x.
Their main property is that they "vanish" precisely on terminal
objects in C: that is, pi_0(C/x) and pi_1(C/x) are both
single-element posets if and only if x is a terminal object in C. In
this sense, any element of pi_0(C/x) and pi_1(C/x) besides the
basepoint may be seen as an "obstruction to x being terminal".
After giving the definition of the invariants, I will explore some
of their properties more in depth: in what ways they are functorial,
and under what conditions the posets are endowed with extra
properties or structures, such as the existence of joins or a
monoidal structure.
This talk is based on joint work with Caterina Puca, Fabrizio Genovese,
and Bob Coecke (arXiv:2307.14461).
Friday 3 November 2023 11:00 CET
Rob van Glabbeek,
University of Edinburgh, Scotland:
Translating Petri nets to higher-dimensional automata
Higher-dimensional automata (HDAs) are a natural semantic model for
Petri nets and other formalisms for concurrent systems. I will show
how to translate Petri nets to HDAs, using different semantics, and
discuss some of the properties of these translations. Hopefully a
discussion will ensue on the motivations for this work and how to
carry it further.
Friday 20 October 2023 11:00 CEST
Łukasz Mikulski,
NCU, Toruń, Poland:
Relational structures for interval order semantics of concurrent systems
Relational structures based on acyclic relations capturing the
'before' relationship can provide a successful frameworks for the
modelling and verification of a wide class of concurrent systems
behaviour. There are also relational structures with an acyclic
'before' (strong precedence) relationship and a possibly cyclic 'not
later than' (weak precedence) relationship, which are able to treat
more general concurrent behaviours. However, in each of these cases,
the execution model is based on sequences or step sequences of
executed actions, where actions are assumed to be executed
instantaneously. We will try to remove this restriction and consider
executions modelled by interval orders, where actions are assumed to
be executed non-instantaneously. For this execution model, we will
discuss relational structures which can express both strong
precedence and weak precedence relationships. Interestingly, in the
considered model any mixed cycle of strong and weak precedences is
allowed, provided that it contains at least two consecutive weak
precedence relationships.
Friday 6 October 2023 11:00 CEST
Matt Earnshaw,
TalTech, Tallinn, Estonia:
Monoidal languages
Monoidal language theory is an approach to languages of graphs via
the graphical calculus of string diagrams for monoidal
categories. The class of regular monoidal languages includes regular
languages of words and trees, but also recognizable trace
languages. In this talk I will give an introduction to this theory,
starting from the basics. This will include grammars and automata
for monoidal languages, a pumping lemma, results on determinization,
algebraic recognizability, and applications to Mazurkiewicz trace
languages and asynchronous automata. Time permitting, we will
outline work in progress on the context-free theory.
Friday 15 September 2023 11:00 CEST
Matteo Acclavio,
SDU, Odense, Denmark:
The proof theory of pomsets
Pomset Logic was defined in Retoré's PhD thesis (1993) through the
study of coherent spaces, a categorical interpretation of Linear
Logic. It is characterized by the presence of a non-commutative
sulf-dual binary connective, which can be used to internalize a
notion of order, and the study of its proof theory has led to the
introduction of completely novel approaches and techniques in the
field.
The aim of this talk is to provide an overview of the results on
Pomset logic and its "offspring" (the logic BV and its extensions),
as well as their connections with the theory of pomsets, concurrent
Kleene algebras, and applications to process calculi.
Friday 1 September 2023 11:00 CEST
Loïc Hélouët,
IRISA, Rennes, France:
Waiting nets
In Time Petri nets (TPNs), time and control are tightly connected:
time measurement for a transition starts only when all resources
needed to fire it are available. For many systems, one wants to
start measuring time as soon as a part of the preset of a transition
is filled, and fire it after some delay and when all needed
resources are available.
This work considers an extension of TPN called waiting nets
decoupling time measurement and control. Their semantics ignores
urgency when upper bounds of intervals are reached but some
resources needed to fire are not yet available. Firing of a
transition is then allowed as soon as missing resources become
available. This semantics extension resembles stopwatches, but is
in fact weaker.
It is known that extending bounded TPNs with stopwatches leads to
undecidability. Our extension is weaker, and bounded Waiting nets
are not Turing powerful. Interestingly, state classes, a standard
technique to build a finite abstract representation of the sate
space and analyze bounded time Petri nets extends to waiting nets.
We show how to compute a finite state class graph for bounded
waiting nets, yielding decidability of reachability and
coverability. We then compare expressiveness of waiting nets with
that of other models and show that they are strictly more expressive
than TPNs.
Friday 18 August 2023 11:00 CEST
Jérémy Dubut-Kross,
AIST, Tokyo, Japan:
Bisimulations and unfolding in P-accessible categorical models
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 glueings of paths. We show that
transition systems and presheaf models are instances of our
framework. We also prove that in our framework, several notions of
bisimulation coincide, in particular an ‶operational one” akin to
the standard definition in transition systems. Also, our notion of
accessibility is preserved by coreflections. This also leads us to a
notion of unfolding that behaves well in the accessible case: it is
a right adjoint and is a universal covering, i.e., it is 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, is an unfolding, when the category of path
shapes is well chosen. Joint work with Éric and Jean Goubault.
Friday 14 July 2023 11:00 CEST
Marie Fortin,
IRIF, Paris, France:
Logics and automata for Message Sequence Charts
Message sequence charts (MSCs) are partial orders representing
executions of message-passing systems. They arise as executions of
communicating automata, in which a fixed number of finite-state
processes communicate through FIFO channels: Where a standard finite
automaton defines a language of words, communicating automata define
languages of MSCs. In this talk, I will give an overview of
different formalisms that can be used to specify sets of MSCs, and
explain how fundamental results from formal language theory such as
the Büchi-Elgot-Trakhtenbrot theorem can be extended to MSCs.
Friday 16 June 2023 11:00 CEST
Tobias Kappé,
Open Universiteit, The Netherlands:
Completeness and the finite model property for Kleene algebra, reconsidered
Kleene Algebra (KA) is the algebra of regular expressions. Central
to the study of KA is Kozen's (1994) completeness result, which says
that any equivalence valid in the language model of KA follows from
the axioms of KA. Also of interest is the finite model property
(FMP), which says that false equivalences always have a finite
counterexample. Palka (2005) showed that, for KA, the FMP is
equivalent to completeness.
We provide a unified and elementary proof of both properties. In
contrast with earlier completeness proofs, this proof does not rely
on minimality or bisimilarity techniques for deterministic
automata. Instead, our approach avoids deterministic automata
altogether, and uses Antimirov's derivatives and the well-known
transition monoid construction.
Towards the end, we will offer some thoughts on whether or not these
techniques can be generalized to attack the open completeness
problem for downward-closed series-parallel rational expressions.
Friday 19 May 2023 11:00 CEST
Amazigh Amrane,
EPITA Paris, France:
Series-parallel pomsets: automata and logic
In order to model concurrency, Lodaya and Weil extended
automata theory from the usual word languages to sets of labelled
series-parallel posets (pomset) languages. These languages are
subsets of SP($A$): the smallest class containing the empty
pomset, the letters of $A$ and being closed under sequential
product (concatenation) and parallel product, or equivalently, the
class of posets labelled by the alphabet $A$, having finite
antichains and not containing four distinct elements $x$, $y$,
$z$, $t$ whose relative order form an N: $x < y$, $z < y$ and $z <
t$.
In this talk we focus on a Kleene-like theorem and a
Büchi-Elgot-Trakhtenbrot-like theorem on languages of
SP($A$). Lodaya and Weil introduced a notion of branching
automata. It is a generalization of Kleene automata with two new
types of transitions: fork and join transitions, in addition to
the usual sequential transitions of Kleene automata. The fork
transitions allow to execute concurrently a finite number of
instruction flows and the join transitions merge them. These
automata accept subsets of SP($A$) of unbounded width. Lodaya and
Weil introduced a generalization of the usual rational expressions
to catch the expressivity of branching automata. These two
equivalent models can be restricted to both accept, in an
equivalent way, subsets of SP($A$) of bounded width.
From a logical point of view, Kuske showed that a rational
language of SP($A$) is of bounded width if and only if it is
definable in monadic second order (MSO) logic. However, MSO alone
does not suffice for rational languages of unbounded width. The
finite parallel iteration is not MSO-definable. Bedon introduced
P-MSO, which is monadic second order mixed with Presburger
arithmetic. He shows that the languages of branching automata are
exactly those definable in P-MSO logic. As a consequence, the
P-MSO theory of SP($A$) is decidable.
Friday 14 April 2023 11:00 CEST
Sergio Rajsbaum,
UNAM, Mexico and IRIF, Paris, France:
Unifying concurrent objects and distributed tasks: interval-linearizability
Tasks and objects are two predominant ways of specifying
distributed problems where processes should compute outputs based
on their inputs. Roughly speaking, a task specifies, for each set
of processes and each possible assignment of input values, they are
valid outputs. In contrast, an object is defined by a sequential
specification. Also, an object can be invoked multiple times by
each process, while a task is a one-shot problem. Each one
requires its own implementation notion, stating when an execution
satisfies the specification. For objects, linearizability is
commonly used, while tasks implementation notions are less
explored.
The talk overviews results presented in JACM 2018 together with
Castañeda and Raynal, about the notion of interval-sequential
object, and the corresponding implementation notion of
interval-linearizability, to encompass many problems that have no
sequential specification as objects. A main result of the article
is that interval-sequential objects and (refined) tasks have the
same expressive power and both are complete in the sense that they
are able to specify any prefix-closed set of well-formed
executions.
Friday 17 March 2023 11:00 CET
Safa Zouari,
NTNU Gjøvik, Norway:
Logical characterization of hh-bisimulation via open maps for HDA
The categorical approach of Nielsen & Winskel came up with a
unifying understanding of models of concurrency. Previous
applications of this method to higher dimensional automata (HDA)
have not treated the logic that it yields in much detail. In this
work, we follow the same approach to introduce a new notion of
Bisimulation from open maps and its characteristic path
logic. Further, we investigate fragments of the logic and the
bisimulations that they capture. To this end, we rely on the
recent categorical definition of HDA and the notion of track
objects. The motivation for this study is to develop modal
characterization for all concurrency bisimulations.
ppos-owner@ml.lre.epita.fr