# 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 online seminar.

# How

The seminar takes place on *zoom*.
If you want to participate,
send an email to uli@lrde.epita.fr
so that we can add you to our mailing list.
You will receive about one email per week in average:
seminar announcements, reminders, and the zoom link.

Talks generally last at most one hour, including time for questions.

# Upcoming Talks

See also the seminar's google calendar.

### Friday 6 October 2023 11:00 CEST

**Matt Earnshaw**,
TUT, 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 20 October 2023 11:00 CEST

**Łukasz Mikulski**,
NCU, Toruń, Poland:
TBA

### Friday 3 November 2023 11:00 CET

**Rob van Glabbeek**,
University of Edinburgh, Scotland:
TBA

### Friday 1 December 2023 11:00 CET

**Roman Kniazev**,
Ecole polytechnique, Palaiseau, France:
TBA

# Previous Talks

### 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**,
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é**,
OU, 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're
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.

uli@lrde.epita.fr